1.1 --- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Wed Feb 17 15:43:34 2021 +0100
     1.2 +++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Fri Feb 26 13:13:03 2021 +0100
     1.3 @@ -91,7 +91,16 @@
     1.4  ### Token.syntax_generic, Scan.error
     1.5  \<close>
     1.6  subsubsection \<open>click on "from \<open>0 < d\<close>"\<close>
     1.7 -text \<open>
     1.8 +text \<open>COMPARE Calculation.thy,
     1.9 +subsubsection \<open>on Given: WITHOUT "Specification:" OUTCOMMENTED\<close>
    1.10 +?WHERE DOES DOUBLING COME FROM BELOW..
    1.11 +
    1.12 +-----------------v BEGIN ---------------vv END of      \<open>0 < d\<close>, the argument of "from:
    1.13 +Token ((Pos ((0, 6, 13), [_]), Pos ((0, 13, 0), [_])), \<open>0 < d\<close>, _) 
    1.14 +
    1.15 +---------------------------------------------------------- SCAN STOPS BEFORE "have "0 \<le> c mod d""
    1.16 +Token ((Pos ((0, 6, 13), [_]), Pos ((0, 13, 0), [_])), \<open>0 < d\<close>, _), 
    1.17 +Token ((Pos ((0, 13, 0), [_]), Pos ((0, 0, 0), [_])), , _) 
    1.18  ### Private_Output.report keyword1
    1.19  ### Private_Output.report cartouch
    1.20  ### Private_Output.report delimite

     2.1 --- a/src/Pure/General/position.ML	Wed Feb 17 15:43:34 2021 +0100
     2.2 +++ b/src/Pure/General/position.ML	Fri Feb 26 13:13:03 2021 +0100
     2.3 @@ -10,6 +10,7 @@
     2.4    val ord: T ord
     2.5    val make: Thread_Position.T -> T
     2.6    val dest: T -> Thread_Position.T
     2.7 +  val to_string: T -> string (*WN*)
     2.8    val line_of: T -> int option
     2.9    val offset_of: T -> int option
    2.10    val end_offset_of: T -> int option
    2.11 @@ -95,6 +96,9 @@
    2.12  fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props);
    2.13  fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};
    2.14  
    2.15 +(*WN*)fun to_string (Pos ((line, offset, end_offset), _)) = ("Pos ((" ^
    2.16 +  string_of_int line ^ ", " ^ string_of_int offset ^ ", " ^ string_of_int end_offset ^ "), [_])")
    2.17 +
    2.18  fun valid (i: int) = i > 0;
    2.19  fun if_valid i i' = if valid i then i' else i;
    2.20  

     3.1 --- a/src/Pure/General/scan.ML	Wed Feb 17 15:43:34 2021 +0100
     3.2 +++ b/src/Pure/General/scan.ML	Fri Feb 26 13:13:03 2021 +0100
     3.3 @@ -6,7 +6,7 @@
     3.4  
     3.5  infix 5 -- :-- :|-- |-- --| ^^;
     3.6  infixr 5 ::: @@@;
     3.7 -infix 3 >>;
     3.8 +infix 3 >> @@>>;
     3.9  infixr 0 ||;
    3.10  
    3.11  signature BASIC_SCAN =
    3.12 @@ -15,7 +15,8 @@
    3.13    (*error msg handler*)
    3.14    val !! : ('a * message option -> message) -> ('a -> 'b) -> 'a -> 'b
    3.15    (*apply function*)
    3.16 -  val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
    3.17 +  val >> :                 ('a -> 'b * 'c)  * ('b -> 'd) -> 'a -> 'd * 'c
    3.18 +  val @@>> : (('a -> 'b) * ('a -> 'c * 'd)) * ('c -> 'e) -> 'a -> 'e * 'd
    3.19    (*alternative*)
    3.20    val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
    3.21    (*sequential pairing*)
    3.22 @@ -127,7 +128,8 @@
    3.23  
    3.24  (* scanner combinators *)
    3.25  
    3.26 -fun (scan >> f) xs = scan xs |>> f;
    3.27 +fun (scan >> f) xs =                       scan xs  |>> f;
    3.28 +fun ((write, scan) @@>> f) xs = (write xs; scan xs) |>> f;
    3.29  
    3.30  fun (scan1 || scan2) xs = scan1 xs handle FAIL _ => scan2 xs;
    3.31  

     4.1 --- a/src/Pure/Isar/token.ML	Wed Feb 17 15:43:34 2021 +0100
     4.2 +++ b/src/Pure/Isar/token.ML	Fri Feb 26 13:13:03 2021 +0100
     4.3 @@ -30,6 +30,7 @@
     4.4      Declaration of declaration |
     4.5      Files of file Exn.result list
     4.6    val pos_of: T -> Position.T
     4.7 +  val end_pos_of: T -> Position.T (*WN*)
     4.8    val adjust_offsets: (int -> int option) -> T -> T
     4.9    val eof: T
    4.10    val is_eof: T -> bool
    4.11 @@ -64,6 +65,7 @@
    4.12    val reports: Keyword.keywords -> T -> Position.report_text list
    4.13    val markups: Keyword.keywords -> T -> Markup.T list
    4.14    val unparse: T -> string
    4.15 +  val s_to_string: T list -> string
    4.16    val print: T -> string
    4.17    val text_of: T -> string * string
    4.18    val file_source: file -> Input.source
    4.19 @@ -357,6 +359,15 @@
    4.20    | EOF => ""
    4.21    | _ => x);
    4.22  
    4.23 +(*WN-------------------------------------------------------------------------------------------\\*)
    4.24 +fun to_string tok = ("\nToken ((" ^
    4.25 +  Position.to_string (pos_of tok) ^ ", " ^ 
    4.26 +  Position.to_string (end_pos_of tok) ^ "), " ^
    4.27 +  unparse tok ^ ", _)")
    4.28 +
    4.29 +fun s_to_string toks = fold (curry op ^) (map to_string toks |> rev |> separate ", ") "";
    4.30 +(*WN-------------------------------------------------------------------------------------------//*)
    4.31 +
    4.32  fun print tok = Markup.markups (markups Keyword.empty_keywords tok) (unparse tok);
    4.33  
    4.34  fun text_of tok =

     5.1 --- a/src/Pure/Pure.thy	Wed Feb 17 15:43:34 2021 +0100
     5.2 +++ b/src/Pure/Pure.thy	Fri Feb 26 13:13:03 2021 +0100
     5.3 @@ -811,7 +811,7 @@
     5.4  
     5.5  val _ =
     5.6    Outer_Syntax.command \<^command_keyword>\<open>from\<close> "forward chaining from given facts"
     5.7 -    (facts >>
     5.8 +    ((writeln o Token.s_to_string, facts) @@>>
     5.9        (writeln "####-## from Proof.from_thmss_cmd";(Toplevel.proof o Proof.from_thmss_cmd)));
    5.10  
    5.11  val _ =

     6.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Wed Feb 17 15:43:34 2021 +0100
     6.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Fri Feb 26 13:13:03 2021 +0100
     6.3 @@ -46,14 +46,74 @@
     6.4  \<close> ML \<open>
     6.5  \<close>
     6.6  
     6.7 +subsubsection \<open>tools to analyse parsing in Outer_Syntax >> \<close>
     6.8 +ML \<open>
     6.9 +\<close> text \<open> (*original basics.ML*)
    6.10 +op |>> : ('a * 'b) * ('a -> 'c) -> 'c * 'b;
    6.11 +fun (x, y) |>> f = (f x, y);
    6.12 +\<close> text \<open> (*original scan.ML*)
    6.13 +op >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c;                              (*---vvv*)
    6.14 +fun (scan >> f) xs = scan xs |>> f;
    6.15 +\<close> ML \<open>
    6.16 +\<close> ML \<open> (*cp.from originals*)
    6.17 +infix 3 @>>;
    6.18 +fun (scan @>> f) xs = scan xs |>> f;
    6.19 +op @>> : ('a        -> 'b * 'c)        * ('b -> 'd) -> 'a        -> 'd * 'c;        (*---^^^*)
    6.20 +\<close> ML \<open> (*appl.to parser*)
    6.21 +op @>> : (Token.src -> 'b * Token.src) * ('b -> 'd) -> Token.src -> 'd * Token.src; (*---^^^*)
    6.22 +\<close> ML \<open>
    6.23 +\<close> ML \<open> (*add analysis*)
    6.24 +\<close> text \<open>
    6.25 +datatype T = Pos of (int * int * int) * Properties.T;
    6.26 +
    6.27 +fun s_to_string (Pos ((line, offset, end_offset), _)) = ("Pos ((" ^
    6.28 +  string_of_int line ^ ", " ^ string_of_int offset ^ ", " ^ string_of_int end_offset ^ "), [_])")
    6.29 +
    6.30 +s_to_string: src -> string
    6.31 +\<close> text \<open>
    6.32 +datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot
    6.33 +\<close> ML \<open>
    6.34 +Token.pos_of;        (*^^^^^^^^^^^^^^^*)
    6.35 +Token.end_pos_of;                      (*^^^^^^^^^^^^^*)
    6.36 +Token.unparse;                                            (*^^^^^^^^^^^^^*)
    6.37 +\<close> ML \<open>
    6.38 +fun string_of_tok tok = ("\nToken ((" ^
    6.39 +  Position.to_string (Token.pos_of tok) ^ ", " ^ 
    6.40 +  Position.to_string (Token.end_pos_of tok) ^ "), " ^
    6.41 +  Token.unparse tok ^ ", _)")
    6.42 +\<close> ML \<open>
    6.43 +fun string_of_toks toks = fold (curry op ^) (map string_of_tok toks |> rev |> separate ", ") "";
    6.44 +string_of_toks:    Token.src -> string;
    6.45 +\<close> ML \<open>
    6.46 +Token.s_to_string: Token.src -> string; (*<-- string_of_toks WN*)
    6.47 +\<close> ML \<open>
    6.48 +fun (scan @>> f) xs = (@{print}{a = "_ >> ", toks = xs(*GIVES\<rightarrow>"?"*)}; scan xs) |>> f;
    6.49 +fun (scan @>> f) xs = (writeln ("toks= " ^ Token.s_to_string xs);      scan xs) |>> f;
    6.50 +op @>> : (Token.src -> 'b * Token.src) * ('b -> 'd) -> Token.src -> 'd * Token.src; (*---^^^*)
    6.51 +\<close> ML \<open>
    6.52 +op @>> : (Token.T list -> 'a * 'b) * ('a -> 'c) -> Token.T list -> 'c * 'b
    6.53 +\<close> ML \<open>
    6.54 +\<close> ML \<open> (*Scan < Token in bootstrap, thus we take Token.s_to_string as argument of >> *)
    6.55 +infix 3 @@>>;
    6.56 +\<close> ML \<open>
    6.57 +fun ((write, scan) @@>> f) xs = (write xs;                             scan xs) |>> f;
    6.58 +op @@>> : (('a -> 'b) * ('a -> 'c * 'd)) * ('c -> 'e) -> 'a -> 'e * 'd
    6.59 +\<close> ML \<open>
    6.60 +\<close> ML \<open>
    6.61 +\<close> ML \<open>
    6.62 +\<close> ML \<open>
    6.63 +\<close>
    6.64 +
    6.65 +
    6.66  subsubsection \<open>TODO\<close>
    6.67  ML \<open>
    6.68  \<close> ML \<open>
    6.69  \<close> ML \<open>
    6.70 +\<close> ML \<open>
    6.71  \<close>
    6.72  
    6.73  section \<open>setup command_keyword + preliminary test\<close>
    6.74 -ML \<open>
    6.75 +ML \<open>                                            
    6.76  \<close> ML \<open>
    6.77  val _ =                                                  
    6.78    Outer_Syntax.command \<^command_keyword>\<open>Example\<close> "start a Calculation from a Formalise-file"
    6.79 @@ -71,7 +131,8 @@
    6.80    Outer_Syntax.command \<^command_keyword>\<open>Problem\<close>
    6.81      "start a Specification, either from scratch or from preceding 'Example'"
    6.82  (** )(ParseC.problem >> (Toplevel.theory o Preliminary.init_specify));( **)
    6.83 -(**)(ParseC.problem_headline >> (Toplevel.theory o Preliminary.init_specify));(**)
    6.84 +(**)((writeln o Token.s_to_string, ParseC.problem_headline)
    6.85 +      @@>> (Toplevel.theory o Preliminary.init_specify));(**)
    6.86  \<close> ML \<open>
    6.87  (**)                   Preliminary.init_specify: ParseC.problem_headline -> theory -> theory;(**)
    6.88  (*                                                                          ^^^^^^    ^^^^^^*)
    6.89 @@ -82,13 +143,14 @@
    6.90  \<close> ML \<open>
    6.91  val _ =
    6.92    Outer_Syntax.command \<^command_keyword>\<open>Given\<close> "input Given items to the Model of a Specification"
    6.93 -    (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
    6.94 +(*                                (facts    >> (Toplevel.proof o Proof.from_thmss_cmd));*)
    6.95 +    ((writeln o Token.s_to_string, facts) @@>> (Toplevel.proof o Proof.from_thmss_cmd));
    6.96  val _ =
    6.97    Outer_Syntax.command \<^command_keyword>\<open>Find\<close> "input Find items to the Model of a Specification"
    6.98 -    (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
    6.99 +    (facts @>> (Toplevel.proof o Proof.from_thmss_cmd));
   6.100  val _ =
   6.101    Outer_Syntax.command \<^command_keyword>\<open>Relate\<close> "input Relate items to the Model of a Specification"
   6.102 -    (facts >> (Toplevel.proof o Proof.from_thmss_cmd));
   6.103 +    (facts @>> (Toplevel.proof o Proof.from_thmss_cmd));
   6.104  \<close> ML \<open>
   6.105  (Toplevel.proof o Proof.from_thmss_cmd)
   6.106  :
   6.107 @@ -101,17 +163,52 @@
   6.108  \<close> ML \<open>
   6.109  @{here}(*val it = {offset=8, end_offset=12, id=-4402}: Position.T*)
   6.110  \<close> ML \<open>
   6.111 +\<close> ML \<open>
   6.112 +\<close> ML \<open>
   6.113 +\<close> ML \<open>
   6.114 +val problem_headline_str =
   6.115 +  "( \"Biegelinie\" , [\"Biegelinien\"] )";
   6.116 +\<close> ML \<open>
   6.117 +val problem_headline_str =
   6.118 +  "( \"Biegelinie\" , [\"Biegelinien\"] ) \n" ^
   6.119 +  "(*1 collapse*) \n" ^
   6.120 +  "  Specification:";
   6.121 +\<close> ML \<open>
   6.122 +val toks = ParseC.tokenize problem_headline_str;
   6.123 +\<close> text \<open>
   6.124 +[Token (("(", ({}, {})), (Keyword, "("), Slot), 
   6.125 + Token (("Biegelinie", ({}, {})), (String, "Biegelinie"), Slot), 
   6.126 + Token ((",", ({}, {})), (Keyword, ","), Slot), 
   6.127 + Token (("[", ({}, {})), (Keyword, "["), Slot),
   6.128 + Token (("Biegelinien", ({}, {})), (String, "Biegelinien"), Slot), 
   6.129 + Token (("]", ({}, {})), (Keyword, "]"), Slot), 
   6.130 + Token ((")", ({}, {})), (Keyword, ")"), Slot),
   6.131 + Token (("Specification", ({}, {})), (Keyword, "Specification"), Slot), 
   6.132 + Token ((":", ({}, {})), (Keyword, ":"), Slot)]
   6.133 +\<close> ML \<open>
   6.134 +ParseC.problem_headline toks
   6.135 +\<close> text \<open> (->K, )->Z:
   6.136 +((((("K", "Biegelinie"
   6.137 +    ), ","
   6.138 +   ), ["Biegelinien"]
   6.139 +  ), "Z"
   6.140 + ), 
   6.141 + [Token (("Specification", ({}, {})), (Keyword, "Specification"), Slot), 
   6.142 +  Token ((":", ({}, {})), (Keyword, ":"), Slot)
   6.143 + ]
   6.144 +)
   6.145 +\<close> ML \<open>
   6.146 +\<close> ML \<open>
   6.147  \<close>
   6.148  
   6.149  subsection \<open>test runs with test-Example\<close>
   6.150  (**)
   6.151  Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>
   6.152 -(*(1) outcomment before creating session Isac*)
   6.153  
   6.154  Problem ("Biegelinie", ["Biegelinien"])
   6.155  (*1 collapse* )
   6.156    Specification:                                               (*Outer syntax error\<^here>: command expected, but keyword Specification\<^here> was found*)
   6.157 -  (*2 collapse* )
   6.158 +  (*2 collapse*)
   6.159      Model:
   6.160        Given: "Traegerlaenge " "Streckenlast "              
   6.161        Where: "q_0 ist_integrierbar_auf {| 0, L |}" "0 < L"     (*Outer syntax error\<^here>: command expected, but keyword Where\<^here> was found*)
   6.162 @@ -123,16 +220,116 @@
   6.163        RProblem: ["", ""]
   6.164        RMethod: ["", ""]
   6.165        (*3 collapse*)
   6.166 -  ( *2 collapse*)
   6.167 +  (*2 collapse*)
   6.168    Solution:
   6.169  ( *1 collapse*)
   6.170 -(*(1) outcomment before creating session Isac*)
   6.171  (*
   6.172    compare click on above Given: "Traegerlaenge ", "Streckenlast " 
   6.173    with click on from \<open>0 < d\<close> in SPARK/../Greatest_Common_Divisorthy
   6.174  *)
   6.175  
   6.176 -subsection \<open><Output> BY CLICK ON Problem..Solution\<close>
   6.177 +subsection \<open><Output> BY CLICK ON Problem..Given: Position, command-range?\<close>
   6.178 +subsubsection \<open>on Problem: WITHOUT "Specification:" OUTCOMMENTED\<close>
   6.179 +text \<open>
   6.180 +              line * offset * end_offset
   6.181 +       Symbol_Pos.text       * Position.range)* (kind * string) * slot
   6.182 +-----------------------------------------------------------------------------------
   6.183 +-----------------v BEGIN ---------------vv END OF -----v
   6.184 +Token ((Pos ((0, 9, 10), [_]), Pos ((0, 10, 0), [_])), (, _), 
   6.185 +Token ((Pos ((0, 10, 22), [_]), Pos ((0, 22, 0), [_])), "Biegelinie", _),  //INCLUDING ""
   6.186 +Token ((Pos ((0, 22, 23), [_]), Pos ((0, 23, 0), [_])), ,, _), 
   6.187 +Token ((Pos ((0, 24, 25), [_]), Pos ((0, 25, 0), [_])), [, _), 
   6.188 +Token ((Pos ((0, 25, 38), [_]), Pos ((0, 38, 0), [_])), "Biegelinien", _), 
   6.189 +Token ((Pos ((0, 38, 39), [_]), Pos ((0, 39, 0), [_])), ], _), 
   6.190 +Token ((Pos ((0, 39, 40), [_]), Pos ((0, 40, 0), [_])), ), _), 
   6.191 +Token ((Pos ((0, 58, 71), [_]), Pos ((0, 71, 0), [_])), Specification, _), //58: "P"robken .. "S"pecification
   6.192 +Token ((Pos ((0, 71, 72), [_]), Pos ((0, 72, 0), [_])), :, _), 
   6.193 +Token ((Pos ((0, 220, 225), [_]), Pos ((0, 225, 0), [_])), Model, _),      //LONG COMMENT INBETWEEN
   6.194 +Token ((Pos ((0, 225, 226), [_]), Pos ((0, 226, 0), [_])), :, _) 
   6.195 +-----------------------------------------------------------^ STOPS BEFORE Given WITH Outer_Syntax.
   6.196 +Outer syntax error: command expected,
   6.197 +but keyword Specification was found
   6.198 +\<close>
   6.199 +subsubsection \<open>on Problem: WITH "Specification:" OUTCOMMENTED\<close>
   6.200 +text \<open>
   6.201 +-----------------v BEGIN ---------------vv END OF -----v
   6.202 +Token ((Pos ((0, 9, 10), [_]), Pos ((0, 10, 0), [_])), (, _), 
   6.203 +Token ((Pos ((0, 10, 22), [_]), Pos ((0, 22, 0), [_])), "Biegelinie", _),  //INCLUDING ""
   6.204 +Token ((Pos ((0, 22, 23), [_]), Pos ((0, 23, 0), [_])), ,, _), 
   6.205 +Token ((Pos ((0, 24, 25), [_]), Pos ((0, 25, 0), [_])), [, _), 
   6.206 +Token ((Pos ((0, 25, 38), [_]), Pos ((0, 38, 0), [_])), "Biegelinien", _), 
   6.207 +Token ((Pos ((0, 38, 39), [_]), Pos ((0, 39, 0), [_])), ], _), 
   6.208 +Token ((Pos ((0, 39, 40), [_]), Pos ((0, 40, 0), [_])), ), _) 
   6.209 +{a = "//--- Spark_Commands.init_specify", headline =
   6.210 + (((("(", "Biegelinie"), ","), ["Biegelinien"]), ")")} (line 119 of "~~/src/Tools/isac/BridgeJEdit/preliminary.sml")
   6.211 +\<close>
   6.212 +subsubsection \<open>on Problem: == on Specification: == on Model:\<close>
   6.213 +
   6.214 +subsubsection \<open>on Given: WITHOUT "Specification:" OUTCOMMENTED\<close>
   6.215 +text \<open>COMPARE Greatest_Common_Divisor.thy
   6.216 +subsubsection \<open>click on "from \<open>0 < d\<close>"\<close>
   6.217 +
   6.218 +              line * offset * end_offset
   6.219 +       Symbol_Pos.text      * Position.range)* (kind * string) * slot
   6.220 +-----------------------------------------------------------------------------------
   6.221 +Token ((Pos ((0, 6, 7), [_]), Pos ((0, 7, 0), [_])), :, _), 
   6.222 +Token ((Pos ((0, 8, 24), [_]), Pos ((0, 24, 0), [_])), "Traegerlaenge ", _), 
   6.223 +Token ((Pos ((0, 25, 40), [_]), Pos ((0, 40, 0), [_])), "Streckenlast ", _), 
   6.224 +---------------------------------------------------------- PARSER DOES NOT STOP..
   6.225 +Token ((Pos ((0, 61, 66), [_]), Pos ((0, 66, 0), [_])), Where, _), 
   6.226 +Token ((Pos ((0, 66, 67), [_]), Pos ((0, 67, 0), [_])), :, _), 
   6.227 +Token ((Pos ((0, 68, 105), [_]), Pos ((0, 105, 0), [_])), "q_0 ist_integrierbar_auf {| 0, L |}", _),
   6.228 +Token ((Pos ((0, 106, 113), [_]), Pos ((0, 113, 0), [_])), "0 < L", _) 
   6.229 +Outer syntax error: command expected,
   6.230 +but keyword Where was found
   6.231 +\<close>
   6.232 +subsubsection \<open>on Where: == on Given:\<close>
   6.233 +
   6.234 +subsubsection \<open>on Find:\<close>
   6.235 +text \<open>
   6.236 +toks= 
   6.237 +Token ((Pos ((0, 5, 6), [_]), Pos ((0, 6, 0), [_])), :, _), 
   6.238 +Token ((Pos ((0, 7, 20), [_]), Pos ((0, 20, 0), [_])), "Biegelinie ", _) 
   6.239 +toks= 
   6.240 +Token ((Pos ((0, 5, 6), [_]), Pos ((0, 6, 0), [_])), :, _), 
   6.241 +Token ((Pos ((0, 7, 20), [_]), Pos ((0, 20, 0), [_])), "Biegelinie ", _), 
   6.242 +Token ((Pos ((0, 20, 0), [_]), Pos ((0, 0, 0), [_])), , _) 
   6.243 +Bad context for command "Find" -- using reset state
   6.244 +\<close>
   6.245 +subsubsection \<open>on Relate:\<close>
   6.246 +text \<open>
   6.247 +toks= 
   6.248 +Token ((Pos ((0, 7, 8), [_]), Pos ((0, 8, 0), [_])), :, _), 
   6.249 +Token ((Pos ((0, 9, 27), [_]), Pos ((0, 27, 0), [_])), "Randbedingungen ", _), 
   6.250 +Token ((Pos ((0, 32, 42), [_]), Pos ((0, 42, 0), [_])), References, _), 
   6.251 +Token ((Pos ((0, 42, 43), [_]), Pos ((0, 43, 0), [_])), :, _), 
   6.252 +Token ((Pos ((0, 195, 202), [_]), Pos ((0, 202, 0), [_])), RTheory, _), 
   6.253 +Token ((Pos ((0, 202, 203), [_]), Pos ((0, 203, 0), [_])), :, _), 
   6.254 +Token ((Pos ((0, 204, 206), [_]), Pos ((0, 206, 0), [_])), "", _), 
   6.255 +Token ((Pos ((0, 213, 221), [_]), Pos ((0, 221, 0), [_])), RProblem, _), 
   6.256 +Token ((Pos ((0, 221, 222), [_]), Pos ((0, 222, 0), [_])), :, _), 
   6.257 +Token ((Pos ((0, 223, 224), [_]), Pos ((0, 224, 0), [_])), [, _), 
   6.258 +Token ((Pos ((0, 224, 226), [_]), Pos ((0, 226, 0), [_])), "", _), 
   6.259 +Token ((Pos ((0, 226, 227), [_]), Pos ((0, 227, 0), [_])), ,, _), 
   6.260 +Token ((Pos ((0, 228, 230), [_]), Pos ((0, 230, 0), [_])), "", _), 
   6.261 +Token ((Pos ((0, 230, 231), [_]), Pos ((0, 231, 0), [_])), ], _), 
   6.262 +Token ((Pos ((0, 238, 245), [_]), Pos ((0, 245, 0), [_])), RMethod, _), 
   6.263 +Token ((Pos ((0, 245, 246), [_]), Pos ((0, 246, 0), [_])), :, _), 
   6.264 +Token ((Pos ((0, 247, 248), [_]), Pos ((0, 248, 0), [_])), [, _), 
   6.265 +Token ((Pos ((0, 248, 250), [_]), Pos ((0, 250, 0), [_])), "", _), 
   6.266 +Token ((Pos ((0, 250, 251), [_]), Pos ((0, 251, 0), [_])), ,, _), 
   6.267 +Token ((Pos ((0, 252, 254), [_]), Pos ((0, 254, 0), [_])), "", _), 
   6.268 +Token ((Pos ((0, 254, 255), [_]), Pos ((0, 255, 0), [_])), ], _), 
   6.269 +Token ((Pos ((0, 296, 304), [_]), Pos ((0, 304, 0), [_])), Solution, _), 
   6.270 +Token ((Pos ((0, 304, 305), [_]), Pos ((0, 305, 0), [_])), :, _) 
   6.271 +Outer syntax error: command expected,
   6.272 +but keyword References was found
   6.273 +\<close>
   6.274 +subsubsection \<open>on References: == on Relate: == ...\<close>
   6.275 +
   6.276 +
   6.277 +subsection \<open><Output> BY CLICK ON Problem..Solution: session Isac\<close>
   6.278 +subsubsection \<open>(1)AFTER session Isac (after ./zcoding-to-test.sh)\<close>
   6.279  text \<open>
   6.280    Comparison of the two subsections below:
   6.281  (1) <Output> AFTER session Isac (after ./zcoding-to-test.sh) WITH click on Problem..Specification:
   6.282 @@ -366,5 +563,5 @@
   6.283      Bad context for command "end"\<^here> -- using reset state 
   6.284      Found the end of the theory, but the last SPARK environment is still open.
   6.285  "(2) outcomment before creating session Isac" ABOVE OTHERWISE YOU HAVE..
   6.286 -  ERROR: 
   6.287 +  ERROR:                         
   6.288      Bad context for command "end"\<^here> -- using reset state*)

     7.1 --- a/src/Tools/isac/BridgeJEdit/parseC.sml	Wed Feb 17 15:43:34 2021 +0100
     7.2 +++ b/src/Tools/isac/BridgeJEdit/parseC.sml	Fri Feb 26 13:13:03 2021 +0100
     7.3 @@ -13,7 +13,7 @@
     7.4    val problem_headline: problem_headline parser
     7.5  
     7.6  (* exclude "Problem" from parsing * )
     7.7 -  val read_out_headline: headline_string * Token.T list -> ThyC.id * Problem.id
     7.8 +  val read_out_headline: headline_string * Token.src -> ThyC.id * Problem.id
     7.9  ( * exclude "Problem" from parsing *)
    7.10    val read_out_headline: problem_headline -> ThyC.id * Problem.id
    7.11  (* exclude "Problem" from parsing *)
    7.12 @@ -31,9 +31,9 @@
    7.13    val formalisation: Fdl_Lexer.T list -> form_model_refs * Fdl_Lexer.T list;
    7.14  
    7.15  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    7.16 -  val tokenize: string -> Token.T list
    7.17 -  val string_of_toks: Token.T list -> string
    7.18 -  val parse: (Token.T list -> 'a * Token.T list) -> Token.T list -> 'a * Token.T list
    7.19 +  val tokenize: string -> Token.src
    7.20 +  val string_of_toks: Token.src -> string
    7.21 +  val parse: (Token.src -> 'a * Token.src) -> Token.src -> 'a * Token.src
    7.22  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    7.23  
    7.24    (*Model*)
    7.25 @@ -59,7 +59,7 @@
    7.26    val exec_rewrite_set_inst: (string * string) * string -> string
    7.27    val exec_substitute: (string * string) * string -> string
    7.28  
    7.29 -  val tactic: Token.T list -> (string * string) * Token.T list
    7.30 +  val tactic: Token.src -> (string * string) * Token.src
    7.31  
    7.32    (*Steps*)
    7.33    val steps: (string * (string * string)) list parser