1.1 --- a/test/Pure/Isar/Struct_Deriv.thy	Thu Jun 16 18:51:59 2011 +0200
     1.2 +++ b/test/Pure/Isar/Struct_Deriv.thy	Sat Jun 18 11:28:10 2011 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  header {* structured derivations (SD) according to R.J.Back *}
     1.6  
     1.7 -theory Struct_Deriv
     1.8 +theory Struct_Deriv2
     1.9  imports Main
    1.10  begin
    1.11  text {* table of contents
    1.12 @@ -15,7 +15,7 @@
    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/isar_syn.ML
    1.16 -1.2. minimalized fun parse by Stefan Berghofer
    1.17 +1.2. minimalized fun parse by Stefan Berghofer IsaDevWs'10
    1.18  2. provisional parser for SD
    1.19  2.1. parsers for the elements of a calculation
    1.20  2.1.1. named_rule
    1.21 @@ -140,10 +140,11 @@
    1.22  
    1.23  fun scan pos str =
    1.24    Source.of_string str
    1.25 -  |> Symbol.source {do_recover = false}
    1.26 +  |> Symbol.source (*Isabelle2009-2: {do_recover = false}*)
    1.27    |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
    1.28    |> Source.exhaust;
    1.29 -end; *}
    1.30 +end; 
    1.31 +*}
    1.32  
    1.33  subsubsection {* 1.1.3. parser setup according to src/Pure/Isar/isar_syn.ML *}
    1.34  ML {* 
    1.35 @@ -168,8 +169,18 @@
    1.36  
    1.37  val _ =
    1.38    Outer_SyntaxC.command "calculation" "begin calc" (KeywordC.tag_calc KeywordC.calc_begin)
    1.39 -    (Thy_Header.args >> (Toplevel.print oo Isar_Cmd.init_theory)); (*TODO*)
    1.40 -end; *}
    1.41 +    (Thy_Header.args >> (fn (name, imports, uses) =>
    1.42 +      Toplevel.print o
    1.43 +        Toplevel.init_theory NONE name
    1.44 +          (fn master =>
    1.45 +            Thy_Info.toplevel_begin_theory master name imports (map (apfst Path.explode) uses))));
    1.46 +(*was in Isabelle2009-2:
    1.47 +val _ =
    1.48 +  Outer_SyntaxC.command "calculation" "begin calc" (KeywordC.tag_calc KeywordC.calc_begin)
    1.49 +    (Thy_Header.args >> (Toplevel.print oo Isar_Cmd.init_theory));
    1.50 +*)
    1.51 +end;
    1.52 +*}
    1.53  
    1.54  subsection {* 1.2. minimalized fun parse by Stefan Berghofer *}
    1.55  text {* see ~/devel/IsaDevWS/IsaDevWS-10/T05_Methods.thy by Stefan Berghofer *}
    1.56 @@ -342,7 +353,7 @@
    1.57  fun body _ source = 
    1.58     (  Scan.repeat(    Args.$$$ "top" -- calcline -- 
    1.59                          (Scan.repeat (Args.$$$ "equiv" -- calcline)) >> drop_prefixes
    1.60 -(* GOON            || (Scan.repeat (Args.$$$ "equiv" -- calcline))   >> drop_prefixes  *)
    1.61 +(* FIXME:loops     || (Scan.repeat (Args.$$$ "equiv" -- calcline))   >> drop_prefixes  *)
    1.62                     || Args.$$$ "bullet" -- headline -- body ""       >> drop_prefixes
    1.63                   ) 
    1.64        -- level_up
    1.65 @@ -368,11 +379,22 @@
    1.66           -- (body "") 
    1.67           -- (Scan.option (Args.$$$ "Box"));
    1.68  (*################################ the parser ##############################################*)
    1.69 -
    1.70 +*}
    1.71 +ML {*
    1.72 +writeln "---0----------------------------------------";
    1.73 +parse SD ("calculation                      " ^
    1.74 +          "  bullet CAS \"solve(x+1=2,x)\"  " ^
    1.75 +          "  dots \"[x = 1]\"               ");
    1.76 +*}
    1.77 +ML {*
    1.78  writeln "---0----------------------------------------";
    1.79  parse SD "calculation                      \n\
    1.80           \ bullet CAS \"solve(x+1=2,x)\"   \n\
    1.81           \ dots \"[x = 1]\"                ";
    1.82 +*}
    1.83 +
    1.84 +ML {*
    1.85 +
    1.86  writeln "---1-----------------------------------------";
    1.87  parse SD "calculation                              \n\
    1.88           \ bullet CAS \"solve(x+1=2,x)\"           \n\

     2.1 --- a/test/Pure/Isar/args.ML	Thu Jun 16 18:51:59 2011 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,2 +0,0 @@
     2.4 -(*see test/Pure/Isar/Test_Parser.thy
     2.5 -*)

     3.1 --- a/test/Pure/Isar/isar_syn.ML	Thu Jun 16 18:51:59 2011 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,2 +0,0 @@
     3.4 -(*see test/Pure/Isar/Test_Parser.thy
     3.5 -*)

     4.1 --- a/test/Pure/Isar/parse.ML	Thu Jun 16 18:51:59 2011 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,3 +0,0 @@
     4.4 -(*see test/Pure/Isar/Test_Parse_Term.thy
     4.5 -      
     4.6 -*)

     5.1 --- a/test/Pure/Isar/token.ML	Thu Jun 16 18:51:59 2011 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,3 +0,0 @@
     5.4 -(*see test/Pure/Isar/Test_Parse_Term.thy
     5.5 -      
     5.6 -*)