1.1 --- a/test/Pure/Isar/Test_Parsers_Cookbook.thy	Fri Jul 17 11:42:20 2020 +0200
     1.2 +++ b/test/Pure/Isar/Test_Parsers_Cookbook.thy	Fri Jul 17 11:48:29 2020 +0200
     1.3 @@ -1,6 +1,8 @@
     1.4 +chapter \<open>Trials derived from NEW Isabelle Cookbook\<close>
     1.5 +
     1.6  theory Test_Parsers_Cookbook
     1.7    imports (** ) Pure ( **) HOL.Complex (*.. for inductive even BELOW*)
     1.8 -keywords (*see chapter \<open>Own trials ..\<close>*)
     1.9 +keywords (*see section \<open>Own trials ..\<close>*)
    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 @@ -15,12 +17,12 @@
    1.14  text \<open> trials on parsing with C.U.'s Isabelle Cookbook
    1.15    outdated:
    1.16    https://web.cs.wpi.edu/~dd/resources_isabelle/isabelle_programming.urban.pdf
    1.17 -  2019
    1.18 +  Isabelle 2019:
    1.19    http://talisker.nms.kcl.ac.uk/cgi-bin/repos.cgi/isabelle-cookbook/raw-file/tip/progtutorial.pdf
    1.20  \<close>
    1.21  
    1.22 -chapter \<open>Work along book\<close>
    1.23 -section \<open>Scan strings\<close>
    1.24 +section \<open>Work along book\<close>
    1.25 +subsection \<open>Scan strings\<close>
    1.26  ML \<open>
    1.27  \<close> ML \<open> (*p.134 \<section>6.1*)
    1.28  ($$ "h") (Symbol.explode "hello")
    1.29 @@ -39,7 +41,7 @@
    1.30  \<close> ML \<open>
    1.31  \<close>
    1.32  
    1.33 -section \<open>Scan token list\<close>
    1.34 +subsection \<open>Scan token list\<close>
    1.35  ML \<open>
    1.36  \<close> ML \<open> (*p.141 \<section>6.2*)
    1.37  Token.explode
    1.38 @@ -85,8 +87,8 @@
    1.39  \<close> ML \<open>
    1.40  \<close>
    1.41  
    1.42 -section \<open>Scan.optional\<close>
    1.43 -subsection \<open>Cookbook Scan.optional p.146 \<section>6.7\<close>
    1.44 +subsection \<open>Scan.optional\<close>
    1.45 +subsubsection \<open>Cookbook Scan.optional p.146 \<section>6.7\<close>
    1.46  inductive      (*.. HOL.Complex required *)
    1.47    even and odd
    1.48  where
    1.49 @@ -170,7 +172,7 @@
    1.50  \<close> ML \<open>
    1.51  \<close>
    1.52  
    1.53 -subsection \<open>src/HOL/Tools/value_command.ML Scan.optional\<close>
    1.54 +subsubsection \<open>src/HOL/Tools/value_command.ML Scan.optional\<close>
    1.55  ML \<open>
    1.56  \<close> ML \<open>
    1.57  val opt_modes =
    1.58 @@ -207,12 +209,12 @@
    1.59  \<close>
    1.60  
    1.61  
    1.62 -chapter \<open>Own trials, NO Parse.cartouche, NO Outer_Syntax.command\<close>
    1.63 +section \<open>Own trials, NO Parse.cartouche, NO Outer_Syntax.command\<close>
    1.64  text \<open>
    1.65    compare test/../Keywords_Diag.thy
    1.66    for adding Parse.cartouche, Outer_Syntax.command
    1.67  \<close>
    1.68 -section \<open>lists\<close>
    1.69 +subsection \<open>lists\<close>
    1.70  ML \<open>
    1.71  \<close> ML \<open> (*p.144 \<section>6.2 -- adapted from above ..*)
    1.72  let
    1.73 @@ -257,7 +259,7 @@
    1.74  \<close> ML \<open>
    1.75  \<close>
    1.76  
    1.77 -section \<open>Problem_headline\<close>
    1.78 +subsection \<open>Problem_headline\<close>
    1.79  ML \<open>
    1.80  val toks = filtered_input (
    1.81    (**)
    1.82 @@ -298,7 +300,7 @@
    1.83  \<close> ML \<open>
    1.84  \<close>
    1.85  
    1.86 -section \<open>Model\<close>
    1.87 +subsection \<open>Model\<close>
    1.88  ML \<open>
    1.89  \<close> ML \<open>
    1.90  val toks = filtered_input (
    1.91 @@ -331,7 +333,7 @@
    1.92  \<close> ML \<open>
    1.93  \<close>
    1.94  
    1.95 -section \<open>References\<close>
    1.96 +subsection \<open>References\<close>
    1.97  ML \<open>
    1.98  \<close> ML \<open>
    1.99  val toks = filtered_input (
   1.100 @@ -362,7 +364,7 @@
   1.101  \<close> ML \<open>
   1.102  \<close>
   1.103  
   1.104 -section \<open>Solution\<close>
   1.105 +subsection \<open>Solution\<close>
   1.106  text \<open>
   1.107    Problem is recursively possible in Solution.
   1.108    for recursive parsers see p.140 \<section>6.2: parse_tree
   1.109 @@ -388,10 +390,10 @@
   1.110  \<close> ML \<open>
   1.111  \<close>
   1.112  
   1.113 -section \<open>Problem: headline + Specification + Solution\<close>
   1.114 -subsection \<open>TOWARDS Specification + Solution general\<close>
   1.115 +subsection \<open>Problem: headline + Specification + Solution\<close>
   1.116 +subsubsection \<open>TOWARDS Specification + Solution general\<close>
   1.117  text \<open>
   1.118 -  COMPARE subsection \<open>Cookbook Scan.optional p.146 \<section>6.7\<close> IN THIS FILE
   1.119 +  COMPARE subsubsection \<open>Cookbook Scan.optional p.146 \<section>6.7\<close> IN THIS FILE
   1.120  \<close>
   1.121  ML \<open>
   1.122  \<close> ML \<open>
   1.123 @@ -464,7 +466,7 @@
   1.124  \<close> ML \<open>
   1.125  \<close>
   1.126  
   1.127 -subsection \<open>Specification + Solution collapsed\<close>
   1.128 +subsubsection \<open>Specification + Solution collapsed\<close>
   1.129  text \<open>
   1.130    The variants of input below should be accepted by the final calc_parser
   1.131  \<close>