1.1 --- a/src/Doc/Implementation/Isar.thy Sun Aug 02 12:32:34 2020 +0200
1.2 +++ b/src/Doc/Implementation/Isar.thy Fri Aug 14 12:36:33 2020 +0200
1.3 @@ -148,6 +148,17 @@
1.4 \<^assert> (n = 3);\<close>
1.5 sorry
1.6 end
1.7 +ML \<open>
1.8 +\<close> text \<open>
1.9 +see mail > systems > isabelle > system:
1.10 + Re: [isabelle] Accessing the proof context from ML
1.11 + from Makarius 07/08/20 19:04
1.12 +
1.13 +(#goal @ {Isar.goal})
1.14 +exception UNDEF raised (line 183 of "Isar/toplevel.ML")
1.15 +\<close> ML \<open>
1.16 +\<close> ML \<open>
1.17 +\<close>
1.18
1.19 text \<open>
1.20 Here we see 3 individual subgoals in the same way as regular proof methods
2.1 --- a/src/Tools/isac/BridgeJEdit/Isac.thy Sun Aug 02 12:32:34 2020 +0200
2.2 +++ b/src/Tools/isac/BridgeJEdit/Isac.thy Fri Aug 14 12:36:33 2020 +0200
2.3 @@ -28,7 +28,7 @@
2.4
2.5 (** setup command_keyword ISAC **)
2.6 ML \<open>
2.7 -\<close> ML \<open>
2.8 +\<close> ML \<open> (*try to adapt original from Makarius to problem parser*)
2.9 val _ =
2.10 Outer_Syntax.command @{command_keyword ISAC} "embedded ISAC language"
2.11 (Parse.input ((**)Parse.cartouche (** )--(**) ParseC.problem( **)) >> (fn input =>
3.1 --- a/src/Tools/isac/BridgeJEdit/parseC.sml Sun Aug 02 12:32:34 2020 +0200
3.2 +++ b/src/Tools/isac/BridgeJEdit/parseC.sml Fri Aug 14 12:36:33 2020 +0200
3.3 @@ -10,11 +10,12 @@
3.4 type problem
3.5 val problem: problem parser
3.6
3.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.8 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.9 (*tools*)
3.10 val tokenize: string -> Token.T list
3.11 val string_of_toks: Token.T list -> string
3.12 val parse: (Token.T list -> 'a * Token.T list) -> Token.T list -> 'a * Token.T list
3.13 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.14
3.15 (*Problem headline*)
3.16 type problem_headline
4.1 --- a/src/Tools/isac/TODO.thy Sun Aug 02 12:32:34 2020 +0200
4.2 +++ b/src/Tools/isac/TODO.thy Fri Aug 14 12:36:33 2020 +0200
4.3 @@ -28,7 +28,9 @@
4.4 \begin{itemize}
4.5 \item xxx
4.6 \item xxx
4.7 - \item xxx
4.8 + \item as soon as src/../parseC.sml is stable,
4.9 + remove defs from Test_Parse_Isac.thy
4.10 + + and shift tests from Test_Parse_Isac -> test/../parseC.sml
4.11 \item xxx
4.12 \item Specify.find_next_step: References.select
4.13 cpI = ["vonBelastungZu", "Biegelinien"]: References_Def.id
5.1 --- a/test/Pure/Isar/Keyword_ISAC.thy Sun Aug 02 12:32:34 2020 +0200
5.2 +++ b/test/Pure/Isar/Keyword_ISAC.thy Fri Aug 14 12:36:33 2020 +0200
5.3 @@ -4,7 +4,7 @@
5.4 keywords "ISAC" :: diag
5.5 begin
5.6
5.7 -ML \<open>
5.8 +ML \<open> (* original from Makarius 2018 *)
5.9 val _ =
5.10 Outer_Syntax.command @{command_keyword ISAC} "embedded ISAC language"
5.11 (Parse.input Parse.cartouche >> (fn input =>
5.12 @@ -40,10 +40,9 @@
5.13 Tactic Check_Postcond ["Biegelinien"]
5.14 "y x = -6 * q_0 * L ^ 2 / (-24 * EI) * x ^ 2 + 4 * L * q_0 / (-24 * EI) * x ^ 3 + -1 * q_0 / (-24 * EI) * x ^ 4"
5.15 \<close>
5.16 +
5.17 ML \<open>
5.18 \<close> ML \<open>
5.19 -ML_Lex.read_source: Input.source -> ML_Lex.token Antiquote.antiquote list
5.20 -\<close> ML \<open>
5.21 \<close> ML \<open>
5.22 \<close>
5.23 end
6.1 --- a/test/Pure/Isar/Test_Parse_Isac.thy Sun Aug 02 12:32:34 2020 +0200
6.2 +++ b/test/Pure/Isar/Test_Parse_Isac.thy Fri Aug 14 12:36:33 2020 +0200
6.3 @@ -1,9 +1,9 @@
6.4 theory Test_Parse_Isac
6.5 imports (** ) Pure ( **) Isac.Isac_Knowledge (* required for LibraryC.strs2str *)
6.6 keywords (*see section \<open>Own trials ..\<close>*)
6.7 - (* this has a type and thus is a "major keyword" * )
6.8 + (* this has a type and thus is a "major keyword" *)
6.9 "ISAC" :: diag and
6.10 - ( * the following are without type: "minor keywords" *)
6.11 + (* the following are without type: "minor keywords" *)
6.12 "Problem" (* root-problem + recursively in Solution *)
6.13 "Specification" "Model" "References" "Solution" (* structure only *) and
6.14 "Given" "Find" "Relate" "Where" (* await input of term
6.15 @@ -683,6 +683,28 @@
6.16 \<close>
6.17
6.18 section \<open>Problem\<close>
6.19 +subsection \<open>type problem\<close>
6.20 +ML \<open>
6.21 +type problem =
6.22 + (((((((((string * string) * string) * string) * string list) * string) *
6.23 + ((string * string) *
6.24 + (((((((((((((((string * ((string * string) * string)) * string) * string) * string) * string list) * string) * string) * string list) * string) * string) * string) *
6.25 + string) * string) * string list) *
6.26 + ((string * string) * ((((((((string * string) * string) * string) * string) * string list) * string) * string) * string list)))))
6.27 + * string) * string) * string list);
6.28 +\<close> ML \<open>
6.29 +type cartouche_problem =
6.30 + (string *
6.31 + (((((((((string * string) * string) * string) * string list) * string) *
6.32 + ((string * string) *
6.33 + (((((((((((((((string * ((string * string) * string)) * string) * string) * string) * string list) * string) * string) * string list) * string) * string) * string) *
6.34 + string) * string) * string list) *
6.35 + ((string * string) * ((((((((string * string) * string) * string) * string) * string list) * string) * string) * string list))))) *
6.36 + string) * string) * string list));
6.37 +\<close> ML \<open> (*type cartouche_problem*)
6.38 +type cartouche_problem = string * problem;
6.39 +\<close>
6.40 +
6.41 subsection \<open>whole Problem\<close>
6.42 ML \<open>
6.43 \<close> ML \<open>
6.44 @@ -1183,10 +1205,275 @@
6.45
6.46
6.47 section \<open>Parse Isac cartouche\<close>
6.48 -subsection \<open>xxx\<close>
6.49 +ML \<open>
6.50 +val problem =
6.51 + problem_headline --
6.52 + specification --
6.53 + Parse.$$$ "Solution" -- Parse.$$$ ":" --
6.54 + (*/----- this will become "and steps".. *)
6.55 + (Scan.repeat (
6.56 + ((Parse.term -- (Scan.optional tactic ("", ""))) >> exec_step_term) (** ) ||
6.57 + (problem >> exec_subproblem) ( *exec_* make types equal for both args of ||*)
6.58 + ))
6.59 +\<close> ML \<open> (*original with trials to adapt with problem parser*)
6.60 +val _ =
6.61 + Outer_Syntax.command @{command_keyword ISAC} "embedded ISAC language"
6.62 + (
6.63 + (Parse.input ((**)Parse.cartouche (** )-- (** ) ParseC.( **)problem ( **)))
6.64 + >> (* try variants ^^^^^^^^^^^^^^^ ^^ ^^^^^^^*)
6.65 + (fn input => Toplevel.keep (fn _ => ignore (ML_Lex.read_source input)))
6.66 + )
6.67 +\<close> ML \<open>
6.68 +\<close> text \<open> (* check variants in definition of Outer_Syntax.command: *)
6.69 + Parse.cartouche: eval.of definition OK
6.70 + ParseC.problem: eval.of definition OK
6.71 + Parse.cartouche -- ParseC.problem eval.of definition OK
6.72 + Parse.$$$ "\<open>" -- problem -- "\<close>" eval.of definition OK
6.73 +
6.74 +--------------------------------- but appl.of definition: see subsequent subsection
6.75 +\<close>
6.76 +
6.77 +subsection \<open>minimal ISAC \<open>Problem..\<close>: \<close>
6.78 +text \<open>
6.79 + see definition
6.80 + val _ = Outer_Syntax.command ..with variant (**)Parse.cartouche (** )--..*)
6.81 + ------------- ^^^^^^^^^^^^^^^
6.82 +\<close>
6.83 +ISAC \<open>
6.84 +Problem ("Biegelinie", ["Biegelinien"])
6.85 + Specification:
6.86 + Model :
6.87 + Given: "Traegerlaenge L", "Streckenlast q_0"
6.88 + Where: "q_0 ist_integrierbar_auf {| 0, L |}", "0 < L"
6.89 + Find: "Biegelinie y"
6.90 + Relate: "Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]"
6.91 + References:
6.92 + RTheory: "Biegelinie"
6.93 + RProblem: ["Biegelinien"]
6.94 + RMethod: ["Integrieren", "KonstanteBestimmen2"]
6.95 + Solution:
6.96 +\<close>
6.97 +text \<open>
6.98 + Parse.cartouche:
6.99 + niceley rendered black / red (* thus this variant is CURRENTLY ACTIVATED in definition above*)
6.100 + problem:
6.101 + Outer syntax error: keyword "Problem" expected,
6.102 + but text cartouche was found:
6.103 + Parse.cartouche -- problem:
6.104 + Outer syntax error: keyword "Problem" expected,
6.105 + but end-of-input was found
6.106 + ----->>> cartouche recognised OK, but cartouche changes content text !
6.107 + Parse.$$$ "\<open>" -- problem -- "\<close>"
6.108 + Outer syntax error: keyword "\<open>" expected,
6.109 + but text cartouche was found: "\<close>"
6.110 +\<close> ML \<open>
6.111 +\<close>
6.112 +
6.113 +subsection \<open>How are "\<open>" "\<close>" handled in Naproche .. Parse.embedded_position INSIGHT AT END\<close>
6.114 +text \<open>
6.115 + see /usr/local/Isabelle_Naproche-20190611/contrib/naproche-20190418/Isabelle/Test_WN.thy
6.116 + conclusion:
6.117 +********************************************************************************
6.118 +* check_forthel just sends to server, so tokens DO NOT COME FROM some ML code *
6.119 +********************************************************************************
6.120 +\<close> ML \<open>
6.121 +\<close> ML \<open> (* compare Parse.cartouche .. Parse.embedded (latter found in Isabelle_Naproche)*)
6.122 +Parse.cartouche (tokenize ("\<open>" ^ problem_headline_str ^ "\<close>"))
6.123 +(* = ("Problem ( \"Biegelinie\" , [\"Biegelinien\"] )", [])*)
6.124 +\<close> ML \<open>
6.125 +Parse.embedded (tokenize ("\<open>" ^ problem_headline_str ^ "\<close>"))
6.126 +(* = ("Problem ( \"Biegelinie\" , [\"Biegelinien\"] )", [])*)
6.127 +\<close> ML \<open>
6.128 +parse problem_headline (tokenize problem_headline_str );
6.129 +\<close> text \<open> (* but all these create
6.130 +exception MORE () raised (line 159 of "General/scan.ML")*)..
6.131 +
6.132 +parse problem_headline (tokenize ("\<open>" ^ problem_headline_str ^ "\<close>"));
6.133 +parse (Parse.embedded -- problem) (tokenize ("\<open>" ^ problem_headline_str ^ "\<close>"));
6.134 +
6.135 +\<close> text \<open> (*as well a Parse.cartouche by Makarius*)..
6.136 +parse (Parse.cartouche -- problem) (tokenize ("\<open>" ^ problem_headline_str ^ "\<close>"));
6.137 +\<close> ML \<open>
6.138 +\<close> ML \<open> (*this drops "\<open>" "\<close>", found in Naproche/naproche.ML*)
6.139 +Parse.embedded_input: Input.source parser
6.140 +\<close> ML \<open> (*BUT Outer_Syntax.command REQUIRES ..*)
6.141 +Parse.cartouche: string parser
6.142 +\<close> ML \<open> (* ..AND THERE IS NO OPORTUNITY FOR "problem parser"*)
6.143 +problem: problem parser
6.144 +\<close> ML \<open>
6.145 +\<close> ML \<open>
6.146 +\<close> ML \<open>
6.147 +\<close> ML \<open>
6.148 +\<close>
6.149 +
6.150 +subsection \<open>How are "\<open>" "\<close>" handled in Parse.cartouche .. ML_Lex.read_source above NO SUCCESS\<close>
6.151 ML \<open>
6.152 \<close> ML \<open>
6.153 +\<close> ML \<open>
6.154 +\<close> ML \<open> (* Parse.cartouche in Pure/Isar/parse.ML*)
6.155 +fun RESET_VALUE atom = (*required for all primitive parsers*)
6.156 + Scan.ahead (Scan.one (K true)) -- atom >> (fn (arg, x) => (Token.assign NONE arg; x));
6.157 +\<close> ML \<open>
6.158 +fun kind k =
6.159 + Parse.group (fn () => Token.str_of_kind k)
6.160 + (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of));
6.161 +\<close> ML \<open>
6.162 +val cartouche = kind Token.Cartouche;
6.163 + cartouche: Token.T list -> string * Token.T list;
6.164 + cartouche: string parser
6.165 +\<close> ML \<open>
6.166 +\<close> ML \<open>
6.167 +\<close> ML \<open> (* Pure/Isar/token.ML*)
6.168 +val err_prefix = "Outer lexical error: ";
6.169 +
6.170 +val scan_cartouche =
6.171 + Symbol_Pos.scan_pos --
6.172 + ((Symbol_Pos.scan_cartouche err_prefix >> Symbol_Pos.cartouche_content) -- Symbol_Pos.scan_pos);
6.173 +\<close> ML \<open>
6.174 +\<close> ML \<open> (*prep. read_cartouche*)
6.175 +Token.init_assignable Token.eof
6.176 +(* = Token (("", ({}, {})), (EOF, ""), Assignable (ref NONE)): Token.T*)
6.177 +\<close> ML \<open>
6.178 +fun token_range k (pos1, (ss, pos2)) =
6.179 +(*Token (Symbol_Pos.implode_range (pos1, pos2) ss, (k, Symbol_Pos.content ss), Slot);*)
6.180 +(*dummy..*)Token.init_assignable Token.eof
6.181 +\<close> ML \<open>
6.182 +Symbol_Pos.content: Symbol_Pos.T list -> string
6.183 +\<close> ML \<open>
6.184 +fun read_cartouche syms =
6.185 + (case Scan.read Symbol_Pos.stopper (scan_cartouche >> token_range Token.Cartouche) syms of
6.186 + SOME tok => tok
6.187 + | NONE => error ("Single cartouche expected" ^ Position.here (#1 (Symbol_Pos.range syms))));
6.188 +\<close> ML \<open>
6.189 +\<close> ML \<open>
6.190 +\<close>
6.191 +
6.192 +subsection \<open>COMPARE Outer_Syntax.command..ISAC WITH Outer_Syntax.local_theory..Naproche\<close>
6.193 +subsubsection \<open>decompose Outer_Syntax.command @ {command_keyword ISAC}\<close>
6.194 +ML \<open>
6.195 +\<close> ML \<open> (*3rd arg of Outer_Syntax.command vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
6.196 +Outer_Syntax.command :
6.197 +Outer_Syntax.command_keyword -> string -> (Toplevel.transition -> Toplevel.transition) parser -> unit
6.198 +\<close> ML \<open>
6.199 +(
6.200 + (Parse.input ((**)Parse.cartouche (** )-- (** ) ParseC.( **)problem ( **)))
6.201 + >> (* try variants ^^^^^^^^^^^^^^^ ^^ ^^^^^^^*)
6.202 + (fn input => Toplevel.keep (fn _ => ignore (ML_Lex.read_source input)))
6.203 + ):
6.204 + Token.T list -> (Toplevel.transition -> Toplevel.transition) * Token.T list
6.205 +(*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
6.206 +\<close> ML \<open> (*decompose 3rd arg of >>*)
6.207 +(* 1st arg 2nd arg result
6.208 + /-------------\ /--------\ /-----------\*)
6.209 +op >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c;
6.210 +\<close> ML \<open>
6.211 +\<close> ML \<open> (*-- 1st arg instantiates types*)
6.212 +Parse.input Parse.cartouche: Token.T list -> Input.source * Token.T list;
6.213 +Parse.input Parse.cartouche: Input.source parser;
6.214 +\<close> ML \<open>
6.215 +op >> : (Token.T list -> 'b * 'c) * ('b -> 'd) -> Token.T list -> 'd * 'c;
6.216 +op >> : (Token.T list -> Input.source * 'c) * (Input.source -> 'd) -> Token.T list -> 'd * 'c;
6.217 +op >> : (Token.T list -> Input.source * Token.T list) * (Input.source -> 'd) -> Token.T list -> 'd * Token.T list;
6.218 +\<close> ML \<open>
6.219 +\<close> ML \<open> (*-- 2nd arg instantiates types*)
6.220 +(fn input => Toplevel.keep (fn _ => ignore (ML_Lex.read_source input))):
6.221 + Input.source -> Toplevel.transition -> Toplevel.transition
6.222 +\<close> ML \<open>
6.223 +op >> : (Token.T list -> Input.source * Token.T list) * (Input.source -> 'd) ->
6.224 + Token.T list -> 'd * Token.T list;
6.225 +op >> : (Token.T list -> Input.source * Token.T list) * (Input.source -> (Toplevel.transition -> Toplevel.transition)) ->
6.226 + Token.T list -> (Toplevel.transition -> Toplevel.transition) * Token.T list;
6.227 +op >> : ( Input.source parser ) * (Input.source -> (Toplevel.transition -> Toplevel.transition)) ->
6.228 + (Toplevel.transition -> Toplevel.transition) parser;
6.229 +(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
6.230 +\<close> ML \<open>
6.231 +\<close> ML \<open> (*check with sig.of Outer_Syntax.command*)
6.232 +Outer_Syntax.command :
6.233 +Outer_Syntax.command_keyword -> string -> (Toplevel.transition -> Toplevel.transition) parser -> unit
6.234 +(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
6.235 +\<close> ML \<open>
6.236 \<close>
6.237 +
6.238 +subsubsection \<open>decompose Outer_Syntax.command @ {command_keyword ISAC}\<close>
6.239 +ML \<open>
6.240 +\<close> ML \<open> (*3rd arg of Outer_Syntax.command vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
6.241 +Outer_Syntax.local_theory:
6.242 +Outer_Syntax.command_keyword -> string -> (local_theory -> local_theory) parser -> unit
6.243 +\<close> ML \<open>
6.244 +\<close> ML \<open> (*dummy definition for check_forthel*)
6.245 +fun check_forthel (_: Proof.context) (_: string, _: Position.T) = ();
6.246 +\<close> ML \<open>
6.247 +(Parse.embedded_position >> (fn inp => fn lthy => (check_forthel lthy inp; lthy))):
6.248 + Token.T list -> (Proof.context -> Proof.context) * Token.T list
6.249 +(*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
6.250 +\<close> ML \<open> (*decompose 3rd arg of >>*)
6.251 +(* 1st arg 2nd arg result
6.252 + /-------------\ /--------\ /-----------\*)
6.253 +op >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c;
6.254 +\<close> ML \<open>
6.255 +\<close> ML \<open> (*-- 1st arg instantiates types*)
6.256 +Parse.embedded_position: Token.T list -> (string * Position.T) * Token.T list;
6.257 +Parse.embedded_position: (string * Position.T) parser;
6.258 +\<close> ML \<open>
6.259 +op >> : (Token.T list -> 'b * 'c) * ('b -> 'd) -> Token.T list -> 'd * 'c;
6.260 +op >> : (Token.T list -> (string * Position.T) * 'c) * ((string * Position.T) -> 'd) -> Token.T list -> 'd * 'c;
6.261 +op >> : (Token.T list -> (string * Position.T) * Token.T list) * ((string * Position.T) -> 'd) -> Token.T list -> 'd * Token.T list;
6.262 +\<close> ML \<open>
6.263 +\<close> ML \<open> (*-- 2nd arg instantiates types*)
6.264 +(fn inp => fn lthy => (check_forthel lthy inp; lthy)):
6.265 + string * Position.T -> Proof.context -> Proof.context
6.266 +\<close> ML \<open>
6.267 +op >> : (Token.T list -> (string * Position.T) * Token.T list) * ((string * Position.T) -> 'd) ->
6.268 + Token.T list -> 'd * Token.T list; (*\--------- 2nd arg ---------/*)
6.269 +op >> : (Token.T list -> (string * Position.T) * Token.T list) * ((string * Position.T) -> (Proof.context -> Proof.context)) ->
6.270 + Token.T list -> (Proof.context -> Proof.context) * Token.T list;
6.271 +op >> : ( (string * Position.T) parser ) * ((string * Position.T) -> (Proof.context -> Proof.context)) ->
6.272 + (Proof.context -> Proof.context) parser;
6.273 +(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
6.274 +\<close> ML \<open>
6.275 +\<close> ML \<open> (*check with sig.of Outer_Syntax.local_theory*)
6.276 +Outer_Syntax.local_theory:
6.277 + Outer_Syntax.command_keyword -> string -> (Proof.context -> Proof.context) parser -> unit;
6.278 +Outer_Syntax.local_theory:
6.279 + Outer_Syntax.command_keyword -> string -> (local_theory -> local_theory ) parser -> unit;
6.280 +(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
6.281 +\<close> ML \<open>
6.282 +\<close>
6.283 +
6.284 +subsubsection \<open>trial on problem parser in Outer_Syntax.command @ {command_keyword ISAC} FAILED\<close>
6.285 +ML \<open>
6.286 +\<close> ML \<open>
6.287 +(Parse.input ((**)Parse.cartouche (** )-- (** ) ParseC.( **)problem ( **))): Input.source parser;
6.288 +(Parse.input ((**)Parse.cartouche (**) -- (** ) ParseC.( **)problem (**))): Input.source parser;
6.289 +\<close> ML \<open>
6.290 +Parse.input: 'a parser -> Input.source parser
6.291 +\<close> ML \<open>
6.292 +((**) Parse.cartouche (** )-- (** ) ParseC.( **)problem ( **))
6.293 + : string parser;
6.294 +((**) Parse.cartouche (** )-- (** ) ParseC.( **)problem ( **))
6.295 + : Token.T list -> string * Token.T list;
6.296 +((** )Parse.cartouche (**) -- (**) ParseC.( **)problem (**))
6.297 + : Token.T list -> problem * Token.T list;
6.298 +((**) Parse.cartouche (**) -- (** ) ParseC.( **)problem (**))
6.299 + : Token.T list -> cartouche_problem * Token.T list;
6.300 +\<close> ML \<open>
6.301 +\<close> ML \<open>
6.302 +op >> : (Token.T list -> 'b * 'c) * ('b -> 'd) -> Token.T list -> 'd * 'c;
6.303 +op >> : (Token.T list -> problem * 'c) * (problem -> 'd) -> Token.T list -> 'd * 'c;
6.304 +op >> : (Token.T list -> problem * Token.T list) * (problem -> 'd) -> Token.T list -> 'd * Token.T list;
6.305 +\<close> ML \<open>
6.306 +\<close> ML \<open> (*----------------- 2nd arg *)
6.307 +(fn input => Toplevel.keep (fn _ => ignore (ML_Lex.read_source input)))
6.308 + : Input.source -> (Toplevel.transition -> Toplevel.transition);
6.309 +\<close> ML \<open>
6.310 +(* 1st arg 2nd arg result
6.311 + /--------------------------------------\ /-------------\ /-------------------------------\*)
6.312 +op >> : (Token.T list -> problem * Token.T list) * (problem -> 'd) -> Token.T list -> 'd * Token.T list;
6.313 +op >> : (Token.T list -> problem * Token.T list) * (problem -> 'd) -> Token.T list -> 'd * Token.T list;
6.314 +\<close> ML \<open> (* there is someth.wrong with 1st arg ^^^^^^^*)
6.315 +\<close> ML \<open>
6.316 +\<close>
6.317 +
6.318 subsubsection \<open>xxx\<close>
6.319 ML \<open>
6.320 \<close> ML \<open>