# HG changeset patch # User Walther Neuper # Date 1290497912 -3600 # Node ID a6ce90b2f06a911e53e575e7c4ea1bab557e5805 # Parent 679dd9ebb17b9da3ae0e69d13c629113623e1788 tuned diff -r 679dd9ebb17b -r a6ce90b2f06a test/Pure/Isar/Struct_Deriv.thy --- a/test/Pure/Isar/Struct_Deriv.thy Thu Nov 18 18:25:05 2010 +0100 +++ b/test/Pure/Isar/Struct_Deriv.thy Tue Nov 23 08:38:32 2010 +0100 @@ -9,16 +9,15 @@ theory Struct_Deriv imports Main begin -text {* contents -1. parsing SDs -1.1. keywords, outer syntax and parser setup +text {* table of contents +1. fun parse for SDs by minimal copy from Isabelle code +1.1. keywords and outer syntax preparing parser setup 1.1.1. keywords according to src/Pure/Isar/keyword.ML 1.1.2. outer syntax according to src/Pure/Isar/outer_syntax.ML -1.1.3. parser setup according to src/Pure/Isar/outer_syntax.ML -1.2. build parser for SD -1.2.1. fun parse by Stefan Berghofer +1.1.3. parser setup according to src/Pure/Isar/isar_syn.ML +1.2. minimalized fun parse by Stefan Berghofer 2. provisional parser for SD -2.1. calc elements to be executed separately +2.1. parsers for the elements of a calculation 2.1.1. named_rule 2.1.2. term_rule 2.1.3. rule @@ -26,15 +25,15 @@ 2.1.5. CASheadline 2.1.6. headline 2.1.7. calcline -2.2. parser for a whole SD -2.2.1. provisional parser setup +2.2. combine the parsers for elements to a whole SD-parser +2.2.1. provisional SD-parser setup 2.2.2. parser applied to example 1 2.2.3. parser applied to example 2 *} -section {* provisional parser setup *} +section {* 1. fun parse for SDs by minimal copy from Isabelle code *} -subsection {* keywords, outer syntax and parser setup *} +subsection {* 1.1. keywords, outer syntax and parser setup *} text {* this is a minimal copy from respective Isabelle sourcefiles, minimal with respect to the goal to parse simple SDs, see ex1, ex2 below. @@ -45,7 +44,7 @@ Problems arising with the simplifications will teach the reasons for the original source. *} -subsubsection {* keywords according to src/Pure/Isar/keyword.ML*} +subsubsection {* 1.1.1. keywords according to src/Pure/Isar/keyword.ML*} ML {* signature KEYWORDC = (*minimal C-copy from KEYWORD*) sig @@ -100,7 +99,7 @@ end; *} -subsubsection {* outer syntax according to src/Pure/Isar/outer_syntax.ML*} +subsubsection {* 1.1.2. outer syntax according to src/Pure/Isar/outer_syntax.ML*} ML {* signature OUTER_SYNTAXC = sig @@ -146,8 +145,8 @@ |> Source.exhaust; end; *} -subsubsection {* parser setup according to src/Pure/Isar/outer_syntax.ML *} -ML {* (*src/Pure/Isar/isar_syn.ML*) +subsubsection {* 1.1.3. parser setup according to src/Pure/Isar/isar_syn.ML *} +ML {* structure Isac_Syn: sig end = struct @@ -172,21 +171,21 @@ (Thy_Header.args >> (Toplevel.print oo Isar_Cmd.init_theory)); (*TODO*) end; *} -subsection {* build parser for SD *} - -subsubsection {* fun parse by Stefan Berghofer *} +subsection {* 1.2. minimalized fun parse by Stefan Berghofer *} text {* see ~/devel/IsaDevWS/IsaDevWS-10/T05_Methods.thy by Stefan Berghofer *} ML {* fun filtered_input str = filter Token.is_proper (Outer_SyntaxC.scan Position.none str); +(*################################ fun parse ###############################################*) fun parse p str = Scan.finite Token.stopper p (filtered_input str); +(*################################ fun parse ###############################################*) *} -section {* provisional parser for SD *} -subsection {* calc elements to be executed separately *} +section {* 2. provisional parser for SD *} +subsection {* 2.1. parsers for the elements of a calculation *} -subsubsection {* named_rule *} +subsubsection {* 2.1.1. named_rule *} ML {* "---1----------------------------------------"; val named_rule' = (Args.$$$ "Calculate" || Args.$$$ "Rewrite" || Args.$$$ "Rewrite_Set" @@ -211,7 +210,7 @@ (*** notebook->ML: Calculate times*) *} -subsubsection {* term_rule *} +subsubsection {* 2.1.2. term_rule *} ML {* "---1----------------------------------------"; val term_rule' = Args.$$$ "THM" -- Parse.term; @@ -227,13 +226,13 @@ (*** notebook->ML: THM (a+x=b)=(x=-a*b)*) *} -subsubsection {* rule *} +subsubsection {* 2.1.3. rule *} ML {* val rule = named_rule || term_rule; *} -subsubsection {* PBLheadline *} +subsubsection {* 2.1.4. PBLheadline *} ML {* "---1----------------------------------------"; val PBLheadline' = Args.$$$ "Problem" -- Args.$$$ "(" -- Args.name -- Args.$$$ "," @@ -268,7 +267,7 @@ *** notebook->ML: Problem (Biegelinie.thy, [setzeRandbedingungen, Biegelinien])*) *} -subsubsection {* CASheadline *} +subsubsection {* 2.1.5. CASheadline *} ML {* "---1----------------------------------------"; val CASheadline' = Args.$$$ "CAS" -- Parse.term; @@ -291,7 +290,7 @@ (*** notebook->ML: solve(x+1=2,x)*) *} -subsubsection {* headline *} +subsubsection {* 2.1.6. headline *} ML {* val headline = (PBLheadline || CASheadline) -- Scan.option rule; @@ -301,7 +300,7 @@ parse headline "CAS \"solve(x+1=2,x)\" THM \"(a+x=b)=(x=-a*b)\" "; *} -subsubsection {* calcline *} +subsubsection {* 2.1.7. calcline *} ML {* "---1----------------------------------------"; val calcline' = Parse.term ; @@ -324,9 +323,9 @@ (*** notebook->ML: "-1 + x = 0"*) *} -subsection {* parser for a whole SD *} +subsection {* 2.2. combine the parsers for elements to a whole SD-parser *} -subsubsection {* provisional parser setup *} +subsubsection {* 2.2.1. provisional SD-parser setup *} text {* Prefixes, which are complete enough to trigger a semantic action, have already be handled by exec*. Thus combining such prefixes allows to drop these prefixes. *} @@ -364,9 +363,11 @@ *} ML {* +(*################################ the parser ##############################################*) val SD = Args.$$$ "calculation" -- Args.$$$ "bullet" -- headline -- (body "") -- (Scan.option (Args.$$$ "Box")); +(*################################ the parser ##############################################*) writeln "---0----------------------------------------"; parse SD "calculation \n\ @@ -411,7 +412,7 @@ *} -subsubsection {* parser applied to example 1 *} +subsubsection {* 2.2.2. parser applied to example 1 *} ML {* val ex1 = "calculation \n\ \ bullet CAS \"solve(x+1=2,x)\" \n\ @@ -430,7 +431,7 @@ parse SD ex1; *} -subsubsection {* parser applied to example 2 *} +subsubsection {* 2.2.3. parser applied to example 2 *} ML {* val ex2 = "calculation \n\ \ bullet Problem (Biegelinie.thy, [Biegelinien]) \n\