1.1 --- a/test/Pure/Isar/Struct_Deriv.thy Thu Nov 18 18:25:05 2010 +0100
1.2 +++ b/test/Pure/Isar/Struct_Deriv.thy Tue Nov 23 08:38:32 2010 +0100
1.3 @@ -9,16 +9,15 @@
1.4 theory Struct_Deriv
1.5 imports Main
1.6 begin
1.7 -text {* contents
1.8 -1. parsing SDs
1.9 -1.1. keywords, outer syntax and parser setup
1.10 +text {* table of contents
1.11 +1. fun parse for SDs by minimal copy from Isabelle code
1.12 +1.1. keywords and outer syntax preparing parser setup
1.13 1.1.1. keywords according to src/Pure/Isar/keyword.ML
1.14 1.1.2. outer syntax according to src/Pure/Isar/outer_syntax.ML
1.15 -1.1.3. parser setup according to src/Pure/Isar/outer_syntax.ML
1.16 -1.2. build parser for SD
1.17 -1.2.1. fun parse by Stefan Berghofer
1.18 +1.1.3. parser setup according to src/Pure/Isar/isar_syn.ML
1.19 +1.2. minimalized fun parse by Stefan Berghofer
1.20 2. provisional parser for SD
1.21 -2.1. calc elements to be executed separately
1.22 +2.1. parsers for the elements of a calculation
1.23 2.1.1. named_rule
1.24 2.1.2. term_rule
1.25 2.1.3. rule
1.26 @@ -26,15 +25,15 @@
1.27 2.1.5. CASheadline
1.28 2.1.6. headline
1.29 2.1.7. calcline
1.30 -2.2. parser for a whole SD
1.31 -2.2.1. provisional parser setup
1.32 +2.2. combine the parsers for elements to a whole SD-parser
1.33 +2.2.1. provisional SD-parser setup
1.34 2.2.2. parser applied to example 1
1.35 2.2.3. parser applied to example 2
1.36 *}
1.37
1.38 -section {* provisional parser setup *}
1.39 +section {* 1. fun parse for SDs by minimal copy from Isabelle code *}
1.40
1.41 -subsection {* keywords, outer syntax and parser setup *}
1.42 +subsection {* 1.1. keywords, outer syntax and parser setup *}
1.43 text {* this is a minimal copy from respective Isabelle sourcefiles,
1.44 minimal with respect to the goal to parse simple SDs, see ex1, ex2 below.
1.45
1.46 @@ -45,7 +44,7 @@
1.47 Problems arising with the simplifications will teach the reasons for the original source.
1.48 *}
1.49
1.50 -subsubsection {* keywords according to src/Pure/Isar/keyword.ML*}
1.51 +subsubsection {* 1.1.1. keywords according to src/Pure/Isar/keyword.ML*}
1.52 ML {*
1.53 signature KEYWORDC = (*minimal C-copy from KEYWORD*)
1.54 sig
1.55 @@ -100,7 +99,7 @@
1.56
1.57 end; *}
1.58
1.59 -subsubsection {* outer syntax according to src/Pure/Isar/outer_syntax.ML*}
1.60 +subsubsection {* 1.1.2. outer syntax according to src/Pure/Isar/outer_syntax.ML*}
1.61 ML {*
1.62 signature OUTER_SYNTAXC =
1.63 sig
1.64 @@ -146,8 +145,8 @@
1.65 |> Source.exhaust;
1.66 end; *}
1.67
1.68 -subsubsection {* parser setup according to src/Pure/Isar/outer_syntax.ML *}
1.69 -ML {* (*src/Pure/Isar/isar_syn.ML*)
1.70 +subsubsection {* 1.1.3. parser setup according to src/Pure/Isar/isar_syn.ML *}
1.71 +ML {*
1.72 structure Isac_Syn: sig end =
1.73 struct
1.74
1.75 @@ -172,21 +171,21 @@
1.76 (Thy_Header.args >> (Toplevel.print oo Isar_Cmd.init_theory)); (*TODO*)
1.77 end; *}
1.78
1.79 -subsection {* build parser for SD *}
1.80 -
1.81 -subsubsection {* fun parse by Stefan Berghofer *}
1.82 +subsection {* 1.2. minimalized fun parse by Stefan Berghofer *}
1.83 text {* see ~/devel/IsaDevWS/IsaDevWS-10/T05_Methods.thy by Stefan Berghofer *}
1.84 ML {*
1.85 fun filtered_input str =
1.86 filter Token.is_proper (Outer_SyntaxC.scan Position.none str);
1.87 +(*################################ fun parse ###############################################*)
1.88 fun parse p str = Scan.finite Token.stopper p (filtered_input str);
1.89 +(*################################ fun parse ###############################################*)
1.90 *}
1.91
1.92
1.93 -section {* provisional parser for SD *}
1.94 -subsection {* calc elements to be executed separately *}
1.95 +section {* 2. provisional parser for SD *}
1.96 +subsection {* 2.1. parsers for the elements of a calculation *}
1.97
1.98 -subsubsection {* named_rule *}
1.99 +subsubsection {* 2.1.1. named_rule *}
1.100 ML {*
1.101 "---1----------------------------------------";
1.102 val named_rule' = (Args.$$$ "Calculate" || Args.$$$ "Rewrite" || Args.$$$ "Rewrite_Set"
1.103 @@ -211,7 +210,7 @@
1.104 (*** notebook->ML: Calculate times*)
1.105 *}
1.106
1.107 -subsubsection {* term_rule *}
1.108 +subsubsection {* 2.1.2. term_rule *}
1.109 ML {*
1.110 "---1----------------------------------------";
1.111 val term_rule' = Args.$$$ "THM" -- Parse.term;
1.112 @@ -227,13 +226,13 @@
1.113 (*** notebook->ML: THM (a+x=b)=(x=-a*b)*)
1.114 *}
1.115
1.116 -subsubsection {* rule *}
1.117 +subsubsection {* 2.1.3. rule *}
1.118 ML {*
1.119 val rule = named_rule || term_rule;
1.120 *}
1.121
1.122
1.123 -subsubsection {* PBLheadline *}
1.124 +subsubsection {* 2.1.4. PBLheadline *}
1.125 ML {*
1.126 "---1----------------------------------------";
1.127 val PBLheadline' = Args.$$$ "Problem" -- Args.$$$ "(" -- Args.name -- Args.$$$ ","
1.128 @@ -268,7 +267,7 @@
1.129 *** notebook->ML: Problem (Biegelinie.thy, [setzeRandbedingungen, Biegelinien])*)
1.130 *}
1.131
1.132 -subsubsection {* CASheadline *}
1.133 +subsubsection {* 2.1.5. CASheadline *}
1.134 ML {*
1.135 "---1----------------------------------------";
1.136 val CASheadline' = Args.$$$ "CAS" -- Parse.term;
1.137 @@ -291,7 +290,7 @@
1.138 (*** notebook->ML: solve(x+1=2,x)*)
1.139 *}
1.140
1.141 -subsubsection {* headline *}
1.142 +subsubsection {* 2.1.6. headline *}
1.143 ML {*
1.144 val headline = (PBLheadline || CASheadline) -- Scan.option rule;
1.145
1.146 @@ -301,7 +300,7 @@
1.147 parse headline "CAS \"solve(x+1=2,x)\" THM \"(a+x=b)=(x=-a*b)\" ";
1.148 *}
1.149
1.150 -subsubsection {* calcline *}
1.151 +subsubsection {* 2.1.7. calcline *}
1.152 ML {*
1.153 "---1----------------------------------------";
1.154 val calcline' = Parse.term ;
1.155 @@ -324,9 +323,9 @@
1.156 (*** notebook->ML: "-1 + x = 0"*)
1.157 *}
1.158
1.159 -subsection {* parser for a whole SD *}
1.160 +subsection {* 2.2. combine the parsers for elements to a whole SD-parser *}
1.161
1.162 -subsubsection {* provisional parser setup *}
1.163 +subsubsection {* 2.2.1. provisional SD-parser setup *}
1.164 text {* Prefixes, which are complete enough to trigger a semantic action,
1.165 have already be handled by exec*.
1.166 Thus combining such prefixes allows to drop these prefixes. *}
1.167 @@ -364,9 +363,11 @@
1.168 *}
1.169
1.170 ML {*
1.171 +(*################################ the parser ##############################################*)
1.172 val SD = Args.$$$ "calculation" -- Args.$$$ "bullet" -- headline
1.173 -- (body "")
1.174 -- (Scan.option (Args.$$$ "Box"));
1.175 +(*################################ the parser ##############################################*)
1.176
1.177 writeln "---0----------------------------------------";
1.178 parse SD "calculation \n\
1.179 @@ -411,7 +412,7 @@
1.180 *}
1.181
1.182
1.183 -subsubsection {* parser applied to example 1 *}
1.184 +subsubsection {* 2.2.2. parser applied to example 1 *}
1.185 ML {*
1.186 val ex1 = "calculation \n\
1.187 \ bullet CAS \"solve(x+1=2,x)\" \n\
1.188 @@ -430,7 +431,7 @@
1.189 parse SD ex1;
1.190 *}
1.191
1.192 -subsubsection {* parser applied to example 2 *}
1.193 +subsubsection {* 2.2.3. parser applied to example 2 *}
1.194 ML {*
1.195 val ex2 = "calculation \n\
1.196 \ bullet Problem (Biegelinie.thy, [Biegelinien]) \n\