1.1 --- a/test/Pure/Isar/Keywords_Diag.thy Thu Jul 02 09:57:58 2020 +0200
1.2 +++ b/test/Pure/Isar/Keywords_Diag.thy Fri Jul 17 11:42:20 2020 +0200
1.3 @@ -10,16 +10,16 @@
1.4 subsection \<open>definitions for keywords\<close>
1.5
1.6 theory Keywords_Diag
1.7 -imports Pure
1.8 +imports Isac.Isac_Knowledge (*Pure: not for Problem Biegelinie*)
1.9 keywords
1.10 (* this has a type and thus is a "major keyword" *)
1.11 "ISAC" :: diag and
1.12 (* the following are without type: "minor keywords" *)
1.13 - "Problem" (* await input of (string * string list) *)and
1.14 + "Problem" (* root-problem + recursively in Solution *)
1.15 "Specification" "Model" "References" "Solution" (* structure only *) and
1.16 "Given" "Find" "Relate" "Where" (* await input of term *) and
1.17 - "Theory" (* await input of string *) and
1.18 - "Problem" "Method" (* await input of string list *) and
1.19 + "RTheory" (* await input of string; "R" distingues "Problem".."RProblem" *) and
1.20 + "RProblem" "RMethod" (* await input of string list *) and
1.21 "Tactic" (* optionally repeated with each step 0.. end of calculation *)
1.22 begin
1.23
1.24 @@ -34,6 +34,10 @@
1.25 : Token.T list -> (Toplevel.transition -> Toplevel.transition) * Token.T list;
1.26 (*---------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ value of >> *)
1.27 \<close> ML \<open>
1.28 +op >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c (* args -------vvv-- 1st -- 2nd*)
1.29 +(* ('a parser : T list -> 'a * T list
1.30 + * (Input.source -> (Toplevel.transition -> Toplevel.transition))*)
1.31 +\<close> ML \<open>
1.32 (Parse.input Parse.cartouche) : Input.source parser;
1.33 (*-----------------------------^^^^^^^^^^^^^^^^^^^^^----------------------------- 1st arg of >> *)
1.34 \<close> ML \<open>
1.35 @@ -44,7 +48,7 @@
1.36 \<close> ML \<open> (*decompose and investigate 1st arg..------------------------------------------------- *)
1.37 Parse.input : 'a parser -> Input.source parser;
1.38 Parse.cartouche : string parser
1.39 -;
1.40 +\<close> ML \<open>
1.41 val input = Input.string "123"
1.42 (* = Source {delimited = true, range = ({}, {}), text = "123"}*)
1.43 : Input.source;
1.44 @@ -95,9 +99,30 @@
1.45 (*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ 1st arg of >> *)
1.46 \<close> ML \<open>
1.47 Parse.input : 'a parser -> Input.source parser;
1.48 -\<close> ML \<open>
1.49 Parse.cartouche : string parser
1.50 (*\\------------------------------------------------------------------------------------------//*)
1.51 +\<close> ML \<open>
1.52 +\<close>
1.53 +
1.54 +subsubsection \<open>tokenise input"\<close>
1.55 +ML \<open>
1.56 +\<close> ML \<open>
1.57 + Outer_Syntax.command @{command_keyword TEST_SIGNAT} "investigate signatures involveD"
1.58 + ((Parse.input Parse.cartouche) >> (fn input =>
1.59 + Toplevel.keep (fn _ => ignore (ML_Lex.read_source input) ) ) ) : unit
1.60 +\<close> ML \<open>
1.61 +ML_Lex.read_source: Input.source -> (ML_Lex.token Antiquote.antiquote) list
1.62 +\<close> ML \<open>
1.63 +Source.source:
1.64 + 'a Scan.stopper ->
1.65 + ('a list -> 'b list * 'a list) ->
1.66 + ('a, 'c) Source.source -> ('b, ('a, 'c) Source.source) Source.source
1.67 +\<close> ML \<open>
1.68 +\<close> ML \<open>
1.69 +\<close> ML \<open>
1.70 +K
1.71 +\<close> ML \<open>
1.72 +\<close> ML \<open>
1.73 \<close>
1.74
1.75 subsection \<open>stepwise incrementing the parser\<close>
1.76 @@ -107,23 +132,7 @@
1.77 "Outer_Syntax.command @ {command_keyword xxx}" is allowed only once in a theory,
1.78 so outcomment accordingly !
1.79 \<close>
1.80 -subsubsection \<open>step 0: provide functions such that \<close>
1.81 -ML \<open>
1.82 -val ISAC_parser = Parse.cartouche
1.83 -\<close> ML \<open>
1.84 -val check_ISAC : (Token.T list -> Input.source * Token.T list) = fn input =>
1.85 - let
1.86 - val toks = Parse.input ISAC_parser input
1.87 - val _ (*just check if input is according to ..*) = ISAC_parser
1.88 - in toks end
1.89 -\<close> ML \<open>
1.90 -val _ =
1.91 - Outer_Syntax.command @{command_keyword ISAC}
1.92 - "parsing stepwise incremented by check_ISAC"
1.93 - (check_ISAC >> (fn input => Toplevel.keep (fn _ => ignore (ML_Lex.read_source input))))
1.94 -\<close> ML \<open>
1.95 -\<close>
1.96 -subsubsection \<open>step 1: "Problem Specification Model -- STOPPED HERE"\<close>
1.97 +subsubsection \<open>step -1: investigate signatures "Problem Specification Model -- STOPPED HERE"\<close>
1.98 ML \<open>
1.99 \<close> ML \<open>
1.100 Parse.input : 'a parser -> Input.source parser;
1.101 @@ -154,39 +163,142 @@
1.102 *)
1.103 \<close> ML \<open>
1.104 \<close>
1.105 +subsubsection \<open>step 0: provide a structure for steps\<close>
1.106 +ML \<open>
1.107 +val ISAC_parser = Parse.cartouche;
1.108 +ISAC_parser: string parser
1.109 +\<close> ML \<open>
1.110 +val check_ISAC : (Token.T list -> Input.source * Token.T list) = fn input =>
1.111 + let
1.112 + val toks = Parse.input ISAC_parser input
1.113 + val _ (*just check if input is according to ..*) = ISAC_parser
1.114 + in toks end
1.115 +\<close> text \<open> (*ML -> Duplicate outer syntax command "ISAC" *)
1.116 +val _ = (*-------------v--------------------*)
1.117 + Outer_Syntax.command @ {command_keyword ISAC} "parsing stepwise incremented by check_ISAC"
1.118 + (check_ISAC >> (fn input => Toplevel.keep (fn _ => ignore (ML_Lex.read_source input))))
1.119 +\<close> ML \<open>
1.120 +\<close>
1.121
1.122 -subsection \<open>Makarius' hint on rendering ISAC calculation\<close>
1.123 -subsubsection \<open>ISAC command definition, original by Makarius\<close>
1.124 -(*//------- outcommented during stepwise incrementing the parser ----------------------------* )
1.125 +subsubsection \<open>step 1: Problem ("Biegelinie", ["Biegelinien"]) etc\<close>
1.126 +text \<open>
1.127 + we have {term "Problem (''Biegelinie'', [''Biegelinien''])"} !!!
1.128 + !!! as formula + as Tactic
1.129 +\<close>
1.130 ML \<open>
1.131 -val _ =
1.132 - Outer_Syntax.command @{command_keyword ISAC}
1.133 - "embedded ISAC language" (* an initial hint by Makarius *)
1.134 - (Parse.input Parse.cartouche >>
1.135 - (fn input => Toplevel.keep (fn _ => ignore (ML_Lex.read_source input))))
1.136 -\<close>
1.137 -( *--------- outcommented during stepwise incrementing the parser --------------------------//*)
1.138 +val str = "Problem (''Biegelinie'', [''Biegelinien''])"
1.139 +val t = @{term "Problem (''Biegelinie'', [''Biegelinien''])"}
1.140 +\<close> ML \<open>
1.141 +val input = Input.string str
1.142 +\<close> ML \<open>
1.143 +val toks = ML_Lex.read_source input;
1.144 +\<close> ML \<open>
1.145 +toks: ML_Lex.token Antiquote.antiquote list
1.146 +\<close> ML \<open>
1.147 +length toks = 11;
1.148 +nth 1 toks (* = Text (Token (({}, {}), (Ident, "Problem"))) <--------- (Keyword, "Problem") *);
1.149 +nth 2 toks (* = Text (Token (({}, {}), (Space, " ")))*);
1.150 +nth 3 toks (* = Text (Token (({}, {}), (Keyword, "(")))*);
1.151 +nth 4 toks (*Text (Token (({}, {}), (Type_Var, "''Biegelinie''"))) <---------- Type_Var !?!?*);
1.152 +nth 10 toks (* = Text (Token (({}, {}), (Keyword, ")")))*);
1.153 +\<close> ML \<open>
1.154 +ignore (ML_Lex.read_source input) : unit;
1.155 +\<close> ML \<open>
1.156 +\<close> ML \<open>
1.157 +\<close> ML \<open>
1.158 +val str = "a=b";
1.159 +val input = Input.string str
1.160 +val toks = ML_Lex.read_source (*true*) input;
1.161 +nth 2 toks (* = Text (Token (({}, {}), (Keyword, "="))) ----------^^^ (Keyword, "Problem") *);
1.162 +\<close> ML \<open>
1.163 +\<close>
1.164
1.165 -subsubsection \<open>complete ISAC calculation\<close>
1.166 -ISAC \<open>
1.167 -Problem ("Biegelinie", ["Biegelinien"])
1.168 - Specification:
1.169 - Model:
1.170 +subsubsection \<open>step 2: Model\<close>
1.171 +ML \<open>
1.172 +\<close> ML \<open>
1.173 +val ISAC_parser = Parse.cartouche;
1.174 +ISAC_parser: string parser
1.175 +\<close> ML \<open>
1.176 +val parse_Model = Parse.reserved "Model" --
1.177 + Parse.reserved "Given" -- Parse.list (Parse.term) --
1.178 + Parse.reserved "Where" -- Parse.list (Parse.term) --
1.179 + Parse.reserved "Find" -- Parse.term --
1.180 + Parse.reserved "Relate" -- Parse.list (Parse.term)
1.181 +\<close> ML \<open>
1.182 +parse_Model: Token.T list ->
1.183 + ((((((((string * string) * string list) * string) * string list) * string) * string) * string) * string list) * Token.T list
1.184 +\<close> ML \<open> (*/---------- -> ERROR text cartouche was found ----------\*)
1.185 +val ISAC_parser = (*a* ) parse_Model -- Parse.cartouche ( *a*)
1.186 + (*b*) Parse.cartouche -- parse_Model (*b*)
1.187 +\<close> ML \<open>
1.188 +val check_ISAC : (Token.T list -> Input.source * Token.T list) = fn input =>
1.189 + let
1.190 + val toks = Parse.input ISAC_parser input
1.191 + val _ (*just check if input is according to ..*) = ISAC_parser
1.192 + in toks end
1.193 +\<close> ML \<open> (*ML -> Duplicate outer syntax command "ISAC" *)
1.194 +val _ = (*-------------v--------------------*)
1.195 + Outer_Syntax.command @{command_keyword ISAC} "parsing stepwise incremented by check_ISAC"
1.196 + (check_ISAC >> (fn input => Toplevel.keep (fn _ => ignore (ML_Lex.read_source input))))
1.197 +\<close> ML \<open>
1.198 +\<close>
1.199 +(*/----- with above check_ISAC + ISAC_parser (*a*) | (*b*)*)
1.200 +ISAC \<open>Model:
1.201 Given: "Traegerlaenge L", "Streckenlast q_0"
1.202 Where: "q_0 ist_integrierbar_auf {| 0, L |}", "0 < L"
1.203 Find: "Biegelinie y"
1.204 Relate: "Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]"
1.205 +\<close>
1.206 +(* ----- ERROR (*a*) | (*b*): * )
1.207 +(*a*) Outer syntax error: reserved identifier "Model" expected,
1.208 +but text cartouche was found:
1.209 +\<open>Model: ...
1.210 +
1.211 +(*b*) Outer syntax error\<^here>: reserved identifier "Model" expected,
1.212 +but end-of-input\<^here> was found
1.213 +( *\---------- -> ERROR text cartouche was found ----------/*)
1.214 +
1.215 +
1.216 +subsection \<open>Makarius' hint on rendering ISAC calculation\<close>
1.217 +text \<open>
1.218 + ISAC command definition, original by Makarius
1.219 +/--- outcommented during stepwise incrementing the parser ----------------------------\
1.220 +
1.221 +keywords "ISAC" :: diag
1.222 +
1.223 +ML \<open>
1.224 +val _ =
1.225 + Outer_Syntax.command @ {command_keyword ISAC}
1.226 + "embedded ISAC language" (* an initial hint by Makarius *)
1.227 + (Parse.input Parse.cartouche >>
1.228 + (fn input => Toplevel.keep (fn _ => ignore (ML_Lex.read_source input))))
1.229 +\<close>
1.230 +\--- outcommented during stepwise incrementing the parser ----------------------------/
1.231 +\<close>
1.232 +subsection \<open>complete ISAC calculation\<close>
1.233 +(*/--- outcomment during stepwise incrementing the parser ----------------------------\*)
1.234 +ISAC \<open>
1.235 +"Problem ("Biegelinie", ["Biegelinien"])"
1.236 + Specification:
1.237 + Model:
1.238 + Given: ["Traegerlaenge L", "Streckenlast q_0"]
1.239 + Where: ["q_0 ist_integrierbar_auf {| 0, L |}", "0 < L"]
1.240 + Find: "Biegelinie y"
1.241 + Relate: ["Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]"]
1.242 References:
1.243 - Theory: "Biegelinie"
1.244 - Problem: ["Biegelinien"]
1.245 - Method: ["Integrieren", "KonstanteBestimmen2"]
1.246 + RTheory: "Biegelinie"
1.247 + RProblem: ["Biegelinien"]
1.248 + RMethod: ["Integrieren", "KonstanteBestimmen2"]
1.249 Solution:
1.250 - Problem ("Biegelinie", ["vonBelastungZu", "Biegelinien"])
1.251 + "Problem ("Biegelinie", ["vonBelastungZu", "Biegelinien"])"
1.252 "[Q x = c + -1 * q_0 * x, M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^ 2, y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^ 2 + -1 * q_0 / 6 * x ^ 3), y x = c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^ 2 + c / 6 * x ^ 3 + -1 * q_0 / 24 * x ^ 4)]"
1.253 - Problem ("Biegelinie", ["setzeRandbedingungen", "Biegelinien"])
1.254 +
1.255 + "Problem ("Biegelinie", ["setzeRandbedingungen", "Biegelinien"])"
1.256 "[L * q_0 = c, 0 = (2 * c_2 + 2 * L * c + -1 * L ^ 2 * q_0) / 2, 0 = c_4, 0 = c_3]"
1.257 +
1.258 "solveSystem [L * q_0 = c, 0 = (2 * c_2 + 2 * L * c + -1 * L ^ 2 * q_0) / 2, 0 = c_4, 0 = c_3] [c, c_1, c_2, c_4]"
1.259 "[c = -1 * L * q_0 / -1, c_2 = -1 * L ^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]"
1.260 +
1.261 "y x = c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^ 2 + c / 6 * x ^ 3 + -1 * q_0 / 24 * x ^ 4)"
1.262 Tactic Substitute "c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^ 2 + c / 6 * x ^ 3 + -1 * q_0 / 24 * x ^ 4)" "[c, c_1, c_2, c_4]"
1.263 "y x = 0 + 0 * x + 1 / (-1 * EI) * (-1 * L ^ 2 * q_0 / 2 / 2 * x ^ 2 + -1 * L * q_0 / -1 / 6 * x ^ 3 + -1 * q_0 / 24 * x ^ 4)"
1.264 @@ -195,4 +307,6 @@
1.265 Tactic Check_Postcond ["Biegelinien"]
1.266 "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"
1.267 \<close>
1.268 +(*\--- outcomment during stepwise incrementing the parser ----------------------------/*)
1.269 +
1.270 end
1.271 \ No newline at end of file
2.1 --- a/test/Pure/Isar/Struct_Deriv.thy Thu Jul 02 09:57:58 2020 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,477 +0,0 @@
2.4 -(*
2.5 -$ cd /usr/local/isabisac/src/Pure/isac/smltest/Pure/Isar
2.6 -$ /usr/local/isabisac/bin/isabelle emacs Struct_Deriv.thy &
2.7 -$ /usr/local/isabisac/bin/isabelle jedit Struct_Deriv.thy &
2.8 -*)
2.9 -
2.10 -header \<open>structured derivations (SD) according to R.J.Back\<close>
2.11 -
2.12 -theory Struct_Deriv2
2.13 -imports Main
2.14 -begin
2.15 -text \<open>table of contents
2.16 -1. fun parse for SDs by minimal copy from Isabelle code
2.17 -1.1. keywords and outer syntax preparing parser setup
2.18 -1.1.1. keywords according to src/Pure/Isar/keyword.ML
2.19 -1.1.2. outer syntax according to src/Pure/Isar/outer_syntax.ML
2.20 -1.1.3. parser setup according to src/Pure/Isar/isar_syn.ML
2.21 -1.2. minimalized fun parse by Stefan Berghofer IsaDevWs'10
2.22 -2. provisional parser for SD
2.23 -2.1. parsers for the elements of a calculation
2.24 -2.1.1. named_rule
2.25 -2.1.2. term_rule
2.26 -2.1.3. rule
2.27 -2.1.4. PBLheadline
2.28 -2.1.5. CASheadline
2.29 -2.1.6. headline
2.30 -2.1.7. calcline
2.31 -2.2. combine the parsers for elements to a whole SD-parser
2.32 -2.2.1. provisional SD-parser setup
2.33 -2.2.2. parser applied to example 1
2.34 -2.2.3. parser applied to example 2
2.35 -\<close>
2.36 -
2.37 -section \<open>1. fun parse for SDs by minimal copy from Isabelle code\<close>
2.38 -
2.39 -subsection \<open>1.1. keywords, outer syntax and parser setup\<close>
2.40 -text \<open>this is a minimal copy from respective Isabelle sourcefiles,
2.41 - minimal with respect to the goal to parse simple SDs, see ex1, ex2 below.
2.42 -
2.43 - Actually, the code below has been selected from the function calls at the bottom,
2.44 - up to the initial definitions below.
2.45 -
2.46 - Some functions have been simplified; code is kept as (* original *)
2.47 - Problems arising with the simplifications will teach the reasons for the original source.
2.48 -\<close>
2.49 -
2.50 -subsubsection \<open>1.1.1. keywords according to src/Pure/Isar/keyword.ML\<close>
2.51 -ML \<open>
2.52 -signature KEYWORDC = (*minimal C-copy from KEYWORD*)
2.53 -sig
2.54 - type T
2.55 - val kind_of: T -> string
2.56 - val calc_begin: T
2.57 - val keyword: string -> unit
2.58 - val command: string -> T -> unit
2.59 - val tag_calc: T -> T
2.60 -end;
2.61 -
2.62 -structure KeywordC: KEYWORDC =
2.63 -struct
2.64 -
2.65 -datatype T = KeywordC of string * string list;
2.66 -
2.67 -fun kind s = KeywordC (s, []);
2.68 -fun kind_of (KeywordC (s, _)) = s;
2.69 -
2.70 -val calc_begin = kind "calc-begin";
2.71 -
2.72 -(*
2.73 -fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);
2.74 -fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);
2.75 -fun report_message s =
2.76 - (if print_mode_active keyword_status_reportN then Output.status else writeln) s;*)
2.77 -fun report_message s =
2.78 - (if true (*!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*) then Output.status else writeln) s;
2.79 -fun report_keyword name =
2.80 - report_message (Markup.markup (Markup.keyword_decl name)
2.81 - ("Outer syntax keyword: " ^ quote name));
2.82 -fun report_command (name, kind) =
2.83 - report_message (Markup.markup (Markup.command_decl name (kind_of kind))
2.84 - ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
2.85 -
2.86 -fun keyword name =
2.87 - (apfst (Scan.extend_lexicon (Symbol.explode name));
2.88 - report_keyword name);
2.89 -(* see CRITICAL above
2.90 -fun command name kind =
2.91 - (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
2.92 - change_commands (Symtab.update (name, kind));
2.93 - report_command (name, kind));*)
2.94 -fun command name kind =
2.95 - (apsnd (Scan.extend_lexicon (Symbol.explode name));
2.96 - Symtab.update (name, kind);
2.97 - report_command (name, kind));
2.98 -
2.99 -fun update_tags t ts = t :: remove (op = : string * string -> bool) t ts;
2.100 -fun tag t (KeywordC (s, ts)) = KeywordC (s, update_tags t ts);
2.101 -val tag_calc = tag "calculation"; (* <----------------------------------------*)
2.102 -
2.103 -end;\<close>
2.104 -
2.105 -subsubsection \<open>1.1.2. outer syntax according to src/Pure/Isar/outer_syntax.ML\<close>
2.106 -ML \<open>
2.107 -signature OUTER_SYNTAXC =
2.108 -sig
2.109 - val command: string -> string -> KeywordC.T ->
2.110 - (Toplevel.transition -> Toplevel.transition) parser -> unit
2.111 - val scan: Position.T -> string -> Token.T list
2.112 -end;
2.113 -
2.114 -structure Outer_SyntaxC: OUTER_SYNTAXC =
2.115 -struct
2.116 -
2.117 -datatype command = CommandC of
2.118 - {comment: string,
2.119 - markup: Thy_Output.markup option,
2.120 - int_only: bool,
2.121 - parse: (Toplevel.transition -> Toplevel.transition) parser};
2.122 -
2.123 -fun make_command comment markup int_only parse =
2.124 - CommandC {comment = comment, markup = markup, int_only = int_only, parse = parse};
2.125 -
2.126 -val global_commands = Unsynchronized.ref (Symtab.empty: command Symtab.table);
2.127 -val global_markups = Unsynchronized.ref ([]: (string * Thy_Output.markup) list);
2.128 -
2.129 -fun change_commands f = CRITICAL (fn () =>
2.130 - (Unsynchronized.change global_commands f;
2.131 - global_markups :=
2.132 - Symtab.fold (fn (name, CommandC {markup = SOME m, ...}) => cons (name, m) | _ => I)
2.133 - (! global_commands) []));
2.134 -fun get_commands () = ! global_commands;
2.135 -fun add_command name kind cmd = CRITICAL (fn () =>
2.136 - (KeywordC.command name kind;
2.137 - if not (Symtab.defined (get_commands ()) name) then ()
2.138 - else warning ("Redefining outer syntax command " ^ quote name);
2.139 - change_commands (Symtab.update (name, cmd))));
2.140 -
2.141 -fun command name comment kind parse =
2.142 - add_command name kind (make_command comment NONE false parse);
2.143 -
2.144 -fun scan pos str =
2.145 - Source.of_string str
2.146 - |> Symbol.source (*Isabelle2009-2: {do_recover = false}*)
2.147 - |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
2.148 - |> Source.exhaust;
2.149 -end;
2.150 -\<close>
2.151 -
2.152 -subsubsection \<open>1.1.3. parser setup according to src/Pure/Isar/isar_syn.ML\<close>
2.153 -ML \<open>
2.154 -structure Isac_Syn: sig end =
2.155 -struct
2.156 -
2.157 -val _ = List.app (*contrib/polyml-5.3.0/src/basis/List.sml*) KeywordC.keyword
2.158 - ["(", ")", "[", "]", ",",
2.159 - "=>", "<=",
2.160 - "==", (* simplification without "=" in term *)
2.161 - "equiv", (* equations, etc *)
2.162 - "bullet", (* indicates a subproblem TODO rewrite_set *)
2.163 - "CAS", "Problem", (* "headlines" of subproblems *)
2.164 - "dots", (* end of subproblem TODO of rewrite_set *)
2.165 -(*"bigtriangledown", indicates a rule *)
2.166 - "THM", "MET", (* a ruleconcerning a theorem, a method *)
2.167 - "Calculate", "Rewrite", "Rewrite_Set", "Rewrite_Inst", "Rewrite_Set_Inst",
2.168 - (* rules; TODO?!? Take REFERENCE *)
2.169 - "top", (* term not following from previous term *)
2.170 - "Box" (* qed *)
2.171 - ];
2.172 -
2.173 -val _ =
2.174 - Outer_SyntaxC.command "calculation" "begin calc" (KeywordC.tag_calc KeywordC.calc_begin)
2.175 - (Thy_Header.args >> (fn (name, imports, uses) =>
2.176 - Toplevel.print o
2.177 - Toplevel.init_theory NONE name
2.178 - (fn master =>
2.179 - Thy_Info.toplevel_begin_theory master name imports (map (apfst Path.explode) uses))));
2.180 -(*was in Isabelle2009-2:
2.181 -val _ =
2.182 - Outer_SyntaxC.command "calculation" "begin calc" (KeywordC.tag_calc KeywordC.calc_begin)
2.183 - (Thy_Header.args >> (Toplevel.print oo Isar_Cmd.init_theory));
2.184 -*)
2.185 -end;
2.186 -\<close>
2.187 -
2.188 -subsection \<open>1.2. minimalized fun parse by Stefan Berghofer\<close>
2.189 -text \<open>see ~/devel/IsaDevWS/IsaDevWS-10/T05_Methods.thy by Stefan Berghofer\<close>
2.190 -ML \<open>
2.191 -fun filtered_input str =
2.192 - filter Token.is_proper (Outer_SyntaxC.scan Position.none str);
2.193 -(*################################ fun parse ###############################################*)
2.194 -fun parse p str = Scan.finite Token.stopper p (filtered_input str);
2.195 -(*################################ fun parse ###############################################*)
2.196 -\<close>
2.197 -
2.198 -
2.199 -section \<open>2. provisional parser for SD\<close>
2.200 -subsection \<open>2.1. parsers for the elements of a calculation\<close>
2.201 -
2.202 -subsubsection \<open>2.1.1. named_rule\<close>
2.203 -ML \<open>
2.204 -"---1----------------------------------------";
2.205 -val named_rule' = (Args.$$$ "Calculate" || Args.$$$ "Rewrite" || Args.$$$ "Rewrite_Set"
2.206 - || Args.$$$ "Rewrite_Inst" || Args.$$$ "Rewrite_Set_Inst")
2.207 - -- Args.name;
2.208 -parse named_rule' "Calculate times";
2.209 -(*(("Calculate", "times"), []) : (string * string) * Token.T list*)
2.210 -
2.211 -fun exec2 (nam, rul) =
2.212 - "*** notebook->ML: " ^ nam ^ " " ^ rul
2.213 - |> (fn x => (x, x))
2.214 - |>> writeln
2.215 - |> #2;
2.216 -(*fn : string * string -> string*)
2.217 -val named_rule = named_rule' >> exec2;
2.218 -"---2----------------------------------------";
2.219 -
2.220 -parse named_rule "Calculate times";
2.221 -(*("*** notebook->ML: Calculate times", []) : string * Token.T list*)
2.222 -
2.223 -"---3--- output on top ----------------------";
2.224 -(*** notebook->ML: Calculate times*)
2.225 -\<close>
2.226 -
2.227 -subsubsection \<open>2.1.2. term_rule\<close>
2.228 -ML \<open>
2.229 -"---1----------------------------------------";
2.230 -val term_rule' = Args.$$$ "THM" -- Parse.term;
2.231 -parse term_rule' "THM \"(a+x=b)=(x=-a*b)\" ";
2.232 -(*(("THM", "\^E\^Ftoken\^Ea+x=b = x=-a*b\^E\^F\^E"), []) : (string * string) * Token.T list*)
2.233 -val term_rule = term_rule' >> exec2;
2.234 -"---2----------------------------------------";
2.235 -
2.236 -parse term_rule "THM \"(a+x=b)=(x=-a*b)\" ";
2.237 -(*("*** notebook->ML: THM \^E\^Ftoken\^E(a+x=b)=(x=-a*b)\^E\^F\^E", []) : string * Token.T list*)
2.238 -
2.239 -"---3--- output on top ----------------------";
2.240 -(*** notebook->ML: THM (a+x=b)=(x=-a*b)*)
2.241 -\<close>
2.242 -
2.243 -subsubsection \<open>2.1.3. rule\<close>
2.244 -ML \<open>
2.245 -val rule = named_rule || term_rule;
2.246 -\<close>
2.247 -
2.248 -
2.249 -subsubsection \<open>2.1.4. PBLheadline\<close>
2.250 -ML \<open>
2.251 -"---1----------------------------------------";
2.252 -val PBLheadline' = Args.$$$ "Problem" -- Args.$$$ "(" -- Args.name -- Args.$$$ ","
2.253 - -- (Parse.$$$ "[" |-- Parse.list Parse.name --| Parse.$$$ "]")
2.254 - -- Args.$$$ ")";
2.255 -parse PBLheadline' "Problem (Biegelinie.thy, [Biegelinien])";
2.256 -(*val it = (((((("Problem", "("), "Biegelinie.thy"), ","), ["Biegelinien"]), ")"), [])
2.257 - : (((((string * string) * string) * string) * bstring list) * string) * Token.T list*)
2.258 -
2.259 -fun execN ((((("Problem", "("), thy ), ","), pbl ), ")") =
2.260 - "*** notebook->ML: Problem (" ^ thy ^ ", " ^ ((fn ss => "[" ^ commas ss ^ "]") pbl) ^ ")"
2.261 - |> (fn x => (x, x))
2.262 - |>> writeln
2.263 - |> #2;
2.264 -(*fn : ((((string * string) * string) * string) * string list) * string -> string*)
2.265 -"---2----------------------------------------";
2.266 -execN ((((("Problem", "("), "Biegelinie.thy"), ","), ["Biegelinien"]), ")");
2.267 -(*"*** notebook->ML: Problem (Biegelinie.thy, [Biegelinien])" : string
2.268 - +see top*)
2.269 -
2.270 -val PBLheadline = PBLheadline' >> execN;
2.271 -parse PBLheadline "Problem (Biegelinie.thy, [Biegelinien])";
2.272 -(*("*** notebook->ML: Problem (Biegelinie.thy, [Biegelinien])", []) : string * Token.T list
2.273 - +see top*)
2.274 -parse PBLheadline "Problem (Biegelinie.thy, [setzeRandbedingungen, Biegelinien])";
2.275 -(*("*** notebook->ML: Problem (Biegelinie.thy, [setzeRandbedingungen, Biegelinien])", [])
2.276 - +see top*)
2.277 -
2.278 -"---3--- output on top ----------------------";
2.279 -(** notebook->ML: Problem (Biegelinie.thy, [Biegelinien])
2.280 -*** notebook->ML: Problem (Biegelinie.thy, [Biegelinien])
2.281 -*** notebook->ML: Problem (Biegelinie.thy, [setzeRandbedingungen, Biegelinien])*)
2.282 -\<close>
2.283 -
2.284 -subsubsection \<open>2.1.5. CASheadline\<close>
2.285 -ML \<open>
2.286 -"---1----------------------------------------";
2.287 -val CASheadline' = Args.$$$ "CAS" -- Parse.term;
2.288 -parse CASheadline' "CAS \"solve(x+1=2,x)\"";
2.289 -(*(("CAS", "\^E\^Ftoken\^Esolve(x+1=2,x)\^E\^F\^E"), []) : (string * string) * Token.T list*)
2.290 -
2.291 -fun exec2b ("CAS", trm) =
2.292 - "*** notebook->ML: \"" ^ trm ^ "\""
2.293 - |> (fn x => (x, x))
2.294 - |>> writeln
2.295 - |> #2;
2.296 -(*fn : string * string -> string*)
2.297 -val CASheadline = CASheadline' >> exec2b;
2.298 -"---2----------------------------------------";
2.299 -
2.300 -parse CASheadline "CAS \"solve(x+1=2,x)\"";
2.301 -(*("*** notebook->ML: \^E\^Ftoken\^Esolve(x+1=2,x)\^E\^F\^E", []) : string * Token.T list*)
2.302 -
2.303 -"---3--- output on top ----------------------";
2.304 -(*** notebook->ML: solve(x+1=2,x)*)
2.305 -\<close>
2.306 -
2.307 -subsubsection \<open>2.1.6. headline\<close>
2.308 -ML \<open>
2.309 -val headline = (PBLheadline || CASheadline) -- Scan.option rule;
2.310 -
2.311 -parse headline "Problem (Biegelinie.thy, [setzeRandbedingungen, Biegelinien])";
2.312 -parse headline "CAS \"solve(x+1=2,x)\"";
2.313 -parse headline "CAS \"solve(x+1=2,x)\" Calculate times";
2.314 -parse headline "CAS \"solve(x+1=2,x)\" THM \"(a+x=b)=(x=-a*b)\" ";
2.315 -\<close>
2.316 -
2.317 -subsubsection \<open>2.1.7. calcline\<close>
2.318 -ML \<open>
2.319 -"---1----------------------------------------";
2.320 -val calcline' = Parse.term ;
2.321 -parse calcline' " \"-1 + x = 0\" ";
2.322 -(*("\^E\^Ftoken\^E-1 + x = 0\^E\^F\^E", []) : string * Token.T list*)
2.323 -
2.324 -fun exec1 trm =
2.325 - "*** notebook->ML: \"" ^ trm ^ "\""
2.326 - |> (fn x => (x, x))
2.327 - |>> writeln
2.328 - |> #2;
2.329 -(*fn : string -> string*)
2.330 -val calcline = calcline' >> exec1;
2.331 -"---2----------------------------------------";
2.332 -
2.333 -parse calcline " \"-1 + x = 0\" ";
2.334 -(*("*** notebook->ML: \"\^E\^Ftoken\^E-1 + x = 0\^E\^F\^E\"", []) : string * Token.T list*)
2.335 -
2.336 -"---3--- output on top ----------------------";
2.337 -(*** notebook->ML: "-1 + x = 0"*)
2.338 -\<close>
2.339 -
2.340 -subsection \<open>2.2. combine the parsers for elements to a whole SD-parser\<close>
2.341 -
2.342 -subsubsection \<open>2.2.1. provisional SD-parser setup\<close>
2.343 -text \<open>Prefixes, which are complete enough to trigger a semantic action,
2.344 - have already be handled by exec*.
2.345 - Thus combining such prefixes allows to drop these prefixes.\<close>
2.346 -ML \<open>
2.347 -fun drop_prefixes _ = "DROPPED PREFIXES";
2.348 -\<close>
2.349 -
2.350 -ML \<open>
2.351 -(*val line = headline || calcline; ...this would prevent separation of rewrite_set *)
2.352 -val level_up = Args.$$$ "dots" -- calcline;
2.353 -\<close>
2.354 -
2.355 -ML \<open>(* see IsaDevWS-10/T06_System.thy "recursive parsers" *)
2.356 -fun body _ source =
2.357 - ( Scan.repeat( Args.$$$ "top" -- calcline --
2.358 - (Scan.repeat (Args.$$$ "equiv" -- calcline)) >> drop_prefixes
2.359 -(* FIXME:loops || (Scan.repeat (Args.$$$ "equiv" -- calcline)) >> drop_prefixes *)
2.360 - || Args.$$$ "bullet" -- headline -- body "" >> drop_prefixes
2.361 - )
2.362 - -- level_up
2.363 - ) source;
2.364 -
2.365 -writeln "---0-------";
2.366 -parse (body "") "top \"1+2\" equiv \"3+4\" dots \"5+6\" ";
2.367 -
2.368 -writeln "---1-------";
2.369 -parse (body "") "bullet CAS \"solve(x+1=2,x)\" \
2.370 - \top \"1+2\" equiv \"3+4\" dots \"5+6\" dots \"999\" ";
2.371 -writeln "---2-------";
2.372 -parse (body "") " bullet CAS \"solve (-1 + x = 0, x)\" \n\
2.373 - \ top \"-1 + x = 0\" \n\
2.374 - \ equiv \"[x = 1]\" \n\
2.375 - \ dots \"[x = 1]\" \n\
2.376 - \ dots \"[x = 1]\" ";
2.377 -\<close>
2.378 -
2.379 -ML \<open>
2.380 -(*################################ the parser ##############################################*)
2.381 -val SD = Args.$$$ "calculation" -- Args.$$$ "bullet" -- headline
2.382 - -- (body "")
2.383 - -- (Scan.option (Args.$$$ "Box"));
2.384 -(*################################ the parser ##############################################*)
2.385 -\<close>
2.386 -ML \<open>
2.387 -writeln "---0----------------------------------------";
2.388 -parse SD ("calculation " ^
2.389 - " bullet CAS \"solve(x+1=2,x)\" " ^
2.390 - " dots \"[x = 1]\" ");
2.391 -\<close>
2.392 -ML \<open>
2.393 -writeln "---0----------------------------------------";
2.394 -parse SD "calculation \n\
2.395 - \ bullet CAS \"solve(x+1=2,x)\" \n\
2.396 - \ dots \"[x = 1]\" ";
2.397 -\<close>
2.398 -
2.399 -ML \<open>
2.400 -
2.401 -writeln "---1-----------------------------------------";
2.402 -parse SD "calculation \n\
2.403 - \ bullet CAS \"solve(x+1=2,x)\" \n\
2.404 - \ top \"x + 1 = 2\" \n\
2.405 - \ equiv \"-1 + x = 0\" \n\
2.406 - \ bullet CAS \"solve (-1 + x = 0, x)\" \n\
2.407 - \ top \"-1 + x = 0\" \n\
2.408 - \ equiv \"[x = 1]\" \n\
2.409 - \ dots \"[x = 1]\" \n\
2.410 - \ dots \"[x = 1]\" \n\
2.411 - \ Box ";
2.412 -writeln "---2-----------------------------------------";
2.413 -
2.414 -(* TODO ?!?
2.415 -parse SD "calculation \n\
2.416 - \ bullet CAS \"solve(x+1=2,x)\" \n\
2.417 - \ Calculate times \n\
2.418 - \ top \"x + 1 = 2\" \n\
2.419 - \ equiv \"-1 + x = 0\" \n\
2.420 - \ THM \"(a+x=b)=(x=-a*b)\" \n\
2.421 - \ dots \"[x = 1]\" \n\
2.422 - \ Box ";
2.423 -*)
2.424 -
2.425 -writeln "---3-----------------------------------------";
2.426 -(* GOON: make equiv a viable prefix at this position !
2.427 -parse SD "calculation \n\
2.428 - \ bullet CAS \"solve(x+1=2,x)\" \n\
2.429 - \ bullet CAS \"solve (-1 + x = 0, x)\" \n\
2.430 - \ dots \"[x = 1]\" \n\
2.431 - \ equiv \"-1 + x = 0\" \n\
2.432 - \ dots \"[x = 1]\" \n\
2.433 - \ Box ";
2.434 -*)
2.435 -writeln "---4-----------------------------------------";
2.436 -
2.437 -\<close>
2.438 -
2.439 -
2.440 -subsubsection \<open>2.2.2. parser applied to example 1\<close>
2.441 -ML \<open>
2.442 -val ex1 = "calculation \n\
2.443 - \ bullet CAS \"solve(x+1=2,x)\" \n\
2.444 - \ top \"x + 1 = 2\" \n\
2.445 - \ equiv \"x + 1 - 2 = 0\" \n\
2.446 - \ equiv \"-1 + x = 0\" \n\
2.447 - \ bullet CAS \"solve (-1 + x = 0, x)\" \n\
2.448 - \ top \"-1 + x = 0\" \n\
2.449 - \ equiv \"x = -1 * -1\" \n\
2.450 - \ equiv \"x = 1\" \n\
2.451 - \ equiv \"[x = 1]\" \n\
2.452 - \ dots \"[x = 1]\" \n\
2.453 - \ dots \"[x = 1]\" \n\
2.454 - \ Box ";
2.455 -
2.456 -parse SD ex1;
2.457 -\<close>
2.458 -
2.459 -subsubsection \<open>2.2.3. parser applied to example 2\<close>
2.460 -ML \<open>
2.461 -val ex2 = "calculation \n\
2.462 - \ bullet Problem (Biegelinie.thy, [Biegelinien]) \n\
2.463 - \ bullet Problem (Biegelinie.thy, [vonBelastungZu, Biegelinien]) \n\
2.464 - \ dots \"[Q x = c + -1 * q_0 * x, M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^ 2, \n\
2.465 - \ y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^ 2 + -1 * q_0 / 6 * x ^ 3), \n\
2.466 - \ y x = c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^ 2 + c / 6 * x ^ 3 + -1 * q_0 / 24 * x ^ 4)]\" \n\
2.467 - \ bullet Problem (Biegelinie.thy, [setzeRandbedingungen, Biegelinien]) \n\
2.468 - \ dots \"[L * q_0 = c, 0 = (2 * c_2 + 2 * L * c + -1 * L ^ 2 * q_0) / 2, 0 = c_4, 0 = c_3]\" \n\
2.469 - \ bullet CAS \"solveSystem [0 = c_3] [c_4]\" \n\
2.470 - \ dots \"[c = L * q_0, c_2 = -1 * L ^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]\" \n\
2.471 - \ top \"y x = c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^ 2 + c / 6 * x ^ 3 + -1 * q_0 / 24 * x ^ 4)\" \n\
2.472 - \ equiv \"y x = 0 + 0 * x + 1 / (-1 * EI) * (-1 * L ^ 2 * q_0 / 2 / 2 * x ^ 2 + L * q_0 / 6 * x ^ 3 + -1 * q_0 / 24 * x ^ 4)\"\n\
2.473 - \ equiv \"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\" \n\
2.474 - \ dots \"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\" \n\
2.475 - \ Box";
2.476 -
2.477 -parse SD ex2;
2.478 -\<close>
2.479 -
2.480 -end
2.481 \ No newline at end of file
3.1 --- a/test/Pure/Isar/Test_Parse_Term.thy Thu Jul 02 09:57:58 2020 +0200
3.2 +++ b/test/Pure/Isar/Test_Parse_Term.thy Fri Jul 17 11:42:20 2020 +0200
3.3 @@ -7,17 +7,15 @@
3.4 begin
3.5
3.6 section \<open>parse following Stefan Berghofer at Isabelle Developer Workshop 2010\<close>
3.7 -text (*ML*) \<open>
3.8 +ML \<open>
3.9 fun filtered_input str =
3.10 - filter Token.is_proper (Outer_Syntax.scan Position.none str);
3.11 -... since Isabelle2015: ML error:
3.12 - Value or constructor (scan) has not been declared in structure Outer_Syntax
3.13 + filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) Position.none str)
3.14 fun parse p str = Scan.finite Token.stopper p (filtered_input str);
3.15 \<close>
3.16
3.17 text \<open>should not Parse.term repeat until a non-term token is reached ?
3.18 ######################\" IS REQUIRED \"#######################\<close>
3.19 -text (*ML*) \<open>... since Isabelle2015
3.20 +ML \<open>
3.21 parse Parse.term "\"xxx +++ 111\" end";
3.22 (*val it =
3.23 ("\^E\^Ftoken\^Exxx +++ 111\^E\^F\^E", [Token (("end", ({}, {})), (Command, "end"), Slot)])
3.24 @@ -30,7 +28,7 @@
3.25
3.26 text \<open>Parse.term stops at "Keyword" of outer syntax ?!?
3.27 Should not be parsed according to inner xyntax ?\<close>
3.28 -text (*ML*) \<open>... since Isabelle2015
3.29 +ML \<open>
3.30 parse Parse.term "\"xxx + 111\" end";
3.31 (*val it = ("\^E\^Ftoken\^Exxx + 111\^E\^F\^E", [Token (("end", ({}, {})), (Command, "end"), Slot)])
3.32 : string * Token.T list*)
4.1 --- a/test/Pure/Isar/Test_Parsers.thy Thu Jul 02 09:57:58 2020 +0200
4.2 +++ b/test/Pure/Isar/Test_Parsers.thy Fri Jul 17 11:42:20 2020 +0200
4.3 @@ -1,6 +1,6 @@
4.4 chapter \<open>experiments on scanning and parsing
4.5 following Stefan Berghofers presentation
4.6 - at the Isabelle Developer Workshop 2010
4.7 + at the Isabelle Developer Workshop 2010
4.8 ... broken Isabelle2014-->Isabelle2015, not pursued anymore and thus dropped\<close>
4.9
4.10 theory Test_Parsers
4.11 @@ -10,8 +10,11 @@
4.12 text \<open>parse following Stefan Berghofer at Isabelle Developer Workshop 2010\<close>
4.13 ML \<open>
4.14 fun filtered_input str =
4.15 - filter Token.is_proper (Outer_Syntax.scan Position.none str);
4.16 + filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) Position.none str)
4.17 fun parse p str = Scan.finite Token.stopper p (filtered_input str);
4.18 +\<close> ML \<open>
4.19 +\<close> ML \<open>
4.20 +\<close> ML \<open>
4.21 \<close>
4.22
4.23 section \<open>scanner combinators from src/Pure/General/scan.ML\<close>
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/test/Pure/Isar/Test_Parsers_Cookbook.thy Fri Jul 17 11:42:20 2020 +0200
5.3 @@ -0,0 +1,500 @@
5.4 +theory Test_Parsers_Cookbook
5.5 + imports (** ) Pure ( **) HOL.Complex (*.. for inductive even BELOW*)
5.6 +keywords (*see chapter \<open>Own trials ..\<close>*)
5.7 + (* this has a type and thus is a "major keyword" *)
5.8 + "ISAC" :: diag and
5.9 + (* the following are without type: "minor keywords" *)
5.10 + "Problem" (* root-problem + recursively in Solution *)
5.11 + "Specification" "Model" "References" "Solution" (* structure only *) and
5.12 + "Given" "Find" "Relate" "Where" (* await input of term *) and
5.13 + "RTheory" (* await input of string; "R" distingues "Problem".."RProblem" *) and
5.14 + "RProblem" "RMethod" (* await input of string list *) and
5.15 + "Tactic" (* optionally repeated with each step 0.. end of calculation *)
5.16 +begin
5.17 +
5.18 +text \<open> trials on parsing with C.U.'s Isabelle Cookbook
5.19 + outdated:
5.20 + https://web.cs.wpi.edu/~dd/resources_isabelle/isabelle_programming.urban.pdf
5.21 + 2019
5.22 + http://talisker.nms.kcl.ac.uk/cgi-bin/repos.cgi/isabelle-cookbook/raw-file/tip/progtutorial.pdf
5.23 +\<close>
5.24 +
5.25 +chapter \<open>Work along book\<close>
5.26 +section \<open>Scan strings\<close>
5.27 +ML \<open>
5.28 +\<close> ML \<open> (*p.134 \<section>6.1*)
5.29 +($$ "h") (Symbol.explode "hello")
5.30 +\<close> ML \<open>
5.31 +($$ "h" -- $$ "e" -- $$ "l") (Symbol.explode "hello")
5.32 +\<close> ML \<open>
5.33 +let
5.34 + val p = Scan.optional ($$ "h") "x"
5.35 + val input1 = Symbol.explode "hello"
5.36 + val input2 = Symbol.explode "world"
5.37 +in
5.38 + (p input1, p input2)
5.39 +end
5.40 +\<close> ML \<open>
5.41 +op ||
5.42 +\<close> ML \<open>
5.43 +\<close>
5.44 +
5.45 +section \<open>Scan token list\<close>
5.46 +ML \<open>
5.47 +\<close> ML \<open> (*p.141 \<section>6.2*)
5.48 +Token.explode
5.49 + (Thy_Header.get_keywords' @{context}) Position.none "hello world"
5.50 +\<close> ML \<open>
5.51 +Token.explode: Keyword.keywords -> Position.T -> string -> Token.T list;
5.52 +Thy_Header.get_keywords': Proof.context -> Keyword.keywords;
5.53 +Position.none; (* = {}: Position.T *)
5.54 +\<close> ML \<open>
5.55 +\<close> ML \<open> (*p.142 \<section>6.2*)
5.56 +let
5.57 + val input = Token.explode (Thy_Header.get_keywords' @{context}) Position.none "hello world"
5.58 +in
5.59 + filter Token.is_proper input
5.60 +end
5.61 +\<close> ML \<open>
5.62 +fun filtered_input str =
5.63 + filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) Position.none str)
5.64 +\<close> ML \<open>
5.65 +filtered_input: string -> Token.T list
5.66 +\<close> ML \<open>
5.67 +\<close> ML \<open> (*p.144 \<section>6.2*)
5.68 +(Parse.enum1 "|" (Parse.$$$ "in")): string list parser
5.69 +\<close> text \<open>
5.70 +(Parse.enum1 "|" (Parse.$$$ "in")) (filtered_input "in | in | in")
5.71 +(** )
5.72 +ERROR: exception MORE () raised (line 159 of "General/scan.ML")
5.73 +( **)
5.74 +\<close> ML \<open>
5.75 +let
5.76 + val input = filtered_input "in | in | in"
5.77 + val p = Parse.enum "|" (Parse.$$$ "in")
5.78 +in
5.79 + Scan.finite Token.stopper p input
5.80 +end
5.81 +\<close> ML \<open>
5.82 +fun parse p input = Scan.finite Token.stopper (Scan.error p) input
5.83 +\<close> ML \<open>
5.84 +parse: (Token.T list -> 'a * Token.T list) -> Token.T list -> 'a * Token.T list
5.85 +\<close> ML \<open>
5.86 +parse (Parse.enum "|" (Parse.$$$ "in")) (filtered_input "in | in | in")
5.87 +(* = (["in", "in", "in"], []): string list * Token.T list *)
5.88 +\<close> ML \<open>
5.89 +\<close>
5.90 +
5.91 +section \<open>Scan.optional\<close>
5.92 +subsection \<open>Cookbook Scan.optional p.146 \<section>6.7\<close>
5.93 +inductive (*.. HOL.Complex required *)
5.94 + even and odd
5.95 +where
5.96 + even0: "even 0"
5.97 +| evenS: "odd n \<Longrightarrow> even (Suc n)"
5.98 +| oddS: "even n \<Longrightarrow> odd (Suc n)"
5.99 +
5.100 +ML \<open>
5.101 +@{term "even 0"}
5.102 +\<close> ML \<open>
5.103 +val spec_parser =
5.104 + Parse.vars --
5.105 + Scan.optional
5.106 + (Parse.$$$ "where" |--
5.107 + Parse.!!!
5.108 + (Parse.enum1 "|"
5.109 + (Parse_Spec.opt_thm_name ":" -- Parse.prop))) []
5.110 +\<close> ML \<open>
5.111 +(*relate signature to _ -- Scan.optional _: ---------------------------------------------------\*)
5.112 +spec_parser: ((binding * string option * mixfix) list * (Attrib.binding * string) list) parser;
5.113 +(* \------------ 'b ---------------------/ \---------- 'd --------------/ ^^^^^^*)
5.114 +spec_parser:
5.115 + Token.T list ->
5.116 +(*\--- 'a ---/*)
5.117 + ((binding * string option * mixfix) list * (Attrib.binding * string) list) * Token.T list
5.118 +(* \------------ 'b ---------------------/ \---------- 'd --------------/ \--- 'e ---/*)
5.119 +\<close> ML \<open>
5.120 +Parse.vars: ((binding * string option * mixfix) list) parser
5.121 +(* \------------------ 'b ---------------/ ^^^^^^*)
5.122 +\<close> ML \<open>
5.123 +op -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e (* <--------------------------*)
5.124 +\<close> ML \<open>
5.125 +val aaa =
5.126 + Scan.optional
5.127 + (Parse.$$$ "where" |--
5.128 + Parse.!!!
5.129 + (Parse.enum1 "|"
5.130 + (Parse_Spec.opt_thm_name ":" -- Parse.prop)))
5.131 +:
5.132 + (Attrib.binding * string) list -> Token.T list -> (Attrib.binding * string) list * Token.T list
5.133 +(*\---------- 'd --------------/ \-'a='c='e-/ \---------- 'd --------------/ \-'a='c='e-/*)
5.134 +\<close> ML \<open>
5.135 +aaa : (Attrib.binding * string) list -> (Attrib.binding * string) list parser
5.136 +(* \---------- 'd --------------/ \---------- 'd --------------/ ^^^^^^*)
5.137 +\<close> ML \<open>
5.138 +Scan.optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a;
5.139 +Scan.optional: ('d parser) -> 'd -> ('d parser);
5.140 +Scan.optional:
5.141 + ((Attrib.binding * string) list parser) ->
5.142 + (Attrib.binding * string) list -> ((Attrib.binding * string) list parser);
5.143 +(* \---------- 'd --------------/ -> \---------- 'd --------------/ ^^^^^^*)
5.144 +\<close> ML \<open>
5.145 +val bbb =
5.146 + (Parse.$$$ "where" |--
5.147 + Parse.!!!
5.148 + (Parse.enum1 "|"
5.149 + (Parse_Spec.opt_thm_name ":" -- Parse.prop)))
5.150 +:
5.151 + Token.T list -> (Attrib.binding * string) list * Token.T list;
5.152 +bbb : ((Attrib.binding * string) list) parser
5.153 +(* \---------- 'd --------------/ ^^^^^^*)
5.154 +(*relate signature to _ -- Scan.optional _: ---------------------------------------------------/*)
5.155 +\<close> ML \<open>
5.156 +\<close> ML \<open> (* final check of spec_parser: *)
5.157 +let
5.158 + val input = filtered_input (
5.159 + " even and odd " ^
5.160 + "where " ^
5.161 + " even0[intro]: \"even 0\" " ^
5.162 + "| evenS[intro]: \"odd \<Longrightarrow> even (Suc n)\" " ^
5.163 + "| oddS[intro]: \"even n \<Longrightarrow> odd (Suc n)\"")
5.164 +in
5.165 + parse spec_parser input
5.166 +end
5.167 +(* =
5.168 + (([("even", NONE, NoSyn), ("odd", NONE, NoSyn)],
5.169 + [(("even0", [[Token (("intro", ({}, {})), (Ident, "intro"), Slot)]]), "<markup>"),
5.170 + (("evenS", [[Token (("intro", ({}, {})), (Ident, "intro"), Slot)]]), "<markup>"),
5.171 + (("oddS", [[Token (("intro", ({}, {})), (Ident, "intro"), Slot)]]), "<markup>")]),
5.172 + [])*)
5.173 +\<close> ML \<open>
5.174 +\<close>
5.175 +
5.176 +subsection \<open>src/HOL/Tools/value_command.ML Scan.optional\<close>
5.177 +ML \<open>
5.178 +\<close> ML \<open>
5.179 +val opt_modes =
5.180 + Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!! (Scan.repeat1 Parse.name --| \<^keyword>\<open>)\<close>)) [];
5.181 +\<close> ML \<open>
5.182 +val opt_evaluator =
5.183 + Scan.optional (\<^keyword>\<open>[\<close> |-- Parse.name --| \<^keyword>\<open>]\<close>) "";
5.184 +\<close> ML \<open>
5.185 +val parse_value = opt_evaluator -- opt_modes -- Parse.term
5.186 +:
5.187 +Token.T list -> ((string * string list) * string) * Token.T list
5.188 +\<close> ML \<open>
5.189 +\<close>
5.190 +
5.191 +value "1 + 2 = (3::int)" (* <---------------- *)
5.192 +ML \<open>
5.193 +val toks = filtered_input "\"1 + 2 = (3::int)\""
5.194 +\<close> ML \<open>
5.195 +parse_value toks (* = ((("", []), "<markup>"), [])*)
5.196 +\<close>
5.197 +
5.198 +value [simp] "1 + 2 = (3::int)" (* <---------------- *)
5.199 +ML \<open>
5.200 +val toks = filtered_input "[simp] \"1 + 2 = (3::int)\""
5.201 +\<close> ML \<open>
5.202 +parse_value toks (* = ((("simp", []), "<markup>"), [])*)
5.203 +\<close>
5.204 +
5.205 +value [simp] (asci latex) "1 + 2 = (3::int)" (* <---------------- *)
5.206 +ML \<open>
5.207 +val toks = filtered_input "[simp] (asci latex) \"1 + 2 = (3::int)\""
5.208 +\<close> ML \<open>
5.209 +parse_value toks (* = ((("simp", ["asci", "latex"]), "<markup>"), [])*)
5.210 +\<close>
5.211 +
5.212 +
5.213 +chapter \<open>Own trials, NO Parse.cartouche, NO Outer_Syntax.command\<close>
5.214 +text \<open>
5.215 + compare test/../Keywords_Diag.thy
5.216 + for adding Parse.cartouche, Outer_Syntax.command
5.217 +\<close>
5.218 +section \<open>lists\<close>
5.219 +ML \<open>
5.220 +\<close> ML \<open> (*p.144 \<section>6.2 -- adapted from above ..*)
5.221 +let
5.222 + val input = filtered_input "in , in , in"
5.223 + val p = Parse.enum "," (Parse.$$$ "in")
5.224 +in
5.225 + Scan.finite Token.stopper p input
5.226 +end
5.227 +(* = (["in", "in", "in"], []) *)
5.228 +\<close> ML \<open>
5.229 +let
5.230 + val input = filtered_input "aaa , bbb , ccc"
5.231 + val p = Parse.enum "," Parse.name
5.232 +in
5.233 + Scan.finite Token.stopper p input
5.234 +end
5.235 +(* = (["aaa", "bbb", "ccc"], []) *)
5.236 +\<close> ML \<open>
5.237 +let
5.238 + val input = filtered_input "\"aaa\" , \"bbb\" , \"ccc\""
5.239 + val p = Parse.enum "," Parse.string
5.240 +in
5.241 + Scan.finite Token.stopper p input
5.242 +end
5.243 +(* = (["aaa", "bbb", "ccc"], []) *)
5.244 +\<close> ML \<open>
5.245 +let
5.246 + val input = filtered_input "\"aaa\" , \"bbb\" , \"ccc\""
5.247 + val p = Parse.list1 Parse.string
5.248 +in
5.249 + Scan.finite Token.stopper p input
5.250 +end
5.251 +(* = (["aaa", "bbb", "ccc"], []) *)
5.252 +\<close> ML \<open>
5.253 +let
5.254 + val input = filtered_input "[\"aaa\" , \"bbb\" , \"ccc\"]"
5.255 + val p = Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]"
5.256 +in
5.257 + Scan.finite Token.stopper p input
5.258 +end
5.259 +(* = (["aaa", "bbb", "ccc"], []) *)
5.260 +\<close> ML \<open>
5.261 +\<close>
5.262 +
5.263 +section \<open>Problem_headline\<close>
5.264 +ML \<open>
5.265 +val toks = filtered_input (
5.266 + (**)
5.267 + "Problem" ^ (**)
5.268 + "(" (**) ^
5.269 + "\"Biegelinie\"" (**) ^
5.270 + "," (**) ^
5.271 + " [\"Biegelinien\"]" (**) ^
5.272 + ")" (**)
5.273 +)
5.274 +\<close> ML \<open>
5.275 +parse (Parse.$$$ "Problem") toks
5.276 +\<close> ML \<open>
5.277 +Thy_Header.get_keywords' @{context}
5.278 +(*
5.279 + Keywords
5.280 + {commands =
5.281 + {(".",
5.282 + {files = [], id = 39558, kind = "qed", pos =
5.283 + {line=71, offset=3218, end_offset=3219, file=~~/src/Pure/Pure.thy}, tags = ["proof"]}),
5.284 +:
5.285 + minor =
5.286 + {"!", "!!", "%", "(", ")", "+", ",", ":", "::", ";", "<", "<=", "=", "==", "=>", "?", "Find",
5.287 + "Given", "Model", "Problem", "RMethod", "RProblem", "RTheory", "References", "Relate",
5.288 +:
5.289 +*)
5.290 +\<close> ML \<open>
5.291 +val problem_headline = Parse.$$$ "Problem" --
5.292 + Parse.$$$ "(" --
5.293 + Parse.string -- Parse.$$$ "," --
5.294 + (**)Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]" --(**)
5.295 + Parse.$$$ ")"
5.296 +\<close> ML \<open>
5.297 +val problem_headline' = Scan.finite Token.stopper problem_headline
5.298 +\<close> ML \<open>
5.299 +problem_headline toks
5.300 +(* = (((((("Problem", "("), "Biegelinie"), ","), ["Biegelinien"]), ")"), []) *)
5.301 +\<close> ML \<open>
5.302 +\<close>
5.303 +
5.304 +section \<open>Model\<close>
5.305 +ML \<open>
5.306 +\<close> ML \<open>
5.307 +val toks = filtered_input (
5.308 +" Model:" ^
5.309 +" Given: \"Traegerlaenge L\", \"Streckenlast q_0\"" ^
5.310 +" Where: \"q_0 ist_integrierbar_auf {| 0, L |}\", \"0 < L\"" ^
5.311 +" Find: \"Biegelinie y\"" ^
5.312 +" Relate: \"Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]\""
5.313 +)
5.314 +(* = [Token (("Model", ({}, {})), (Keyword, "Model"), Slot)]*)
5.315 +\<close> ML \<open>
5.316 +val model = (
5.317 + Parse.$$$ "Model" -- Parse.$$$ ":" --
5.318 + Parse.$$$ "Given" -- Parse.$$$ ":" -- Parse.list1 Parse.term --
5.319 + Parse.$$$ "Where" -- Parse.$$$ ":" -- Parse.list Parse.term --
5.320 + Parse.$$$ "Find" -- Parse.$$$ ":" -- Parse.term --
5.321 + Parse.$$$ "Relate" -- Parse.$$$ ":" -- Parse.list Parse.term
5.322 +)
5.323 +\<close> ML \<open>
5.324 +val model' = Scan.finite Token.stopper model
5.325 +\<close> ML \<open>
5.326 +model' toks
5.327 +(* =
5.328 + (((((((((((((("Model", ":"),
5.329 + "Given"), ":"), ["<markup>", "<markup>"]),
5.330 + "Where"), ":"), ["<markup>", "<markup>"]),
5.331 + "Find"), ":"), "<markup>"),
5.332 + "Relate"), ":"), ["<markup>"]),
5.333 + [])*)
5.334 +\<close> ML \<open>
5.335 +\<close>
5.336 +
5.337 +section \<open>References\<close>
5.338 +ML \<open>
5.339 +\<close> ML \<open>
5.340 +val toks = filtered_input (
5.341 +" References:" (**) ^
5.342 +" RTheory: \"Biegelinie\"" (**) ^
5.343 +" RProblem: [\"Biegelinien\"]" (**) ^
5.344 +" RMethod: [\"Integrieren\", \"KonstanteBestimmen2\"]" (**)
5.345 +)
5.346 +\<close> ML \<open>
5.347 +val references = (
5.348 + Parse.$$$ "References" -- Parse.$$$ ":" --
5.349 + Parse.$$$ "RTheory" -- Parse.$$$ ":" -- Parse.string --
5.350 + Parse.$$$ "RProblem" -- Parse.$$$ ":" --
5.351 + Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]" --
5.352 + Parse.$$$ "RMethod" -- Parse.$$$ ":" --
5.353 + Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]"
5.354 +)
5.355 +\<close> ML \<open>
5.356 +val references' = Scan.finite Token.stopper references
5.357 +\<close> ML \<open>
5.358 +references toks
5.359 +(* =
5.360 + ((((((((((("References", ":"),
5.361 + "RTheory"), ":"), "Biegelinie"),
5.362 + "RProblem"), ":"), ["Biegelinien"]),
5.363 + "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"]),
5.364 + [])*)
5.365 +\<close> ML \<open>
5.366 +\<close>
5.367 +
5.368 +section \<open>Solution\<close>
5.369 +text \<open>
5.370 + Problem is recursively possible in Solution.
5.371 + for recursive parsers see p.140 \<section>6.2: parse_tree
5.372 +\<close>
5.373 +ML \<open>
5.374 +\<close> ML \<open>
5.375 +val toks = filtered_input ( (*Problem.. postponed, some term shortened*)
5.376 +" Solution:" (**) ^
5.377 +(* HOW HANDLE THIS SPECIFIC Problem ?..
5.378 + "solveSystem [L * q_0 = c, 0 = (2 * c_2 + 2 * L * c + -1 * L ^ 2 * q_0) / 2, 0 = c_4, 0 = c_3] [c, c_1, c_2, c_4]"*)
5.379 +" [c = -1 * L * q_0 / -1, c_2 = -1 * L ^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]" (**) ^
5.380 +" y x = c_4 + c_3 * x + 1 / (-1 * EI)" (**) ^
5.381 +" Tactic Substitute \"c_4 + c_3 * x + 1 / (-1 * EI)\" \"[c, c_1, c_2, c_4]\"" (**) ^
5.382 +" y x = 0 + 0 * x + 1 / (-1 * EI)" (**) ^
5.383 +" Tactic Rewrite_Set_Inst \"[(bdv, x)]\" \"make_ratpoly_in\" \"y x\"" (**) ^
5.384 +" y x = -6 * q_0 * L ^ 2 / (-24 * EI)" (**) ^
5.385 +" Tactic Check_Postcond [\"Biegelinien\"]" (**)
5.386 +)
5.387 +\<close> ML \<open>
5.388 +\<close> ML \<open>
5.389 +\<close> ML \<open>
5.390 +\<close> ML \<open>
5.391 +\<close> ML \<open>
5.392 +\<close>
5.393 +
5.394 +section \<open>Problem: headline + Specification + Solution\<close>
5.395 +subsection \<open>TOWARDS Specification + Solution general\<close>
5.396 +text \<open>
5.397 + COMPARE subsection \<open>Cookbook Scan.optional p.146 \<section>6.7\<close> IN THIS FILE
5.398 +\<close>
5.399 +ML \<open>
5.400 +\<close> ML \<open>
5.401 +val toks = filtered_input (
5.402 +" Problem ( \"Biegelinie\" , [\"Biegelinien\"] )" (**) ^
5.403 +" Specification:" (**) ^
5.404 +" Solution:" (**)
5.405 +)
5.406 +\<close> ML \<open>
5.407 +(
5.408 + problem_headline (**) --
5.409 + Parse.$$$ "Specification" -- Parse.$$$ ":" (**) --
5.410 + Parse.$$$ "Solution" -- Parse.$$$ ":" (**)
5.411 +) toks
5.412 +\<close> ML \<open>
5.413 +(
5.414 + problem_headline (**) --
5.415 + (Scan.optional
5.416 + (Parse.$$$ "Specification" -- Parse.$$$ ":" (**) --
5.417 + Parse.$$$ "Solution" -- Parse.$$$ ":")
5.418 +) (*toks*)
5.419 +\<close> ML \<open>
5.420 +\<close> text \<open>
5.421 +(*relate signature to _ -- Scan.optional _: ---------------------------------------------------\*)
5.422 +calc_parser: (string list * string) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ parser
5.423 +(* \------- 'b ---------/ \---------- 'd --------------/ ^^^^^^*)
5.424 +calc_parser:
5.425 + Token.T list ->
5.426 +(*\--- 'a ---/*)
5.427 + ((string list * string) * (((string * string) * string) * string)) * Token.T list
5.428 +(* \------- 'b ---------/ \----------------- 'd --------------/ \-'a='c='e-/*)
5.429 +\<close> ML \<open>
5.430 +problem_headline: (string list * string) parser;
5.431 +(* \------- 'b ---------/ ^^^^^^*)
5.432 +\<close> ML \<open>
5.433 +op -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e (* <--------------------------*)
5.434 +\<close> ML \<open>
5.435 +\<close> ML \<open>
5.436 +\<close> ML \<open>
5.437 +\<close> ML \<open>
5.438 +\<close> ML \<open>
5.439 +\<close> ML \<open>
5.440 +\<close> ML \<open>
5.441 +\<close> ML \<open>
5.442 +\<close> ML \<open>
5.443 +\<close> ML \<open>
5.444 +\<close> ML \<open>
5.445 +\<close> ML \<open>
5.446 +\<close> ML \<open>
5.447 +\<close> ML \<open>
5.448 +Scan.optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a;
5.449 +Scan.optional:
5.450 + ((((string * string) * string) * string) parser) ->
5.451 + (((string * string) * string) * string) -> ((((string * string) * string) * string) parser);
5.452 +(* \----------------- 'd ---------------/ -> \----------------- 'd ---------------/ ^^^^^^*)
5.453 +\<close> ML \<open>
5.454 +val bbb =
5.455 + (Parse.$$$ "Specification" -- Parse.$$$ ":" (**) --
5.456 + Parse.$$$ "Solution" -- Parse.$$$ ":")
5.457 +:
5.458 + Token.T list -> (((string * string) * string) * string) * Token.T list;
5.459 +bbb: (((string * string) * string) * string) parser
5.460 +(* \----------------- 'd --------------/ ^^^^^^*)
5.461 +(*relate signature to _ -- Scan.optional _: ---------------------------------------------------/*)
5.462 +\<close> ML \<open>
5.463 +\<close> ML \<open>
5.464 +\<close> ML \<open>
5.465 +\<close> ML \<open>
5.466 +\<close> ML \<open>
5.467 +\<close> ML \<open>
5.468 +\<close>
5.469 +
5.470 +subsection \<open>Specification + Solution collapsed\<close>
5.471 +text \<open>
5.472 + The variants of input below should be accepted by the final calc_parser
5.473 +\<close>
5.474 +ML \<open>
5.475 +\<close> ML \<open>
5.476 +val toks = filtered_input (
5.477 +" Problem ( \"Biegelinie\" , [\"Biegelinien\"] )"
5.478 +)
5.479 +\<close> ML \<open>
5.480 +val toks = filtered_input (
5.481 +" Problem ( \"Biegelinie\" , [\"Biegelinien\"] )" (**) ^
5.482 +" Specification:" (**) ^
5.483 +" Solution:" (**)
5.484 +)
5.485 +\<close> ML \<open>
5.486 +\<close> ML \<open> (* + other variants ...*)
5.487 +\<close> ML \<open>
5.488 +(
5.489 + problem_headline (**) --
5.490 + Parse.$$$ "Specification" -- Parse.$$$ ":" (**) --
5.491 + Parse.$$$ "Solution" -- Parse.$$$ ":" (**)
5.492 +) toks
5.493 +\<close> ML \<open>
5.494 +\<close> ML \<open>
5.495 +\<close> ML \<open>
5.496 +\<close> ML \<open>
5.497 +\<close> ML \<open>
5.498 +\<close> ML \<open>
5.499 +\<close> ML \<open>
5.500 +\<close> ML \<open>
5.501 +\<close>
5.502 +
5.503 +(** )end( * Missing outer syntax command(s) "ISAC" *)
6.1 --- a/test/Tools/isac/Test_Isac.thy Thu Jul 02 09:57:58 2020 +0200
6.2 +++ b/test/Tools/isac/Test_Isac.thy Fri Jul 17 11:42:20 2020 +0200
6.3 @@ -57,23 +57,24 @@
6.4
6.5 theory Test_Isac
6.6 imports Isac.Build_Isac (* note that imports are WITHOUT open struct ..*)
6.7 - (* in case of ERROR Bad theory import "Draft.Thy_All"..., open each theory one by one *)
6.8 + (* in case of ERROR Bad theory import "Draft.Thy_All"..., open each theory one by one
6.9 + and find out, which ML_file or *.thy causes an error (might be ONLY one).
6.10 + Also backup files (#* ) recognised by jEdit cause this trouble *)
6.11 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
6.12 - "~~/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All" (*broken with 05944144a692 *)
6.13 -(**)"~~/test/Tools/isac/ADDTESTS/Ctxt" (*broken with 05944144a692 *)
6.14 -(**)"~~/test/Tools/isac/ADDTESTS/test-depend/Build_Test" (*broken with 05944144a692 *)
6.15 -(**)"~~/test/Tools/isac/ADDTESTS/All_Ctxt" (*broken with 05944144a692 *)
6.16 -(**)"~~/test/Tools/isac/ADDTESTS/Test_Units" (*broken with 05944144a692 *)
6.17 -(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics" (*broken with 05944144a692 *)
6.18 -(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting" (*broken with 05944144a692 *)
6.19 -(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"(*broken with 05944144a692 *)
6.20 -(**)"~~/test/Tools/isac/ADDTESTS/file-depend/BuildC_Test" (*broken with 05944144a692 *)
6.21 -(**)"~~/test/Tools/isac/ADDTESTS/session-get_theory/Foo" (*broken with 05944144a692 *)
6.22 + "~~/test/Tools/isac/ADDTESTS/accumulate-val/Thy_All"
6.23 +(**)"~~/test/Tools/isac/ADDTESTS/Ctxt"
6.24 +(**)"~~/test/Tools/isac/ADDTESTS/test-depend/Build_Test"
6.25 +(**)"~~/test/Tools/isac/ADDTESTS/All_Ctxt"
6.26 +(**)"~~/test/Tools/isac/ADDTESTS/Test_Units"
6.27 +(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics"
6.28 +(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"
6.29 +(**)"~~/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"
6.30 +(**)"~~/test/Tools/isac/ADDTESTS/file-depend/BuildC_Test"
6.31 +(**)"~~/test/Tools/isac/ADDTESTS/session-get_theory/Foo"
6.32 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
6.33 ADDTESTS/------------------------------------------- see end of tests *)
6.34 -(*"~~/test/Pure/Isar/Test_Parsers" dropped Isabelle2014-->2015 *)
6.35 -(*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011*)
6.36 -(**)"~~/test/Pure/Isar/Test_Parse_Term" (*broken with 05944144a692 *)
6.37 +(**)"~~/test/Pure/Isar/Test_Parsers"
6.38 +(**)"~~/test/Pure/Isar/Test_Parse_Term"
6.39 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
6.40 "~~/test/Tools/isac/Specify/refine" (* setup for refine.sml *)
6.41 "~~/test/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *)
7.1 --- a/test/Tools/isac/Test_Isac_Short.thy Thu Jul 02 09:57:58 2020 +0200
7.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Fri Jul 17 11:42:20 2020 +0200
7.3 @@ -73,9 +73,8 @@
7.4 (**)"~~/test/Tools/isac/ADDTESTS/session-get_theory/Foo"
7.5 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
7.6 ADDTESTS/------------------------------------------- see end of tests *)
7.7 -(*"~~/test/Pure/Isar/Test_Parsers" dropped Isabelle2014-->2015 TODO?!?: replace *)
7.8 -(*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011 DELELTE *)
7.9 -(**)"~~/test/Pure/Isar/Test_Parse_Term" (*code outcommente TODO?!?: replace *)
7.10 +(**)"~~/test/Pure/Isar/Test_Parsers"
7.11 +(**)"~~/test/Pure/Isar/Test_Parse_Term"
7.12 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
7.13 "~~/test/Tools/isac/Specify/refine" (* setup for refine.sml *)
7.14 "~~/test/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *)