# HG changeset patch
# User Walther Neuper <walther.neuper@jku.at>
# Date 1596190894 -7200
# Node ID a05df90c0deebad4df9707efa6067fe4ebfd9543
# Parent  95a20f5bc2560e7af79da729c2dfc0077e6210bc
prep.2 recursion Problem .. Solution

diff -r 95a20f5bc256 -r a05df90c0dee src/Tools/isac/TODO.thy
--- a/src/Tools/isac/TODO.thy	Tue Jul 28 16:17:42 2020 +0200
+++ b/src/Tools/isac/TODO.thy	Fri Jul 31 12:21:34 2020 +0200
@@ -224,6 +224,19 @@
 text \<open>
   \begin{itemize}
   \item xxx          
+  \item xxx
+  \item make parser mutually recursive for Problem .. Solution
+    preps. in Test_Parse_Isac:
+      Test_Parse_Isac:
+        subsubsection "problem_mini" shows a principal issue with recursive parsing
+        probably due to !2! arguments of parser (as shown in Cookbook)
+      Test_Parsers_Cookbook:
+        (* recursive parser p.140 \<section>6.1 adapted to tokens: *) shows differences,
+        which might help understanding the principal issue
+    see also Test_Parsers  subsection "recursive parsing"
+  \item xxx
+  \item xxx          
+  \item xxx          
   \item revisit bootstrap Calcelements. rule->calcelems->termC
     would be nice, but is hard: UnparseC.terms -> TermC.s_to_string
   \item xxx
diff -r 95a20f5bc256 -r a05df90c0dee test/Pure/Isar/Test_Parse_Isac.thy
--- a/test/Pure/Isar/Test_Parse_Isac.thy	Tue Jul 28 16:17:42 2020 +0200
+++ b/test/Pure/Isar/Test_Parse_Isac.thy	Fri Jul 31 12:21:34 2020 +0200
@@ -19,6 +19,10 @@
 \<close> ML \<open>
 fun parse parser toks = Scan.finite Token.stopper (Scan.error parser) toks
 \<close> ML \<open>
+fun string_of_strs strs = fold (curry op ^) (rev strs) ""
+\<close> ML \<open>
+fun string_of_toks toks = fold (curry op ^) (map Token.unparse toks |> rev |> separate ", ") "";
+\<close> ML \<open>
 \<close>
 
 section \<open>Goals for parsing\<close>
@@ -168,8 +172,6 @@
       steps_nonrec
 )
 \<close> ML \<open>
-problem_whole_str
-\<close> ML \<open>
 if problem_whole_str =
   "Problem ( \"Biegelinie\" , [\"Biegelinien\"] )" ^
     "Specification:" ^
@@ -354,9 +356,7 @@
     (model -- references) (**)
 )
 \<close> ML \<open>
-val specification_whole' = Scan.finite Token.stopper specification_whole
-\<close> ML \<open>
-specification_whole toks
+parse specification_whole toks
 (* = (((
   "Specification", ":"),
      ((((((((((((((
@@ -616,7 +616,19 @@
 
 subsubsection \<open>enter Specification TODO\<close>
 text \<open>
-the Model only has Descriptors and the References are empty
+  the Model only has Descriptors and the References are empty
+\<close> ML \<open>
+val toks = tokenize (
+  problem_headline_str ^
+    "Specification:" ^
+      model_empty_str ^ (* <<<----- empty *)
+      "References:" ^   (* <<<----- collapsed *)
+    "Solution:"
+)
+\<close> text \<open>
+parse problem toks
+\<close> ML \<open>
+\<close> ML \<open>
 \<close> ML \<open>
 \<close> ML \<open>
 \<close> ML \<open>
@@ -720,10 +732,8 @@
   problem_nonrec  parser
 (*               ^^^^^^^*)
 \<close> ML \<open>
-parse problem_nonrec toks
-\<close> ML \<open>
 case parse problem_nonrec toks of
-  (((((((((("Problem", "("), "Biegelinie"), ","), ["Biegelinien"]), ")"), (* problem_headline *)
+  (((((((((("Problem", "("), "Biegelinie"), ","), ["Biegelinien"]), ")"), (* ..problem_headline *)
       (("Specification", ":"),
        ((((((((((( (((("", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""),
          []), (((((((((("", ""), ""), ""), ""), ""), ""), []), ""), ""), []) )))
@@ -741,10 +751,114 @@
 \<close> ML \<open>
 \<close>
 
+subsubsection \<open>problem_mini\<close>
+text \<open>
+  we make a minimal problem in order to investigate types
+  of the parser's components
+\<close> ML \<open>
+val problem_headline_mini = Parse.$$$ "Problem" 
+\<close> ML \<open>
+val specification_mini = Parse.$$$ "Specification"
+\<close> ML \<open>
+fun exec_name str = "EXEC IMMEDIATELY exec_name: " ^ str;
+fun exec_int int = "EXEC IMMEDIATELY exec_int: " ^ string_of_int int;
+\<close> ML \<open>
+Parse.name >> exec_name: string parser;
+Parse.int >> exec_int  : string parser
+\<close> ML \<open>
+\<close> ML \<open> (* nonrecursive *)
+fun problem_mini toks =
+  problem_headline_mini --
+  specification_mini -- steps_mini toks
+and steps_mini _ =
+  Parse.name >> exec_name || Parse.int >> exec_int
+\<close> ML \<open>
+(problem_mini "") (tokenize "Problem Specification aaa")
+(* = ((("Problem", "Specification"), "EXEC IMMEDIATELY exec_name: aaa"), [])*)
+\<close> ML \<open>
+problem_mini: 'a -> Token.T list -> ((string * string) * string) * Token.T list
+\<close> ML \<open>
+fun exec_problem_mini ((headl, spec), steps) =
+  ["EXEC IMMEDIATELY exec_int: ((" ^ headl ^ ", " ^ spec ^ "0, " ^ string_of_strs steps];
+\<close> ML \<open>
+fun exec_name str = ["EXEC IMMEDIATELY exec_name: " ^ str];
+\<close> ML \<open>
+\<close> ML \<open> (* recursive *)
+fun problem_mini toks =
+  (problem_headline_mini --
+  specification_mini -- steps_mini) toks
+and steps_mini toks =
+  (Parse.name >> exec_name || problem_mini >> exec_problem_mini) toks
+\<close> ML \<open>
+problem_mini: Token.T list -> ((string * string) * string list) * Token.T list ;
+steps_mini  : Token.T list -> string list * Token.T list ;
+\<close> ML \<open>
+problem_mini: ((string * string) * string list) parser;
+steps_mini  : string list parser;
+\<close> ML \<open>
+problem_mini (tokenize "Problem Specification aaa")
+(* = ((("Problem", "Specification"), ["EXEC IMMEDIATELY exec_name: aaa"]), [])*)
+\<close> text \<open> ERROR ?!?!?
+parse problem_mini (tokenize "Problem Specification   Problem Specification")
+exception FAIL (SOME fn) raised (line 152 of "General/scan.ML")
+\<close> ML \<open>
+\<close> ML \<open>
+\<close> ML \<open> (* recursive + repeat *)
+fun exec_name str = "EXEC IMMEDIATELY exec_name: " ^ str;
+\<close> ML \<open>
+fun exec_problem_mini ((headl, spec), steps) =
+  "EXEC IMMEDIATELY exec_int: ((" ^ headl ^ ", " ^ spec ^ "0, " ^ string_of_strs steps;
+\<close> ML \<open>
+fun problem_mini toks =
+  (writeln ("problem_mini " ^ string_of_toks toks); problem_headline_mini --
+  specification_mini -- (writeln ("steps_mini   " ^ string_of_toks toks); steps_mini)) toks
+and steps_mini toks =
+  (Scan.repeat
+    ((writeln ("name         " ^ string_of_toks toks); Parse.name >> exec_name) (**)||
+     (writeln ("sub-problem  " ^ string_of_toks toks); problem_mini >> exec_problem_mini)(**))) toks
+\<close> text \<open>
+problem_mini (tokenize "Problem Specification")
+(*
+problem_mini Problem, Specification 
+steps_mini   Problem, Specification 
+name          
+sub-problem   
+exception MORE () raised (line 159 of "General/scan.ML")*)
+\<close> text \<open>
+problem_mini (tokenize "Problem Specification aaa")
+(*
+problem_mini Problem, Specification, aaa 
+steps_mini   Problem, Specification, aaa 
+name         aaa 
+sub-problem  aaa 
+exception MORE () raised (line 159 of "General/scan.ML")
+
+NOTE: this error persists in case outcommented (** )||
+     (writeln ("sub-problem  " ^ string_of_toks toks); problem_mini >> exec_problem_mini)( **)
+
+THUS THERE IS SOMETHING NOT UNDERSTOOD, see !2! arguments in Test_Parsers_Cookbook.thy
+see Test_Parsers_Cookbook (* recursive parser p.140 \<section>6.1 adapted to tokens: *)
+*)
+\<close> ML \<open>
+\<close> ML \<open>
+\<close> ML \<open>
+\<close> ML \<open>
+\<close> ML \<open>
+\<close> ML \<open>
+\<close> ML \<open>
+\<close> ML \<open>
+\<close> ML \<open>
+\<close> ML \<open>
+\<close> ML \<open>
+\<close> ML \<open>
+\<close> ML \<open>
+\<close> ML \<open>
+\<close> ML \<open>
+\<close>
+
 subsubsection \<open>recursion finalised\<close>
 ML \<open>
 \<close> ML \<open>
-\<close> ML \<open>
 val toks = tokenize (
   problem_headline_str ^
     "Specification:" ^
@@ -753,8 +867,7 @@
 )
 \<close> ML \<open>
 fun exec_step_term (tm, (tac1, tac2)) = exec_step_term_nonrec (tm, (tac1, tac2));
-\<close> ML \<open>
-(* finding the type of exec_subproblem: *)
+\<close> ML \<open> (* finding the type of exec_subproblem: *)
 fun problem xxx =
   problem_headline --
     specification --
@@ -766,7 +879,7 @@
       )
 \<close> ML \<open>
 problem : (problem_nonrec -> string) -> problem_nonrec parser
-(*  xxx : ^^^^^^^^^^^^^^^^^^^^^^^^^^*)
+(*  xxx : ^^^^^^^^^^^^^^^^^^^^^^^^^^                   ^^^^^^*)
 \<close> text \<open>
 (* type of xxx from <Output>: *)
 (((((((((string * string) * string) * string) * string list) * string) *
@@ -783,7 +896,7 @@
         strs18), s19), s20), strs21), s22), s23), s24), s25), s26), strs27),
          ((((((((((s31, s32), s33), s34), s35), s36), s37), strs38), s39), s40), strs41) )))
      , s51), s61), strs71) =
-  "EXEC IMMEDIATELY step_subproblem:\n " ^
+  "EXEC IMMEDIATELY step_subproblem:\n" ^
   "(((( (((((" ^ s1 ^ ", " ^ s2 ^ "), " ^ s3 ^"), " ^ s4 ^"), " ^ LibraryC.strs2str strs5 ^ "), " ^ s6 ^")\n " ^
   "((" ^s7 ^ ", " ^s8 ^ "),\n" ^
   "  ((((((((((( ((((" ^ s11 ^", ((" ^s12 ^ ", " ^ s13 ^ "), " ^ s14 ^ ")), " ^ s15 ^"), " ^s16 ^"), " ^ s17 ^ "),\n " ^
@@ -808,24 +921,27 @@
 \<close> ML \<open>
 exec_subproblem : problem_nonrec -> string
 \<close> ML \<open>
-fun problem xxx =
+\<close> ML \<open> (* exec_subproblem has right? type in problem *)
+fun problem _ =
   problem_headline --
     specification --
-    Parse.$$$ "Solution" -- Parse.$$$ ":" -- (steps xxx)
-and steps xxx =
+    Parse.$$$ "Solution" -- Parse.$$$ ":" -- (steps 1)
+and steps _ =
       Scan.repeat (
         (
           ((Parse.term -- (Scan.optional tactic ("", ""))) >> exec_step_term) ||
-          (problem xxx >> exec_subproblem)
-    (*                    ^^^^^^^^^^^^^^^*)
+          (problem 1 >> exec_subproblem)
+    (*                  ^^^^^^^^^^^^^^^*)
         )
       )
 \<close> ML \<open>
-problem : (problem_nonrec -> string) -> problem_nonrec parser
-(*  xxx : ^^^^^^^^^^^^^^^^^^^^^^^^^^ ..exec_subproblem*)
+problem : int -> problem_nonrec parser
 \<close> ML \<open>
-\<close> ML \<open>
-\<close> ML \<open> (* here is the attempt towards finalisation *)
+steps   : int -> string list    parser
+\<close> ML \<open> (* BUT: omitting the parsers' arguments does NOT work:
+
+ *)
+\<close> ML \<open> (* here is the attempt towards finalisation * )
 val problem =
   problem_headline --
     specification --
@@ -837,106 +953,7 @@
           (problem >> exec_subproblem)
         )
       )
-\<close> text \<open>
-ML error:
-Type error in function application.
-   Function: -- :
-      (Token.T list ->
-         ((((((((string * string) * string) * string) * string list) * string) *
-            ((string * string) *
-             (((((((((((((((string * ((string * string) * string)) * string) * string) * string) * string list) * string) * string) * string list) * string) * string) * string) * string) * string) * string list) *
-              ((((((((((string * string) * string) * string) * string) * string) * string) * string list) * string) * string) * string list))))
-           *
-           string)
-          *
-          string)
-         *
-         Token.T list)
-      *
-      (Token.T list -> 'a * 'b)
-        ->
-        Token.T list ->
-          (((((((((string * string) * string) * string) * string list) * string) *
-              ((string * string) *
-               (((((((((((((((string * ((string * string) * string)) * string) * string) * string) * string list) * string) * string) * string list) * string) * string) * string) * string) * string) * string list)
-                *
-                ((((((((((string * string) * string) * string) * string) * string) * string) * string list) * string) * string) * string list))))
-             *
-             string)
-            *
-            string)
-           *
-           'a)
-          *
-          'b
-   Argument: (problem_headline -- specification -- Parse.$$$ "Solution" -- Parse.$$$ ":", steps) :
-      (Token.T list ->
-         ((((((((string * string) * string) * string) * string list) * string) *
-            ((string * string) *
-             (((((((((((((((string * ((string * string) * string)) * string) * string) * string) * string list) * string) * string) * string list) * string) * string) * string) * string) * string) * string list) *
-              ((((((((((string * string) * string) * string) * string) * string) * string) * string list) * string) * string) * string list))))
-           *
-           string)
-          *
-          string)
-         *
-         Token.T list)
-      *
-      (Token.T list -> Token.T list -> string list * Token.T list)
-   Reason: Can't unify 'a * 'b to Token.T list -> string list * Token.T list (Incompatible types)
-ML error:
-Type error in function application.
-   Function: >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
-   Argument: (problem, exec_subproblem) :
-      ('a ->
-         Token.T list ->
-           (((((((((string * string) * string) * string) * string list) * string) *
-               ((string * string) *
-                (((((((((((((((string * ((string * string) * string)) * string) * string) * string) * string list) * string) * string) * string list) * string) * string) * string) * string) * string) *
-                  string list)
-                 *
-                 ((((((((((string * string) * string) * string) * string) * string) * string) * string list) * string) * string) * string list))))
-              *
-              string)
-             *
-             string)
-            *
-            string list)
-           *
-           Token.T list)
-      *
-      (((((((((string * string) * string) * string) * string list) * string) *
-          ((string * string) *
-           (((((((((((((((string * ((string * string) * string)) * string) * string) * string) * string list) * string) * string) * string list) * string) * string) * string) * string) * string) * string list) *
-            ((((((((((string * string) * string) * string) * string) * string) * string) * string list) * string) * string) * string list))))
-         *
-         string)
-        *
-        string)
-       *
-       string list
-         -> string)
-   Reason:
-      Can't unify 'a * 'b to
-         Token.T list ->
-           (((((((((string * string) * string) * string) * string list) * string) *
-               ((string * string) *
-                (((((((((((((((string * ((string * string) * string)) * string) * string) * string) * string list) * string) * string) * string list) * string) * string) * string) * string) * string) *
-                  string list)
-                 *
-                 ((((((((((string * string) * string) * string) * string) * string) * string) * string list) * string) * string) * string list))))
-              *
-              string)
-             *
-             string)
-            *
-            string list)
-           *
-           Token.T list
-         (Incompatible types)
-\<close> ML \<open>
-\<close> ML \<open>
-\<close> ML \<open>
+*)
 \<close> ML \<open>
 \<close> ML \<open>
 \<close> ML \<open>
diff -r 95a20f5bc256 -r a05df90c0dee test/Pure/Isar/Test_Parsers.thy
--- a/test/Pure/Isar/Test_Parsers.thy	Tue Jul 28 16:17:42 2020 +0200
+++ b/test/Pure/Isar/Test_Parsers.thy	Fri Jul 31 12:21:34 2020 +0200
@@ -187,6 +187,49 @@
 ML \<open>(*from Pure/Isar/args.ML, fun attribs*)
 Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]";
 (*fn : Token.T list -> bstring list * Token.T list*)
+\<close> ML \<open>
+\<close> ML \<open> (* example close to lists see Cookbook p.144 \<section>6.2 *)
+let
+  val input = filtered_input "in , in , in"
+  val p = Parse.enum "," (Parse.$$$ "in")
+in
+  Scan.finite Token.stopper p input
+end
+(* = (["in", "in", "in"], []) *)
+\<close> ML \<open>
+let
+  val input = filtered_input "aaa , bbb , ccc"
+  val p = Parse.enum "," Parse.name
+in
+  Scan.finite Token.stopper p input
+end
+(* = (["aaa", "bbb", "ccc"], []) *)
+\<close> ML \<open>
+let
+  val input = filtered_input "\"aaa\" , \"bbb\" , \"ccc\""
+  val p = Parse.enum "," Parse.string
+in
+  Scan.finite Token.stopper p input
+end
+(* = (["aaa", "bbb", "ccc"], []) *)
+\<close> ML \<open>
+let
+  val input = filtered_input "\"aaa\" , \"bbb\" , \"ccc\""
+  val p = Parse.list1 Parse.string
+in
+  Scan.finite Token.stopper p input
+end
+(* = (["aaa", "bbb", "ccc"], []) *)
+\<close> ML \<open>
+let
+  val input = filtered_input "[\"aaa\" , \"bbb\" , \"ccc\"]"
+  val p = Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]"
+in
+  Scan.finite Token.stopper p input
+end
+(* = (["aaa", "bbb", "ccc"], []) *)
+
+
 
 \<close> ML \<open>
 parse (Parse.$$$ "[" |-- Parse.list Parse.name --| Parse.$$$ "]")
diff -r 95a20f5bc256 -r a05df90c0dee test/Pure/Isar/Test_Parsers_Cookbook.thy
--- a/test/Pure/Isar/Test_Parsers_Cookbook.thy	Tue Jul 28 16:17:42 2020 +0200
+++ b/test/Pure/Isar/Test_Parsers_Cookbook.thy	Fri Jul 31 12:21:34 2020 +0200
@@ -1,17 +1,9 @@
-chapter \<open>Trials derived from NEW Isabelle Cookbook\<close>
+(*
+  Trials derived from NEW Isabelle Cookbook
+*)
 
 theory Test_Parsers_Cookbook
   imports (**) Pure (** ) HOL.Complex ( *.. for inductive even BELOW*)
-keywords (*see section \<open>Own trials ..\<close>*)
-  (* this has a type and thus is a "major keyword" * )
-  "ISAC" :: diag and
-  ( * the following are without type: "minor keywords" *)
-  "Problem" (* root-problem + recursively in Solution *)
-  "Specification" "Model" "References" "Solution" (* structure only *) and
-  "Given" "Find" "Relate" "Where" (* await input of term *) and
-  "RTheory" (* await input of string; "R" distingues "Problem".."RProblem" *) and
-  "RProblem" "RMethod" (* await input of string list *) and
-  "Tactic" (* optionally repeated with each step 0.. end of calculation *)
 begin
 
 text \<open> trials on parsing with C.U.'s Isabelle Cookbook
@@ -175,6 +167,205 @@
 \<close> ML \<open>
 \<close>
 
+subsection \<open>recursive parsers\<close>
+subsubsection \<open>recursive parser p.140 \<section>6.1\<close>
+ML \<open>
+\<close> ML \<open>
+datatype tree =
+    Lf of string
+  | Br of tree * tree
+\<close> ML \<open> (* this version loops *)
+fun parse_basic s =
+  $$ s >> Lf || $$ "(" |-- parse_tree s --| $$ ")"
+and parse_tree s =
+  parse_basic s --| $$ "," -- parse_tree s >> Br || parse_basic s
+\<close> ML \<open>
+parse_basic: string -> string list -> tree * string list;
+parse_tree : string -> string list -> tree * string list
+\<close> ML \<open>
+\<close> ML \<open> (* this version works *)
+fun parse_basic s xs =
+  ($$ s >> Lf || $$ "(" |-- parse_tree s --| $$ ")") xs
+and parse_tree s xs =
+  (parse_basic s --| $$ "," -- parse_tree s >> Br || parse_basic s) xs
+\<close> ML \<open>
+parse_basic: string -> string list -> tree * string list;
+parse_tree : string -> string list -> tree * string list
+\<close> ML \<open>
+let
+  val input = Symbol.explode "(A,((A))),A"
+in
+  Scan.finite Symbol.stopper (parse_tree "A") (input)
+end
+(*= (Br (Br (Lf "A", Lf "A"), Lf "A"), []) *)
+\<close> ML \<open>
+Scan.finite Symbol.stopper (parse_tree "A") (Symbol.explode "(A,((A))),A")
+ = (Br (Br (Lf "A", Lf "A"), Lf "A"), [])
+\<close> ML \<open>
+Scan.finite Symbol.stopper (parse_tree "B") (Symbol.explode "(B,((B))),B")
+ = (Br (Br (Lf "B", Lf "B"), Lf "B"), [])
+\<close> ML \<open>
+Br (Lf "a",                Lf "b");
+Br (Lf "a",                Br (Lf "b1", Lf "b2"));
+Br (Br (Lf "a1", Lf "a2"), Br (Lf "b1", Lf "b2"));
+\<close> ML \<open>
+\<close> ML \<open>
+Scan.finite Symbol.stopper (parse_tree "A") (Symbol.explode "A")
+ = (Lf "A", [])
+\<close> ML \<open>
+Scan.finite Symbol.stopper (parse_tree "A") (Symbol.explode "A A")
+ = (Lf "A", [" ", "A"])
+\<close> ML \<open>
+Scan.finite Symbol.stopper (parse_tree "A") (Symbol.explode "A B")
+ = (Lf "A", [" ", "B"])
+\<close> ML \<open>
+Scan.finite Symbol.stopper (parse_tree "A") (Symbol.explode "AB")
+ = (Lf "A", ["B"])
+\<close> ML \<open>
+Scan.finite Symbol.stopper (parse_tree "A") (Symbol.explode "A,")
+ = (Lf "A", [","])
+\<close> text \<open>
+Scan.finite Symbol.stopper (parse_tree "A") (Symbol.explode "(A,")
+exception FAIL NONE raised (line 161 of "General/scan.ML")
+\<close> ML \<open>
+\<close> ML \<open>
+\<close>
+
+subsubsection \<open>recursive parser p.140 \<section>6.1 + writeln\<close>
+ML \<open>
+\<close> ML \<open>
+fun string_of_strs strs = fold (curry op ^) (rev strs) ""
+\<close> ML \<open>
+fun parse_basic s xs =
+(
+  writeln ("parse_basic " ^ s ^ " " ^ string_of_strs xs);
+  ($$ s >> Lf || $$ "(" |-- parse_tree s --| $$ ")") xs
+)
+and parse_tree s xs =
+(
+  writeln ("parse_tree  " ^ s ^ " " ^ string_of_strs xs);
+  (parse_basic s --| $$ "," -- parse_tree s >> Br || parse_basic s) xs
+)
+\<close> ML \<open>
+Scan.finite Symbol.stopper (parse_tree "A") (Symbol.explode "(A,((A))),A")
+(*
+parse_tree  A (A,((A))),A 
+parse_basic A (A,((A))),A 
+parse_tree  A A,((A))),A 
+parse_basic A A,((A))),A 
+
+parse_tree  A ((A))),A     ..1 + from here the version with tokenize differs
+parse_basic A ((A))),A 
+parse_tree  A (A))),A 
+parse_basic A (A))),A 
+parse_tree  A A))),A 
+parse_basic A A))),A 
+parse_basic A A))),A 
+parse_basic A (A))),A 
+parse_tree  A A))),A 
+parse_basic A A))),A 
+parse_basic A A))),A 
+parse_basic A ((A))),A      ..1
+parse_tree  A (A))),A 
+parse_basic A (A))),A 
+parse_tree  A A))),A 
+parse_basic A A))),A 
+parse_basic A A))),A 
+parse_basic A (A))),A 
+parse_tree  A A))),A 
+parse_basic A A))),A 
+parse_basic A A))),A 
+parse_tree  A A 
+parse_basic A A 
+parse_basic A A 
+val it = (Br (Br (Lf "A", Lf "A"), Lf "A"), []): tree * string list*)
+\<close> ML \<open>
+\<close> ML \<open>
+\<close> ML \<open>
+\<close> ML \<open>
+\<close> ML \<open>
+\<close> ML \<open>
+\<close> ML \<open>
+\<close>
+
+subsubsection \<open>recursive parser, same with tokenise + writeln\<close>
+text \<open>
+  Differences between Cookbook original on strings and below on tokes
+  might help to understand principles of recursive parsing.
+  See also Test_Parsers:  subsection "recursive parsing" 
+\<close> ML \<open>
+\<close> ML \<open> (* tools from Test_Parse_Isac.thy *)
+fun tokenize str =
+  filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) Position.none str)
+fun parse parser toks = Scan.finite Token.stopper (Scan.error parser) toks
+\<close> ML \<open>
+val toks = tokenize "(A,((A))),A"
+\<close> ML \<open>
+fun string_of_toks toks = fold (curry op ^) (map Token.unparse toks |> rev) "";
+string_of_toks toks = "(A,((A))),A"
+\<close> ML \<open>
+\<close> ML \<open> (* recursive parser p.140 \<section>6.1 adapted to tokens: *)
+fun parse_basic s xs =
+(
+  writeln ("parse_basic " ^ s ^ " " ^ string_of_toks xs);
+  (Parse.$$$ s >> Lf || Parse.$$$ "(" |-- parse_tree s --| Parse.$$$ ")") xs
+)
+and parse_tree s xs =
+(
+  writeln ("parse_tree  " ^ s ^ " " ^ string_of_toks xs);
+  (parse_basic s --| Parse.$$$ "," -- parse_tree s >> Br || parse_basic s) xs
+)
+\<close> ML \<open>
+parse_basic : string -> Token.T list -> tree * Token.T list;
+parse_tree  : string -> Token.T list -> tree * Token.T list;
+
+parse_basic : string -> tree parser;
+parse_tree  : string -> tree parser;
+\<close> text \<open>
+(parse_tree "A") (tokenize "(A,((A))),A");
+(* compare subsubsection \<open>recursive parser p.140 \<section>6.1 + writeln\<close> ..
+parse_tree  A (A,((A))),A 
+parse_basic A (A,((A))),A 
+parse_tree  A A,((A))),A 
+parse_basic A A,((A))),A
+                        parser p.140 \<section>6.1: parse_tree  A ((A))),A
+                                           :
+parse_basic A A,((A))),A                   .. different
+parse_basic A (A,((A))),A 
+parse_tree  A A,((A))),A 
+parse_basic A A,((A))),A 
+parse_basic A A,((A))),A 
+exception FAIL (SOME fn) raised (line 152 of "General/scan.ML")*)
+\<close> text \<open>
+(parse_basic "A") (tokenize "A");
+(*
+parse_basic A A 
+exception FAIL (SOME fn) raised (line 152 of "General/scan.ML")*)
+\<close> text \<open>
+parse (parse_basic "A") (tokenize "A")
+(*
+parse_basic A A 
+exception FAIL (SOME fn) raised (line 152 of "General/scan.ML")*)
+\<close> text \<open>
+(parse_tree "A") (tokenize "(A,A)");
+(*
+parse_tree  A (A,A) 
+parse_basic A (A,A) 
+parse_tree  A A,A) 
+parse_basic A A,A) 
+parse_basic A A,A) 
+parse_basic A (A,A) 
+parse_tree  A A,A) 
+parse_basic A A,A) 
+parse_basic A A,A) 
+exception FAIL (SOME fn) raised (line 152 of "General/scan.ML")*)
+\<close> ML \<open>
+\<close> ML \<open>
+\<close> ML \<open>
+\<close> ML \<open>
+\<close>
+
+
 section \<open>Own trials, NO Parse.cartouche, NO Outer_Syntax.command\<close>
 text \<open>
   compare test/../Keywords_Diag.thy
@@ -225,26 +416,4 @@
 \<close> ML \<open>
 \<close>
 
-subsection \<open>problem_headline\<close>
-text \<open>
-  -> Test_Parsers_Isac.thy
-\<close>
-subsection \<open>Specification\<close>
-text \<open>
-  -> Test_Parsers_Isac.thy
-\<close>
-subsection \<open>Solution\<close>
-text \<open>
-  -> Test_Parsers_Isac.thy
-\<close>
-
-subsubsection \<open>Problem - Solution recursively\<close>
-ML \<open>
-\<close> ML \<open>
-\<close> ML \<open>
-\<close> ML \<open>
-\<close> ML \<open>
-\<close> ML \<open>
-\<close>
-
-(**)end (* Missing outer syntax command(s) "ISAC" *)
+(**)end(**)
diff -r 95a20f5bc256 -r a05df90c0dee test/Tools/isac/CLEANUP
--- a/test/Tools/isac/CLEANUP	Tue Jul 28 16:17:42 2020 +0200
+++ b/test/Tools/isac/CLEANUP	Fri Jul 31 12:21:34 2020 +0200
@@ -69,7 +69,7 @@
       rm *.orig~
       rm *.orig~~
       rm *.orig~~~
-     cd .. 
+      cd .. 
     cd SignalProcess
       rm *~
       rm #*
@@ -79,16 +79,35 @@
       rm *.orig~
       rm *.orig~~
       rm *.orig~~~
-     cd .. 
+      cd .. 
     cd .. 
   cd file-depend
-      rm *~
-      rm #*
-      rm .\#*
-      rm *.tar*
-      rm *.orig*
-      cd .. 
+    rm *~
+    rm #*
+    rm .\#*
+    rm *.tar*
+    rm *.orig*
+    cd .. 
   cd libisabelle
+    rm *~
+    rm #*
+    rm .\#*
+    rm *.tar*
+    rm *.orig
+    rm *.orig~
+    rm *.orig~~
+    rm *.orig~~~
+    cd .. 
+  cd test-depend
+    rm *~
+    rm #*
+    rm .\#*
+    rm *.tar*
+    rm *.orig
+    rm *.orig~
+    rm *.orig~~
+    rm *.orig~~~
+    cd testdir1
       rm *~
       rm #*
       rm .\#*
@@ -98,7 +117,7 @@
       rm *.orig~~
       rm *.orig~~~
       cd .. 
-  cd test-depend
+    cd testdirm
       rm *~
       rm #*
       rm .\#*
@@ -107,27 +126,28 @@
       rm *.orig~
       rm *.orig~~
       rm *.orig~~~
-      cd testdir1
-          rm *~
-          rm #*
-          rm .\#*
-          rm *.tar*
-          rm *.orig
-          rm *.orig~
-          rm *.orig~~
-          rm *.orig~~~
-          cd .. 
-      cd testdirm
-          rm *~
-          rm #*
-          rm .\#*
-          rm *.tar*
-          rm *.orig
-          rm *.orig~
-          rm *.orig~~
-          rm *.orig~~~
-          cd .. 
       cd .. 
+    cd .. 
+  cd .. 
+cd Pure
+  rm *~
+  rm #*
+  rm .\#*
+  rm *.tar*
+  rm *.orig
+  rm *.orig~
+  rm *.orig~~
+  rm *.orig~~~
+  cd Isar
+    rm *~
+    rm #*
+    rm .\#*
+    rm *.tar*
+    rm *.orig
+    rm *.orig~
+    rm *.orig~~
+    rm *.orig~~~
+    cd .. 
   cd .. 
 cd Minisubpbl
   rm #*
diff -r 95a20f5bc256 -r a05df90c0dee test/Tools/isac/Test_Isac_Short.thy
--- a/test/Tools/isac/Test_Isac_Short.thy	Tue Jul 28 16:17:42 2020 +0200
+++ b/test/Tools/isac/Test_Isac_Short.thy	Fri Jul 31 12:21:34 2020 +0200
@@ -73,6 +73,12 @@
 (**)"~~/test/Tools/isac/ADDTESTS/session-get_theory/Foo"
 (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
    ADDTESTS/------------------------------------------- see end of tests *)
+(*/--- these work independently, but create problems here ..
+  "~~/test/Pure/Isar/Keyword_ISAC.thy"           (* Malformed theory import, "keywords" ?!? *)
+  "~~/test/Pure/Isar/Keywords_Diag.thy"          (* Malformed theory import, "keywords" ?!? *)
+  "~~/test/Pure/Isar/Test_Parse_Isac.thy"        (* Malformed theory import, "keywords" ?!? *)
+  "~~/test/Pure/Isar/Test_Parsers_Cookbook.thy"  (* Malformed theory import             ?!? *)
+  \--- .. these work independently, but create problems here *)
 (**)"~~/test/Pure/Isar/Test_Parsers"
 (**)"~~/test/Pure/Isar/Test_Parse_Term"
 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)