--- a/NEWS Mon May 17 18:59:59 2010 -0700
+++ b/NEWS Tue May 18 06:28:42 2010 -0700
@@ -506,14 +506,18 @@
context actually works, but under normal circumstances one needs to
pass the proper local context through the code!
-* Renamed some important ML structures, while keeping the old names as
-legacy aliases for some time:
-
+* Renamed some important ML structures, while keeping the old names
+for some time as aliases within the structure Legacy:
+
+ OuterKeyword ~> Keyword
+ OuterLex ~> Token
+ OuterParse ~> Parse
OuterSyntax ~> Outer_Syntax
- OuterKeyword ~> Keyword
- OuterParse ~> Parse
SpecParse ~> Parse_Spec
+Note that "open Legacy" simplifies porting of sources, but forgetting
+to remove it again will complicate porting again in the future.
+
*** System ***
--- a/doc-src/antiquote_setup.ML Mon May 17 18:59:59 2010 -0700
+++ b/doc-src/antiquote_setup.ML Tue May 18 06:28:42 2010 -0700
@@ -166,9 +166,9 @@
in
val _ = entity_antiqs no_check "" "syntax";
-val _ = entity_antiqs (K (is_some o OuterKeyword.command_keyword)) "isacommand" "command";
-val _ = entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "keyword";
-val _ = entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "element";
+val _ = entity_antiqs (K (is_some o Keyword.command_keyword)) "isacommand" "command";
+val _ = entity_antiqs (K Keyword.is_keyword) "isakeyword" "keyword";
+val _ = entity_antiqs (K Keyword.is_keyword) "isakeyword" "element";
val _ = entity_antiqs (thy_check Method.intern Method.defined) "" "method";
val _ = entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute";
val _ = entity_antiqs no_check "" "fact";
--- a/doc-src/rail.ML Mon May 17 18:59:59 2010 -0700
+++ b/doc-src/rail.ML Tue May 18 06:28:42 2010 -0700
@@ -59,9 +59,9 @@
(* [(kind, (markup, check, style))*)
Symtab.make [
("syntax", ("", no_check, true)),
- ("command", ("isacommand", K (is_some o OuterKeyword.command_keyword), true)),
- ("keyword", ("isakeyword", K OuterKeyword.is_keyword, true)),
- ("element", ("isakeyword", K OuterKeyword.is_keyword, true)),
+ ("command", ("isacommand", K (is_some o Keyword.command_keyword), true)),
+ ("keyword", ("isakeyword", K Keyword.is_keyword, true)),
+ ("element", ("isakeyword", K Keyword.is_keyword, true)),
("method", ("", thy_check Method.intern Method.defined, true)),
("attribute", ("", thy_check Attrib.intern Attrib.defined, true)),
("fact", ("", no_check, true)),
@@ -473,7 +473,7 @@
|> parse
|> print;
-val _ = ThyOutput.antiquotation "rail" (Scan.lift ( OuterParse.position Args.name ))
+val _ = ThyOutput.antiquotation "rail" (Scan.lift (Parse.position Args.name))
(fn {context = ctxt,...} => fn txt => process txt ctxt);
end;
--- a/src/FOL/ex/Iff_Oracle.thy Mon May 17 18:59:59 2010 -0700
+++ b/src/FOL/ex/Iff_Oracle.thy Tue May 18 06:28:42 2010 -0700
@@ -52,7 +52,7 @@
subsection {* Oracle as proof method *}
method_setup iff = {*
- Scan.lift OuterParse.nat >> (fn n => fn ctxt =>
+ Scan.lift Parse.nat >> (fn n => fn ctxt =>
SIMPLE_METHOD
(HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n)))
handle Fail _ => no_tac))
--- a/src/HOL/Boogie/Tools/boogie_commands.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Tue May 18 06:28:42 2010 -0700
@@ -263,31 +263,31 @@
fun scan_arg f = Args.parens f
fun scan_opt n = Scan.optional (scan_arg (Args.$$$ n >> K true)) false
-val vc_offsets = Scan.optional (Args.bracks (OuterParse.list1
- (OuterParse.string --| Args.colon -- OuterParse.nat))) []
+val vc_offsets = Scan.optional (Args.bracks (Parse.list1
+ (Parse.string --| Args.colon -- Parse.nat))) []
val _ =
- OuterSyntax.command "boogie_open"
+ Outer_Syntax.command "boogie_open"
"Open a new Boogie environment and load a Boogie-generated .b2i file."
- OuterKeyword.thy_decl
- (scan_opt "quiet" -- OuterParse.name -- vc_offsets >>
+ Keyword.thy_decl
+ (scan_opt "quiet" -- Parse.name -- vc_offsets >>
(Toplevel.theory o boogie_open))
-val vc_name = OuterParse.name
+val vc_name = Parse.name
-val vc_label = OuterParse.name
+val vc_label = Parse.name
val vc_labels = Scan.repeat1 vc_label
val vc_paths =
- OuterParse.nat -- (Args.$$$ "-" |-- OuterParse.nat) >> (op upto) ||
- OuterParse.nat >> single
+ Parse.nat -- (Args.$$$ "-" |-- Parse.nat) >> (op upto) ||
+ Parse.nat >> single
val vc_opts =
scan_arg
(scan_val "assertion" vc_label >> VC_Single ||
scan_val "examine" vc_labels >> VC_Examine ||
- scan_val "take" ((OuterParse.list vc_paths >> flat) -- Scan.option (
+ scan_val "take" ((Parse.list vc_paths >> flat) -- Scan.option (
scan_val "without" vc_labels >> pair false ||
scan_val "and_also" vc_labels >> pair true) >> VC_Take) ||
scan_val "only" vc_labels >> VC_Only ||
@@ -295,9 +295,9 @@
Scan.succeed VC_Complete
val _ =
- OuterSyntax.command "boogie_vc"
+ Outer_Syntax.command "boogie_vc"
"Enter into proof mode for a specific verification condition."
- OuterKeyword.thy_goal
+ Keyword.thy_goal
(vc_name -- vc_opts >> (fn args =>
(Toplevel.print o Toplevel.theory_to_proof (boogie_vc args))))
@@ -305,7 +305,7 @@
val quick_timeout = 5
val default_timeout = 20
-fun timeout name = Scan.optional (scan_val name OuterParse.nat)
+fun timeout name = Scan.optional (scan_val name Parse.nat)
val status_test =
scan_arg (
@@ -328,18 +328,18 @@
f (Toplevel.theory_of state))
val _ =
- OuterSyntax.improper_command "boogie_status"
+ Outer_Syntax.improper_command "boogie_status"
"Show the name and state of all loaded verification conditions."
- OuterKeyword.diag
+ Keyword.diag
(status_test >> status_cmd ||
status_vc >> status_cmd ||
Scan.succeed (status_cmd boogie_status))
val _ =
- OuterSyntax.command "boogie_end"
+ Outer_Syntax.command "boogie_end"
"Close the current Boogie environment."
- OuterKeyword.thy_decl
+ Keyword.thy_decl
(Scan.succeed (Toplevel.theory boogie_end))
--- a/src/HOL/Decision_Procs/Approximation.thy Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Decision_Procs/Approximation.thy Tue May 18 06:28:42 2010 -0700
@@ -3310,13 +3310,13 @@
by auto
method_setup approximation = {*
- Scan.lift (OuterParse.nat)
+ Scan.lift Parse.nat
--
Scan.optional (Scan.lift (Args.$$$ "splitting" |-- Args.colon)
- |-- OuterParse.and_list' (free --| Scan.lift (Args.$$$ "=") -- Scan.lift OuterParse.nat)) []
+ |-- Parse.and_list' (free --| Scan.lift (Args.$$$ "=") -- Scan.lift Parse.nat)) []
--
Scan.option (Scan.lift (Args.$$$ "taylor" |-- Args.colon)
- |-- (free |-- Scan.lift (Args.$$$ "=") |-- Scan.lift OuterParse.nat))
+ |-- (free |-- Scan.lift (Args.$$$ "=") |-- Scan.lift Parse.nat))
>>
(fn ((prec, splitting), taylor) => fn ctxt =>
SIMPLE_METHOD' (fn i =>
--- a/src/HOL/Import/import_syntax.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Import/import_syntax.ML Tue May 18 06:28:42 2010 -0700
@@ -4,26 +4,23 @@
signature HOL4_IMPORT_SYNTAX =
sig
- type token = OuterLex.token
- type command = token list -> (theory -> theory) * token list
-
- val import_segment: token list -> (theory -> theory) * token list
- val import_theory : token list -> (theory -> theory) * token list
- val end_import : token list -> (theory -> theory) * token list
-
- val setup_theory : token list -> (theory -> theory) * token list
- val end_setup : token list -> (theory -> theory) * token list
+ val import_segment: (theory -> theory) parser
+ val import_theory : (theory -> theory) parser
+ val end_import : (theory -> theory) parser
+
+ val setup_theory : (theory -> theory) parser
+ val end_setup : (theory -> theory) parser
+
+ val thm_maps : (theory -> theory) parser
+ val ignore_thms : (theory -> theory) parser
+ val type_maps : (theory -> theory) parser
+ val def_maps : (theory -> theory) parser
+ val const_maps : (theory -> theory) parser
+ val const_moves : (theory -> theory) parser
+ val const_renames : (theory -> theory) parser
- val thm_maps : token list -> (theory -> theory) * token list
- val ignore_thms : token list -> (theory -> theory) * token list
- val type_maps : token list -> (theory -> theory) * token list
- val def_maps : token list -> (theory -> theory) * token list
- val const_maps : token list -> (theory -> theory) * token list
- val const_moves : token list -> (theory -> theory) * token list
- val const_renames : token list -> (theory -> theory) * token list
-
- val skip_import_dir : token list -> (theory -> theory) * token list
- val skip_import : token list -> (theory -> theory) * token list
+ val skip_import_dir : (theory -> theory) parser
+ val skip_import : (theory -> theory) parser
val setup : unit -> unit
end
@@ -31,28 +28,23 @@
structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX =
struct
-type token = OuterLex.token
-type command = token list -> (theory -> theory) * token list
-
-local structure P = OuterParse and K = OuterKeyword in
-
(* Parsers *)
-val import_segment = P.name >> set_import_segment
+val import_segment = Parse.name >> set_import_segment
-val import_theory = P.name >> (fn thyname =>
+val import_theory = Parse.name >> (fn thyname =>
fn thy =>
thy |> set_generating_thy thyname
|> Sign.add_path thyname
|> add_dump (";setup_theory " ^ thyname))
fun do_skip_import_dir s = (ImportRecorder.set_skip_import_dir (SOME s); I)
-val skip_import_dir : command = P.string >> do_skip_import_dir
+val skip_import_dir = Parse.string >> do_skip_import_dir
val lower = String.map Char.toLower
fun do_skip_import s = (ImportRecorder.set_skip_import (case lower s of "on" => true | "off" => false | _ => Scan.fail ()); I)
-val skip_import : command = P.short_ident >> do_skip_import
+val skip_import = Parse.short_ident >> do_skip_import
fun end_import toks =
Scan.succeed
@@ -84,7 +76,7 @@
|> add_dump ";end_setup"
end) toks
-val ignore_thms = Scan.repeat1 P.name
+val ignore_thms = Scan.repeat1 Parse.name
>> (fn ignored =>
fn thy =>
let
@@ -93,7 +85,7 @@
Library.foldl (fn (thy,thmname) => ignore_hol4 thyname thmname thy) (thy,ignored)
end)
-val thm_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
+val thm_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
>> (fn thmmaps =>
fn thy =>
let
@@ -102,7 +94,7 @@
Library.foldl (fn (thy,(hol,isa)) => add_hol4_mapping thyname hol isa thy) (thy,thmmaps)
end)
-val type_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
+val type_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
>> (fn typmaps =>
fn thy =>
let
@@ -111,7 +103,7 @@
Library.foldl (fn (thy,(hol,isa)) => add_hol4_type_mapping thyname hol false isa thy) (thy,typmaps)
end)
-val def_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
+val def_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname)
>> (fn defmaps =>
fn thy =>
let
@@ -120,7 +112,7 @@
Library.foldl (fn (thy,(hol,isa)) => add_defmap thyname hol isa thy) (thy,defmaps)
end)
-val const_renames = Scan.repeat1 (P.name --| P.$$$ ">" -- P.name)
+val const_renames = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.name)
>> (fn renames =>
fn thy =>
let
@@ -129,7 +121,7 @@
Library.foldl (fn (thy,(hol,isa)) => add_hol4_const_renaming thyname hol isa thy) (thy,renames)
end)
-val const_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
+val const_maps = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ))
>> (fn constmaps =>
fn thy =>
let
@@ -139,7 +131,7 @@
| (thy,((hol,isa),SOME ty)) => add_hol4_const_wt_mapping thyname hol false isa (Syntax.read_typ_global thy ty) thy) (thy,constmaps)
end)
-val const_moves = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
+val const_moves = Scan.repeat1 (Parse.name --| Parse.$$$ ">" -- Parse.xname -- Scan.option (Parse.$$$ "::" |-- Parse.typ))
>> (fn constmaps =>
fn thy =>
let
@@ -160,18 +152,18 @@
(Scan.make_lexicon (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]),
Scan.empty_lexicon)
val get_lexes = fn () => !lexes
- val token_source = OuterLex.source {do_recover = NONE} get_lexes Position.start symb_source
- val token_list = filter_out (OuterLex.is_kind OuterLex.Space) (Source.exhaust token_source)
- val import_segmentP = OuterParse.$$$ "import_segment" |-- import_segment
- val type_mapsP = OuterParse.$$$ "type_maps" |-- type_maps
- val def_mapsP = OuterParse.$$$ "def_maps" |-- def_maps
- val const_mapsP = OuterParse.$$$ "const_maps" |-- const_maps
- val const_movesP = OuterParse.$$$ "const_moves" |-- const_moves
- val const_renamesP = OuterParse.$$$ "const_renames" |-- const_renames
- val ignore_thmsP = OuterParse.$$$ "ignore_thms" |-- ignore_thms
- val thm_mapsP = OuterParse.$$$ "thm_maps" |-- thm_maps
+ val token_source = Token.source {do_recover = NONE} get_lexes Position.start symb_source
+ val token_list = filter_out (Token.is_kind Token.Space) (Source.exhaust token_source)
+ val import_segmentP = Parse.$$$ "import_segment" |-- import_segment
+ val type_mapsP = Parse.$$$ "type_maps" |-- type_maps
+ val def_mapsP = Parse.$$$ "def_maps" |-- def_maps
+ val const_mapsP = Parse.$$$ "const_maps" |-- const_maps
+ val const_movesP = Parse.$$$ "const_moves" |-- const_moves
+ val const_renamesP = Parse.$$$ "const_renames" |-- const_renames
+ val ignore_thmsP = Parse.$$$ "ignore_thms" |-- ignore_thms
+ val thm_mapsP = Parse.$$$ "thm_maps" |-- thm_maps
val parser = type_mapsP || def_mapsP || const_mapsP || const_movesP || const_renamesP || thm_mapsP || ignore_thmsP || import_segmentP
- val importP = OuterParse.$$$ "import" |-- Scan.repeat parser --| OuterParse.$$$ "end"
+ val importP = Parse.$$$ "import" |-- Scan.repeat parser --| Parse.$$$ "end"
fun apply [] thy = thy
| apply (f::fs) thy = apply fs (f thy)
in
@@ -194,7 +186,7 @@
NONE => error "Import data already cleared - forgotten a setup_theory?"
| SOME _ => ImportData.put NONE thy
-val setup_theory = P.name
+val setup_theory = Parse.name
>>
(fn thyname =>
fn thy =>
@@ -218,64 +210,62 @@
|> Sign.parent_path
end) toks
-val set_dump = P.string -- P.string >> setup_dump
+val set_dump = Parse.string -- Parse.string >> setup_dump
fun fl_dump toks = Scan.succeed flush_dump toks
-val append_dump = (P.verbatim || P.string) >> add_dump
+val append_dump = (Parse.verbatim || Parse.string) >> add_dump
fun setup () =
- (OuterKeyword.keyword ">";
- OuterSyntax.command "import_segment"
+ (Keyword.keyword ">";
+ Outer_Syntax.command "import_segment"
"Set import segment name"
- K.thy_decl (import_segment >> Toplevel.theory);
- OuterSyntax.command "import_theory"
+ Keyword.thy_decl (import_segment >> Toplevel.theory);
+ Outer_Syntax.command "import_theory"
"Set default HOL4 theory name"
- K.thy_decl (import_theory >> Toplevel.theory);
- OuterSyntax.command "end_import"
+ Keyword.thy_decl (import_theory >> Toplevel.theory);
+ Outer_Syntax.command "end_import"
"End HOL4 import"
- K.thy_decl (end_import >> Toplevel.theory);
- OuterSyntax.command "skip_import_dir"
+ Keyword.thy_decl (end_import >> Toplevel.theory);
+ Outer_Syntax.command "skip_import_dir"
"Sets caching directory for skipping importing"
- K.thy_decl (skip_import_dir >> Toplevel.theory);
- OuterSyntax.command "skip_import"
+ Keyword.thy_decl (skip_import_dir >> Toplevel.theory);
+ Outer_Syntax.command "skip_import"
"Switches skipping importing on or off"
- K.thy_decl (skip_import >> Toplevel.theory);
- OuterSyntax.command "setup_theory"
+ Keyword.thy_decl (skip_import >> Toplevel.theory);
+ Outer_Syntax.command "setup_theory"
"Setup HOL4 theory replaying"
- K.thy_decl (setup_theory >> Toplevel.theory);
- OuterSyntax.command "end_setup"
+ Keyword.thy_decl (setup_theory >> Toplevel.theory);
+ Outer_Syntax.command "end_setup"
"End HOL4 setup"
- K.thy_decl (end_setup >> Toplevel.theory);
- OuterSyntax.command "setup_dump"
+ Keyword.thy_decl (end_setup >> Toplevel.theory);
+ Outer_Syntax.command "setup_dump"
"Setup the dump file name"
- K.thy_decl (set_dump >> Toplevel.theory);
- OuterSyntax.command "append_dump"
+ Keyword.thy_decl (set_dump >> Toplevel.theory);
+ Outer_Syntax.command "append_dump"
"Add text to dump file"
- K.thy_decl (append_dump >> Toplevel.theory);
- OuterSyntax.command "flush_dump"
+ Keyword.thy_decl (append_dump >> Toplevel.theory);
+ Outer_Syntax.command "flush_dump"
"Write the dump to file"
- K.thy_decl (fl_dump >> Toplevel.theory);
- OuterSyntax.command "ignore_thms"
+ Keyword.thy_decl (fl_dump >> Toplevel.theory);
+ Outer_Syntax.command "ignore_thms"
"Theorems to ignore in next HOL4 theory import"
- K.thy_decl (ignore_thms >> Toplevel.theory);
- OuterSyntax.command "type_maps"
+ Keyword.thy_decl (ignore_thms >> Toplevel.theory);
+ Outer_Syntax.command "type_maps"
"Map HOL4 type names to existing Isabelle/HOL type names"
- K.thy_decl (type_maps >> Toplevel.theory);
- OuterSyntax.command "def_maps"
+ Keyword.thy_decl (type_maps >> Toplevel.theory);
+ Outer_Syntax.command "def_maps"
"Map HOL4 constant names to their primitive definitions"
- K.thy_decl (def_maps >> Toplevel.theory);
- OuterSyntax.command "thm_maps"
+ Keyword.thy_decl (def_maps >> Toplevel.theory);
+ Outer_Syntax.command "thm_maps"
"Map HOL4 theorem names to existing Isabelle/HOL theorem names"
- K.thy_decl (thm_maps >> Toplevel.theory);
- OuterSyntax.command "const_renames"
+ Keyword.thy_decl (thm_maps >> Toplevel.theory);
+ Outer_Syntax.command "const_renames"
"Rename HOL4 const names"
- K.thy_decl (const_renames >> Toplevel.theory);
- OuterSyntax.command "const_moves"
+ Keyword.thy_decl (const_renames >> Toplevel.theory);
+ Outer_Syntax.command "const_moves"
"Rename HOL4 const names to other HOL4 constants"
- K.thy_decl (const_moves >> Toplevel.theory);
- OuterSyntax.command "const_maps"
+ Keyword.thy_decl (const_moves >> Toplevel.theory);
+ Outer_Syntax.command "const_maps"
"Map HOL4 const names to existing Isabelle/HOL const names"
- K.thy_decl (const_maps >> Toplevel.theory));
+ Keyword.thy_decl (const_maps >> Toplevel.theory));
end
-
-end
--- a/src/HOL/Import/proof_kernel.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Import/proof_kernel.ML Tue May 18 06:28:42 2010 -0700
@@ -189,7 +189,7 @@
else Delimfix (Syntax.escape c)
fun quotename c =
- if Syntax.is_identifier c andalso not (OuterKeyword.is_keyword c) then c else quote c
+ if Syntax.is_identifier c andalso not (Keyword.is_keyword c) then c else quote c
fun simple_smart_string_of_cterm ct =
let
--- a/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML Tue May 18 06:28:42 2010 -0700
@@ -144,11 +144,11 @@
val setup =
Method.setup @{binding sos}
- (Scan.lift (Scan.option OuterParse.xname)
+ (Scan.lift (Scan.option Parse.xname)
>> (sos_solver print_cert o Sum_Of_Squares.Prover o call_solver))
"prove universal problems over the reals using sums of squares" #>
Method.setup @{binding sos_cert}
- (Scan.lift OuterParse.string
+ (Scan.lift Parse.string
>> (fn cert => fn ctxt =>
sos_solver ignore
(Sum_Of_Squares.Certificate (PositivstellensatzTools.cert_to_pss_tree ctxt cert)) ctxt))
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue May 18 06:28:42 2010 -0700
@@ -330,14 +330,14 @@
fun thms_of_name ctxt name =
let
- val lex = OuterKeyword.get_lexicons
+ val lex = Keyword.get_lexicons
val get = maps (ProofContext.get_fact ctxt o fst)
in
Source.of_string name
|> Symbol.source {do_recover=false}
- |> OuterLex.source {do_recover=SOME false} lex Position.start
- |> OuterLex.source_proper
- |> Source.source OuterLex.stopper (Parse_Spec.xthms1 >> get) NONE
+ |> Token.source {do_recover=SOME false} lex Position.start
+ |> Token.source_proper
+ |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
|> Source.exhaust
end
--- a/src/HOL/Nominal/nominal_atoms.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Nominal/nominal_atoms.ML Tue May 18 06:28:42 2010 -0700
@@ -1004,10 +1004,10 @@
(* syntax und parsing *)
-structure P = OuterParse and K = OuterKeyword;
+structure P = Parse and K = Keyword;
val _ =
- OuterSyntax.command "atom_decl" "Declare new kinds of atoms" K.thy_decl
- (Scan.repeat1 P.name >> (Toplevel.theory o create_nom_typedecls));
+ Outer_Syntax.command "atom_decl" "declare new kinds of atoms" Keyword.thy_decl
+ (Scan.repeat1 Parse.name >> (Toplevel.theory o create_nom_typedecls));
end;
--- a/src/HOL/Nominal/nominal_datatype.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Nominal/nominal_datatype.ML Tue May 18 06:28:42 2010 -0700
@@ -2076,11 +2076,10 @@
(* FIXME: The following stuff should be exported by Datatype *)
-local structure P = OuterParse and K = OuterKeyword in
-
val datatype_decl =
- Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_mixfix --
- (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
+ Scan.option (Parse.$$$ "(" |-- Parse.name --| Parse.$$$ ")") --
+ Parse.type_args -- Parse.name -- Parse.opt_mixfix --
+ (Parse.$$$ "=" |-- Parse.enum1 "|" (Parse.name -- Scan.repeat Parse.typ -- Parse.opt_mixfix));
fun mk_datatype args =
let
@@ -2090,9 +2089,7 @@
in add_nominal_datatype Datatype.default_config names specs end;
val _ =
- OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl
- (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
-
-end;
+ Outer_Syntax.command "nominal_datatype" "define inductive datatypes" Keyword.thy_decl
+ (Parse.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
end
--- a/src/HOL/Nominal/nominal_induct.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Nominal/nominal_induct.ML Tue May 18 06:28:42 2010 -0700
@@ -138,8 +138,6 @@
local
-structure P = OuterParse;
-
val avoidingN = "avoiding";
val fixingN = "arbitrary"; (* to be consistent with induct; hopefully this changes again *)
val ruleN = "rule";
@@ -165,14 +163,14 @@
Scan.repeat (unless_more_args free)) [];
val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN -- Args.colon) |--
- P.and_list' (Scan.repeat (unless_more_args free))) [];
+ Parse.and_list' (Scan.repeat (unless_more_args free))) [];
val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms;
in
val nominal_induct_method =
- Args.mode Induct.no_simpN -- (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
+ Args.mode Induct.no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
avoiding -- fixing -- rule_spec) >>
(fn (no_simp, (((x, y), z), w)) => fn ctxt =>
RAW_METHOD_CASES (fn facts =>
--- a/src/HOL/Nominal/nominal_inductive.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Nominal/nominal_inductive.ML Tue May 18 06:28:42 2010 -0700
@@ -672,23 +672,20 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = OuterKeyword.keyword "avoids";
+val _ = Keyword.keyword "avoids";
val _ =
- OuterSyntax.local_theory_to_proof "nominal_inductive"
- "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
- (P.xname -- Scan.optional (P.$$$ "avoids" |-- P.and_list1 (P.name --
- (P.$$$ ":" |-- Scan.repeat1 P.name))) [] >> (fn (name, avoids) =>
+ Outer_Syntax.local_theory_to_proof "nominal_inductive"
+ "prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
+ Keyword.thy_goal
+ (Parse.xname -- Scan.optional (Parse.$$$ "avoids" |-- Parse.and_list1 (Parse.name --
+ (Parse.$$$ ":" |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
prove_strong_ind name avoids));
val _ =
- OuterSyntax.local_theory "equivariance"
- "prove equivariance for inductive predicate involving nominal datatypes" K.thy_decl
- (P.xname -- Scan.optional (P.$$$ "[" |-- P.list1 P.name --| P.$$$ "]") [] >>
+ Outer_Syntax.local_theory "equivariance"
+ "prove equivariance for inductive predicate involving nominal datatypes" Keyword.thy_decl
+ (Parse.xname -- Scan.optional (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]") [] >>
(fn (name, atoms) => prove_eqvt name atoms));
-end;
-
end
--- a/src/HOL/Nominal/nominal_inductive2.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Nominal/nominal_inductive2.ML Tue May 18 06:28:42 2010 -0700
@@ -485,17 +485,14 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
val _ =
- OuterSyntax.local_theory_to_proof "nominal_inductive2"
- "prove strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
- (P.xname --
- Scan.option (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) --
- (Scan.optional (P.$$$ "avoids" |-- P.enum1 "|" (P.name --
- (P.$$$ ":" |-- P.and_list1 P.term))) []) >> (fn ((name, rule_name), avoids) =>
+ Outer_Syntax.local_theory_to_proof "nominal_inductive2"
+ "prove strong induction theorem for inductive predicate involving nominal datatypes"
+ Keyword.thy_goal
+ (Parse.xname --
+ Scan.option (Parse.$$$ "(" |-- Parse.!!! (Parse.name --| Parse.$$$ ")")) --
+ (Scan.optional (Parse.$$$ "avoids" |-- Parse.enum1 "|" (Parse.name --
+ (Parse.$$$ ":" |-- Parse.and_list1 Parse.term))) []) >> (fn ((name, rule_name), avoids) =>
prove_strong_ind name rule_name avoids));
-end;
-
end
--- a/src/HOL/Nominal/nominal_primrec.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Nominal/nominal_primrec.ML Tue May 18 06:28:42 2010 -0700
@@ -393,28 +393,24 @@
(* outer syntax *)
-local structure P = OuterParse in
-
-val freshness_context = P.reserved "freshness_context";
-val invariant = P.reserved "invariant";
+val freshness_context = Parse.reserved "freshness_context";
+val invariant = Parse.reserved "invariant";
-fun unless_flag scan = Scan.unless ((freshness_context || invariant) -- P.$$$ ":") scan;
+fun unless_flag scan = Scan.unless ((freshness_context || invariant) -- Parse.$$$ ":") scan;
-val parser1 = (freshness_context -- P.$$$ ":") |-- unless_flag P.term >> SOME;
-val parser2 = (invariant -- P.$$$ ":") |--
- (Scan.repeat1 (unless_flag P.term) >> SOME) -- Scan.optional parser1 NONE ||
+val parser1 = (freshness_context -- Parse.$$$ ":") |-- unless_flag Parse.term >> SOME;
+val parser2 = (invariant -- Parse.$$$ ":") |--
+ (Scan.repeat1 (unless_flag Parse.term) >> SOME) -- Scan.optional parser1 NONE ||
(parser1 >> pair NONE);
val options =
- Scan.optional (P.$$$ "(" |-- P.!!! (parser2 --| P.$$$ ")")) (NONE, NONE);
+ Scan.optional (Parse.$$$ "(" |-- Parse.!!! (parser2 --| Parse.$$$ ")")) (NONE, NONE);
val _ =
- OuterSyntax.local_theory_to_proof "nominal_primrec"
- "define primitive recursive functions on nominal datatypes" OuterKeyword.thy_goal
- (options -- P.fixes -- P.for_fixes -- Parse_Spec.where_alt_specs
+ Outer_Syntax.local_theory_to_proof "nominal_primrec"
+ "define primitive recursive functions on nominal datatypes" Keyword.thy_goal
+ (options -- Parse.fixes -- Parse.for_fixes -- Parse_Spec.where_alt_specs
>> (fn ((((invs, fctxt), fixes), params), specs) =>
add_primrec_cmd invs fctxt fixes params specs));
end;
-end;
-
--- a/src/HOL/Orderings.thy Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Orderings.thy Tue May 18 06:28:42 2010 -0700
@@ -422,8 +422,8 @@
(** Diagnostic command **)
val _ =
- OuterSyntax.improper_command "print_orders"
- "print order structures available to transitivity reasoner" OuterKeyword.diag
+ Outer_Syntax.improper_command "print_orders"
+ "print order structures available to transitivity reasoner" Keyword.diag
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
Toplevel.keep (print_structures o Toplevel.context_of)));
--- a/src/HOL/Statespace/state_space.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Statespace/state_space.ML Tue May 18 06:28:42 2010 -0700
@@ -32,10 +32,9 @@
(string * typ) list -> theory -> theory
val statespace_decl :
- OuterParse.token list ->
((string list * bstring) *
((string list * xstring * (bstring * bstring) list) list *
- (bstring * string) list)) * OuterParse.token list
+ (bstring * string) list)) parser
val neq_x_y : Proof.context -> term -> term -> thm option
@@ -668,37 +667,33 @@
(*** outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
val type_insts =
- P.typ >> single ||
- P.$$$ "(" |-- P.!!! (P.list1 P.typ --| P.$$$ ")")
+ Parse.typ >> single ||
+ Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.typ --| Parse.$$$ ")")
-val comp = P.name -- (P.$$$ "::" |-- P.!!! P.typ);
+val comp = Parse.name -- (Parse.$$$ "::" |-- Parse.!!! Parse.typ);
fun plus1_unless test scan =
- scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
+ scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
-val mapsto = P.$$$ "=";
-val rename = P.name -- (mapsto |-- P.name);
-val renames = Scan.optional (P.$$$ "[" |-- P.!!! (P.list1 rename --| P.$$$ "]")) [];
+val mapsto = Parse.$$$ "=";
+val rename = Parse.name -- (mapsto |-- Parse.name);
+val renames = Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.list1 rename --| Parse.$$$ "]")) [];
-val parent = ((type_insts -- P.xname) || (P.xname >> pair [])) -- renames
+val parent = ((type_insts -- Parse.xname) || (Parse.xname >> pair [])) -- renames
>> (fn ((insts,name),renames) => (insts,name,renames))
val statespace_decl =
- P.type_args -- P.name --
- (P.$$$ "=" |--
+ Parse.type_args -- Parse.name --
+ (Parse.$$$ "=" |--
((Scan.repeat1 comp >> pair []) ||
(plus1_unless comp parent --
- Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 comp)) [])))
+ Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 comp)) [])))
val statespace_command =
- OuterSyntax.command "statespace" "define state space" K.thy_decl
+ Outer_Syntax.command "statespace" "define state space" Keyword.thy_decl
(statespace_decl >> (fn ((args,name),(parents,comps)) =>
Toplevel.theory (define_statespace args name parents comps)))
-end;
-
end;
\ No newline at end of file
--- a/src/HOL/Tools/Datatype/datatype.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Datatype/datatype.ML Tue May 18 06:28:42 2010 -0700
@@ -721,8 +721,6 @@
local
-structure P = OuterParse and K = OuterKeyword
-
fun prep_datatype_decls args =
let
val names = map
@@ -732,15 +730,16 @@
in (names, specs) end;
val parse_datatype_decl =
- (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_mixfix --
- (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix)));
+ (Scan.option (Parse.$$$ "(" |-- Parse.name --| Parse.$$$ ")") --
+ Parse.type_args -- Parse.binding -- Parse.opt_mixfix --
+ (Parse.$$$ "=" |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat Parse.typ -- Parse.opt_mixfix)));
-val parse_datatype_decls = P.and_list1 parse_datatype_decl >> prep_datatype_decls;
+val parse_datatype_decls = Parse.and_list1 parse_datatype_decl >> prep_datatype_decls;
in
val _ =
- OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
+ Outer_Syntax.command "datatype" "define inductive datatypes" Keyword.thy_decl
(parse_datatype_decls >> (fn (names, specs) => Toplevel.theory (datatype_cmd names specs)));
end;
--- a/src/HOL/Tools/Datatype/datatype_data.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Tue May 18 06:28:42 2010 -0700
@@ -455,18 +455,11 @@
(* outer syntax *)
-local
-
-structure P = OuterParse and K = OuterKeyword
-
-in
-
val _ =
- OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_goal
- (Scan.option (P.$$$ "(" |-- Scan.repeat1 P.name --| P.$$$ ")") -- Scan.repeat1 P.term
- >> (fn (alt_names, ts) => Toplevel.print
- o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts)));
+ Outer_Syntax.command "rep_datatype" "represent existing types inductively" Keyword.thy_goal
+ (Scan.option (Parse.$$$ "(" |-- Scan.repeat1 Parse.name --| Parse.$$$ ")") --
+ Scan.repeat1 Parse.term
+ >> (fn (alt_names, ts) =>
+ Toplevel.print o Toplevel.theory_to_proof (rep_datatype_cmd alt_names ts)));
end;
-
-end;
--- a/src/HOL/Tools/Function/fun.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Function/fun.ML Tue May 18 06:28:42 2010 -0700
@@ -159,13 +159,10 @@
-local structure P = OuterParse and K = OuterKeyword in
-
val _ =
- OuterSyntax.local_theory "fun" "define general recursive functions (short version)" K.thy_decl
+ Outer_Syntax.local_theory "fun" "define general recursive functions (short version)"
+ Keyword.thy_decl
(function_parser fun_config
- >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config));
+ >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
end
-
-end
--- a/src/HOL/Tools/Function/function.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Function/function.ML Tue May 18 06:28:42 2010 -0700
@@ -274,20 +274,19 @@
fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t
|> the_single |> snd
+
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
val _ =
- OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal
+ Outer_Syntax.local_theory_to_proof "function" "define general recursive functions"
+ Keyword.thy_goal
(function_parser default_config
>> (fn ((config, fixes), statements) => function_cmd fixes statements config))
val _ =
- OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal
- (Scan.option P.term >> termination_cmd)
-
-end
+ Outer_Syntax.local_theory_to_proof "termination" "prove termination of a recursive function"
+ Keyword.thy_goal
+ (Scan.option Parse.term >> termination_cmd)
end
--- a/src/HOL/Tools/Function/function_common.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Function/function_common.ML Tue May 18 06:28:42 2010 -0700
@@ -341,21 +341,19 @@
local
- structure P = OuterParse and K = OuterKeyword
-
- val option_parser = P.group "option"
- ((P.reserved "sequential" >> K Sequential)
- || ((P.reserved "default" |-- P.term) >> Default)
- || (P.reserved "domintros" >> K DomIntros)
- || (P.reserved "no_partials" >> K No_Partials)
- || (P.reserved "tailrec" >> K Tailrec))
+ val option_parser = Parse.group "option"
+ ((Parse.reserved "sequential" >> K Sequential)
+ || ((Parse.reserved "default" |-- Parse.term) >> Default)
+ || (Parse.reserved "domintros" >> K DomIntros)
+ || (Parse.reserved "no_partials" >> K No_Partials)
+ || (Parse.reserved "tailrec" >> K Tailrec))
fun config_parser default =
- (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") [])
+ (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") [])
>> (fn opts => fold apply_opt opts default)
in
fun function_parser default_cfg =
- config_parser default_cfg -- P.fixes -- Parse_Spec.where_alt_specs
+ config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs
end
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue May 18 06:28:42 2010 -0700
@@ -24,8 +24,6 @@
open Nitpick_Nut
open Nitpick
-structure K = OuterKeyword and P = OuterParse
-
val auto = Unsynchronized.ref false;
val _ =
@@ -289,14 +287,14 @@
extract_params (ProofContext.init_global thy) false (default_raw_params thy)
o map (apsnd single)
-val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
+val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
val parse_value =
- Scan.repeat1 (P.minus >> single
- || Scan.repeat1 (Scan.unless P.minus P.name)
- || P.$$$ "," |-- P.number >> prefix "," >> single) >> flat
-val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) []
+ Scan.repeat1 (Parse.minus >> single
+ || Scan.repeat1 (Scan.unless Parse.minus Parse.name)
+ || Parse.$$$ "," |-- Parse.number >> prefix "," >> single) >> flat
+val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
val parse_params =
- Scan.optional (P.$$$ "[" |-- P.list parse_param --| P.$$$ "]") []
+ Scan.optional (Parse.$$$ "[" |-- Parse.list parse_param --| Parse.$$$ "]") []
fun handle_exceptions ctxt f x =
f x
@@ -375,15 +373,15 @@
|> sort_strings |> cat_lines)))))
val parse_nitpick_command =
- (parse_params -- Scan.optional P.nat 1) #>> nitpick_trans
+ (parse_params -- Scan.optional Parse.nat 1) #>> nitpick_trans
val parse_nitpick_params_command = parse_params #>> nitpick_params_trans
-val _ = OuterSyntax.improper_command "nitpick"
+val _ = Outer_Syntax.improper_command "nitpick"
"try to find a counterexample for a given subgoal using Nitpick"
- K.diag parse_nitpick_command
-val _ = OuterSyntax.command "nitpick_params"
+ Keyword.diag parse_nitpick_command
+val _ = Outer_Syntax.command "nitpick_params"
"set and display the default parameters for Nitpick"
- K.thy_decl parse_nitpick_params_command
+ Keyword.thy_decl parse_nitpick_params_command
fun auto_nitpick state =
if not (!auto) then (false, state) else pick_nits [] true 1 0 state
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Tue May 18 06:28:42 2010 -0700
@@ -192,8 +192,6 @@
val setup = Predicate_Compile_Core.setup
-local structure P = OuterParse
-in
(* Parser for mode annotations *)
@@ -207,15 +205,15 @@
(parse_mode_tuple_expr --| Args.$$$ "=>" -- parse_mode_expr >> Fun || parse_mode_tuple_expr) xs
val mode_and_opt_proposal = parse_mode_expr --
- Scan.optional (Args.$$$ "as" |-- P.xname >> SOME) NONE
+ Scan.optional (Args.$$$ "as" |-- Parse.xname >> SOME) NONE
val opt_modes =
- Scan.optional (P.$$$ "(" |-- Args.$$$ "modes" |-- P.$$$ ":" |--
- P.enum "," mode_and_opt_proposal --| P.$$$ ")" >> SOME) NONE
+ Scan.optional (Parse.$$$ "(" |-- Args.$$$ "modes" |-- Parse.$$$ ":" |--
+ Parse.enum "," mode_and_opt_proposal --| Parse.$$$ ")" >> SOME) NONE
val opt_expected_modes =
- Scan.optional (P.$$$ "(" |-- Args.$$$ "expected_modes" |-- P.$$$ ":" |--
- P.enum "," parse_mode_expr --| P.$$$ ")" >> SOME) NONE
+ Scan.optional (Parse.$$$ "(" |-- Args.$$$ "expected_modes" |-- Parse.$$$ ":" |--
+ Parse.enum "," parse_mode_expr --| Parse.$$$ ")" >> SOME) NONE
(* Parser for options *)
@@ -224,46 +222,46 @@
val scan_bool_option = foldl1 (op ||) (map Args.$$$ bool_options)
val scan_compilation = foldl1 (op ||) (map (fn (s, c) => Args.$$$ s >> K c) compilation_names)
in
- Scan.optional (P.$$$ "[" |-- Scan.optional scan_compilation Pred
- -- P.enum "," scan_bool_option --| P.$$$ "]")
+ Scan.optional (Parse.$$$ "[" |-- Scan.optional scan_compilation Pred
+ -- Parse.enum "," scan_bool_option --| Parse.$$$ "]")
(Pred, [])
end
-val opt_print_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
+val opt_print_modes =
+ Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
-val opt_mode = (P.$$$ "_" >> K NONE) || (parse_mode_expr >> SOME)
+val opt_mode = (Parse.$$$ "_" >> K NONE) || (parse_mode_expr >> SOME)
-val opt_param_modes = Scan.optional (P.$$$ "[" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
- P.enum ", " opt_mode --| P.$$$ "]" >> SOME) NONE
+val opt_param_modes = Scan.optional (Parse.$$$ "[" |-- Args.$$$ "mode" |-- Parse.$$$ ":" |--
+ Parse.enum ", " opt_mode --| Parse.$$$ "]" >> SOME) NONE
val stats = Scan.optional (Args.$$$ "stats" >> K true) false
val value_options =
let
- val expected_values = Scan.optional (Args.$$$ "expected" |-- P.term >> SOME) NONE
+ val expected_values = Scan.optional (Args.$$$ "expected" |-- Parse.term >> SOME) NONE
val scan_compilation =
Scan.optional
(foldl1 (op ||)
- (map (fn (s, c) => Args.$$$ s -- P.enum "," P.int >> (fn (_, ps) => (c, ps)))
+ (map (fn (s, c) => Args.$$$ s -- Parse.enum "," Parse.int >> (fn (_, ps) => (c, ps)))
compilation_names))
(Pred, [])
in
- Scan.optional (P.$$$ "[" |-- (expected_values -- stats) -- scan_compilation --| P.$$$ "]")
+ Scan.optional
+ (Parse.$$$ "[" |-- (expected_values -- stats) -- scan_compilation --| Parse.$$$ "]")
((NONE, false), (Pred, []))
end
(* code_pred command and values command *)
-val _ = OuterSyntax.local_theory_to_proof "code_pred"
+val _ = Outer_Syntax.local_theory_to_proof "code_pred"
"prove equations for predicate specified by intro/elim rules"
- OuterKeyword.thy_goal
- (opt_expected_modes -- opt_modes -- scan_options -- P.term_group >> code_pred_cmd)
+ Keyword.thy_goal
+ (opt_expected_modes -- opt_modes -- scan_options -- Parse.term_group >> code_pred_cmd)
-val _ = OuterSyntax.improper_command "values" "enumerate and print comprehensions" OuterKeyword.diag
- (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional P.nat ~1 -- P.term
+val _ = Outer_Syntax.improper_command "values" "enumerate and print comprehensions" Keyword.diag
+ (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional Parse.nat ~1 -- Parse.term
>> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.keep
(Predicate_Compile_Core.values_cmd print_modes param_modes options k t)));
end
-
-end
--- a/src/HOL/Tools/Quotient/quotient_def.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Tue May 18 06:28:42 2010 -0700
@@ -91,20 +91,15 @@
quotient_def ((NONE, NoSyn), (Attrib.empty_binding,
(Quotient_Term.quotient_lift_const qtys (b, t) ctxt, t))) ctxt
-local
- structure P = OuterParse;
-in
-
-val quotdef_decl = (P.binding >> SOME) -- P.opt_mixfix' --| P.$$$ "where"
+val quotdef_decl = (Parse.binding >> SOME) -- Parse.opt_mixfix' --| Parse.$$$ "where"
val quotdef_parser =
Scan.optional quotdef_decl (NONE, NoSyn) --
- P.!!! (Parse_Spec.opt_thm_name ":" -- (P.term --| P.$$$ "is" -- P.term))
-end
+ Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| Parse.$$$ "is" -- Parse.term))
val _ =
- OuterSyntax.local_theory "quotient_definition"
+ Outer_Syntax.local_theory "quotient_definition"
"definition for constants over the quotient type"
- OuterKeyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd))
+ Keyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd))
end; (* structure *)
--- a/src/HOL/Tools/Quotient/quotient_info.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Tue May 18 06:28:42 2010 -0700
@@ -91,9 +91,9 @@
val maps_attr_parser =
Args.context -- Scan.lift
- ((Args.name --| OuterParse.$$$ "=") --
- (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," --
- Args.name --| OuterParse.$$$ ")"))
+ ((Args.name --| Parse.$$$ "=") --
+ (Parse.$$$ "(" |-- Args.name --| Parse.$$$ "," --
+ Args.name --| Parse.$$$ ")"))
val _ = Context.>> (Context.map_theory
(Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute)
@@ -278,8 +278,8 @@
(* setup of the printing commands *)
fun improper_command (pp_fn, cmd_name, descr_str) =
- OuterSyntax.improper_command cmd_name descr_str
- OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
+ Outer_Syntax.improper_command cmd_name descr_str
+ Keyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
val _ = map improper_command
[(print_mapsinfo, "print_quotmaps", "prints out all map functions"),
--- a/src/HOL/Tools/Quotient/quotient_typ.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML Tue May 18 06:28:42 2010 -0700
@@ -299,16 +299,16 @@
end
val quotspec_parser =
- OuterParse.and_list1
- ((OuterParse.type_args -- OuterParse.binding) --
- OuterParse.opt_mixfix -- (OuterParse.$$$ "=" |-- OuterParse.typ) --
- (OuterParse.$$$ "/" |-- OuterParse.term))
+ Parse.and_list1
+ ((Parse.type_args -- Parse.binding) --
+ Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
+ (Parse.$$$ "/" |-- Parse.term))
-val _ = OuterKeyword.keyword "/"
+val _ = Keyword.keyword "/"
val _ =
- OuterSyntax.local_theory_to_proof "quotient_type"
+ Outer_Syntax.local_theory_to_proof "quotient_type"
"quotient type definitions (require equivalence proofs)"
- OuterKeyword.thy_goal (quotspec_parser >> quotient_type_cmd)
+ Keyword.thy_goal (quotspec_parser >> quotient_type_cmd)
end; (* structure *)
--- a/src/HOL/Tools/SMT/smt_solver.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/SMT/smt_solver.ML Tue May 18 06:28:42 2010 -0700
@@ -311,14 +311,14 @@
val setup =
Attrib.setup (Binding.name "smt_solver")
- (Scan.lift (OuterParse.$$$ "=" |-- Args.name) >>
+ (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
(Thm.declaration_attribute o K o select_solver))
"SMT solver configuration" #>
setup_timeout #>
setup_trace #>
setup_fixed_certificates #>
Attrib.setup (Binding.name "smt_certificates")
- (Scan.lift (OuterParse.$$$ "=" |-- Args.name) >>
+ (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
(Thm.declaration_attribute o K o select_certificates))
"SMT certificates" #>
Method.setup (Binding.name "smt") smt_method
@@ -353,9 +353,9 @@
Pretty.big_list "Solver-specific settings:" infos])
end
-val _ = OuterSyntax.improper_command "smt_status"
- "Show the available SMT solvers and the currently selected solver."
- OuterKeyword.diag
+val _ =
+ Outer_Syntax.improper_command "smt_status"
+ "show the available SMT solvers and the currently selected solver" Keyword.diag
(Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
print_setup (Context.Proof (Toplevel.context_of state)))))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue May 18 06:28:42 2010 -0700
@@ -24,8 +24,6 @@
open ATP_Systems
open Sledgehammer_Fact_Minimizer
-structure K = OuterKeyword and P = OuterParse
-
(** Proof method used in Isar proofs **)
val neg_clausify_setup =
@@ -36,7 +34,7 @@
(** Attribute for converting a theorem into clauses **)
val parse_clausify_attribute : attribute context_parser =
- Scan.lift OuterParse.nat
+ Scan.lift Parse.nat
>> (fn i => Thm.rule_attribute (fn context => fn th =>
let val thy = Context.theory_of context in
Meson.make_meta_clause (nth (cnf_axiom thy th) i)
@@ -321,13 +319,13 @@
params |> map string_for_raw_param
|> sort_strings |> cat_lines)))))
-val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
-val parse_value = Scan.repeat1 P.xname
-val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) []
-val parse_params = Scan.optional (Args.bracks (P.list parse_param)) []
+val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
+val parse_value = Scan.repeat1 Parse.xname
+val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
+val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
val parse_fact_refs =
- Scan.repeat1 (Scan.unless (P.name -- Args.colon)
- (P.xname -- Scan.option Attrib.thm_sel)
+ Scan.repeat1 (Scan.unless (Parse.name -- Args.colon)
+ (Parse.xname -- Scan.option Attrib.thm_sel)
>> (fn (name, interval) =>
Facts.Named ((name, Position.none), interval)))
val parse_relevance_chunk =
@@ -340,18 +338,18 @@
>> merge_relevance_overrides))
(add_to_relevance_override [])
val parse_sledgehammer_command =
- (Scan.optional P.short_ident runN -- parse_params -- parse_relevance_override
- -- Scan.option P.nat) #>> sledgehammer_trans
+ (Scan.optional Parse.short_ident runN -- parse_params -- parse_relevance_override
+ -- Scan.option Parse.nat) #>> sledgehammer_trans
val parse_sledgehammer_params_command =
parse_params #>> sledgehammer_params_trans
val _ =
- OuterSyntax.improper_command sledgehammerN
- "search for first-order proof using automatic theorem provers" K.diag
+ Outer_Syntax.improper_command sledgehammerN
+ "search for first-order proof using automatic theorem provers" Keyword.diag
parse_sledgehammer_command
val _ =
- OuterSyntax.command sledgehammer_paramsN
- "set and display the default parameters for Sledgehammer" K.thy_decl
+ Outer_Syntax.command sledgehammer_paramsN
+ "set and display the default parameters for Sledgehammer" Keyword.thy_decl
parse_sledgehammer_params_command
val setup =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue May 18 06:28:42 2010 -0700
@@ -102,7 +102,7 @@
let val s = unyxml y in
y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse
- OuterKeyword.is_keyword s) ? quote
+ Keyword.is_keyword s) ? quote
end
fun monomorphic_term subst t =
--- a/src/HOL/Tools/choice_specification.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/choice_specification.ML Tue May 18 06:28:42 2010 -0700
@@ -232,33 +232,28 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
-val opt_name = Scan.optional (P.name --| P.$$$ ":") ""
-val opt_overloaded = P.opt_keyword "overloaded";
+val opt_name = Scan.optional (Parse.name --| Parse.$$$ ":") ""
+val opt_overloaded = Parse.opt_keyword "overloaded"
val specification_decl =
- P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
- Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop)
+ Parse.$$$ "(" |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| Parse.$$$ ")" --
+ Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
val _ =
- OuterSyntax.command "specification" "define constants by specification" K.thy_goal
+ Outer_Syntax.command "specification" "define constants by specification" Keyword.thy_goal
(specification_decl >> (fn (cos,alt_props) =>
Toplevel.print o (Toplevel.theory_to_proof
(process_spec NONE cos alt_props))))
val ax_specification_decl =
- P.name --
- (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
- Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop))
+ Parse.name --
+ (Parse.$$$ "(" |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| Parse.$$$ ")" --
+ Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop))
val _ =
- OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
+ Outer_Syntax.command "ax_specification" "define constants by specification" Keyword.thy_goal
(ax_specification_decl >> (fn (axname,(cos,alt_props)) =>
Toplevel.print o (Toplevel.theory_to_proof
(process_spec (SOME axname) cos alt_props))))
end
-
-
-end
--- a/src/HOL/Tools/inductive.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/inductive.ML Tue May 18 06:28:42 2010 -0700
@@ -83,8 +83,7 @@
(binding * string option * mixfix) list ->
(Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
bool -> local_theory -> inductive_result * local_theory
- val gen_ind_decl: add_ind_def -> bool ->
- OuterParse.token list -> (bool -> local_theory -> local_theory) * OuterParse.token list
+ val gen_ind_decl: add_ind_def -> bool -> (bool -> local_theory -> local_theory) parser
end;
structure Inductive: INDUCTIVE =
@@ -971,32 +970,28 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = OuterKeyword.keyword "monos";
+val _ = Keyword.keyword "monos";
fun gen_ind_decl mk_def coind =
- P.fixes -- P.for_fixes --
+ Parse.fixes -- Parse.for_fixes --
Scan.optional Parse_Spec.where_alt_specs [] --
- Scan.optional (P.$$$ "monos" |-- P.!!! Parse_Spec.xthms1) []
+ Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) []
>> (fn (((preds, params), specs), monos) =>
(snd oo gen_add_inductive mk_def true coind preds params specs monos));
val ind_decl = gen_ind_decl add_ind_def;
val _ =
- OuterSyntax.local_theory' "inductive" "define inductive predicates" K.thy_decl
+ Outer_Syntax.local_theory' "inductive" "define inductive predicates" Keyword.thy_decl
(ind_decl false);
val _ =
- OuterSyntax.local_theory' "coinductive" "define coinductive predicates" K.thy_decl
+ Outer_Syntax.local_theory' "coinductive" "define coinductive predicates" Keyword.thy_decl
(ind_decl true);
val _ =
- OuterSyntax.local_theory "inductive_cases"
- "create simplified instances of elimination rules (improper)" K.thy_script
- (P.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
+ Outer_Syntax.local_theory "inductive_cases"
+ "create simplified instances of elimination rules (improper)" Keyword.thy_script
+ (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
end;
-
-end;
--- a/src/HOL/Tools/inductive_codegen.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/inductive_codegen.ML Tue May 18 06:28:42 2010 -0700
@@ -775,7 +775,7 @@
add_codegen "inductive" inductive_codegen #>
Attrib.setup @{binding code_ind}
(Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
- Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add))
+ Scan.option (Args.$$$ "params" |-- Args.colon |-- Parse.nat) >> uncurry add))
"introduction rules for executable predicates";
(**** Quickcheck involving inductive predicates ****)
--- a/src/HOL/Tools/inductive_set.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/inductive_set.ML Tue May 18 06:28:42 2010 -0700
@@ -562,18 +562,14 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;
val _ =
- OuterSyntax.local_theory' "inductive_set" "define inductive sets" K.thy_decl
+ Outer_Syntax.local_theory' "inductive_set" "define inductive sets" Keyword.thy_decl
(ind_set_decl false);
val _ =
- OuterSyntax.local_theory' "coinductive_set" "define coinductive sets" K.thy_decl
+ Outer_Syntax.local_theory' "coinductive_set" "define coinductive sets" Keyword.thy_decl
(ind_set_decl true);
end;
-
-end;
--- a/src/HOL/Tools/primrec.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/primrec.ML Tue May 18 06:28:42 2010 -0700
@@ -307,29 +307,26 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
val opt_unchecked_name =
- Scan.optional (P.$$$ "(" |-- P.!!!
- (((P.$$$ "unchecked" >> K true) -- Scan.optional P.name "" ||
- P.name >> pair false) --| P.$$$ ")")) (false, "");
+ Scan.optional (Parse.$$$ "(" |-- Parse.!!!
+ (((Parse.$$$ "unchecked" >> K true) -- Scan.optional Parse.name "" ||
+ Parse.name >> pair false) --| Parse.$$$ ")")) (false, "");
val old_primrec_decl =
opt_unchecked_name --
- Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop);
+ Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop);
-val primrec_decl = P.opt_target -- P.fixes -- Parse_Spec.where_alt_specs;
+val primrec_decl = Parse.opt_target -- Parse.fixes -- Parse_Spec.where_alt_specs;
val _ =
- OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
+ Outer_Syntax.command "primrec" "define primitive recursive functions on datatypes"
+ Keyword.thy_decl
((primrec_decl >> (fn ((opt_target, fixes), specs) =>
Toplevel.local_theory opt_target (add_primrec_cmd fixes specs #> snd)))
|| (old_primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
Toplevel.theory (snd o
(if unchecked then OldPrimrec.add_primrec_unchecked else OldPrimrec.add_primrec)
- alt_name (map P.triple_swap eqns) o
+ alt_name (map Parse.triple_swap eqns) o
tap (fn _ => legacy_feature "Old variant of 'primrec' command -- use new syntax instead")))));
end;
-
-end;
--- a/src/HOL/Tools/recdef.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/recdef.ML Tue May 18 06:28:42 2010 -0700
@@ -289,40 +289,39 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = List.app OuterKeyword.keyword ["permissive", "congs", "hints"];
+val _ = List.app Keyword.keyword ["permissive", "congs", "hints"];
val hints =
- P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- Args.parse) --| P.$$$ ")") >> Args.src;
+ Parse.$$$ "(" |--
+ Parse.!!! (Parse.position (Parse.$$$ "hints" -- Args.parse) --| Parse.$$$ ")") >> Args.src;
val recdef_decl =
- Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
- P.name -- P.term -- Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- P.prop)
+ Scan.optional
+ (Parse.$$$ "(" -- Parse.!!! (Parse.$$$ "permissive" -- Parse.$$$ ")") >> K false) true --
+ Parse.name -- Parse.term -- Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
-- Scan.option hints
- >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
+ >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map Parse.triple_swap eqs) src);
val _ =
- OuterSyntax.command "recdef" "define general recursive functions (TFL)" K.thy_decl
+ Outer_Syntax.command "recdef" "define general recursive functions (TFL)" Keyword.thy_decl
(recdef_decl >> Toplevel.theory);
val defer_recdef_decl =
- P.name -- Scan.repeat1 P.prop --
- Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (Parse_Spec.xthms1 --| P.$$$ ")")) []
+ Parse.name -- Scan.repeat1 Parse.prop --
+ Scan.optional
+ (Parse.$$$ "(" |-- Parse.$$$ "congs" |-- Parse.!!! (Parse_Spec.xthms1 --| Parse.$$$ ")")) []
>> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
val _ =
- OuterSyntax.command "defer_recdef" "defer general recursive functions (TFL)" K.thy_decl
+ Outer_Syntax.command "defer_recdef" "defer general recursive functions (TFL)" Keyword.thy_decl
(defer_recdef_decl >> Toplevel.theory);
val _ =
- OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
- K.thy_goal
- ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- P.xname --
- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
+ Outer_Syntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
+ Keyword.thy_goal
+ ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.xname --
+ Scan.option (Parse.$$$ "(" |-- Parse.nat --| Parse.$$$ ")")
>> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
end;
-
-end;
--- a/src/HOL/Tools/record.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/record.ML Tue May 18 06:28:42 2010 -0700
@@ -2460,17 +2460,14 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
val _ =
- OuterSyntax.command "record" "define extensible record" K.thy_decl
- (P.type_args_constrained -- P.binding --
- (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const_binding)
+ Outer_Syntax.command "record" "define extensible record" Keyword.thy_decl
+ (Parse.type_args_constrained -- Parse.binding --
+ (Parse.$$$ "=" |-- Scan.option (Parse.typ --| Parse.$$$ "+") --
+ Scan.repeat1 Parse.const_binding)
>> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd false x y z)));
end;
-end;
-
structure Basic_Record: BASIC_RECORD = Record;
open Basic_Record;
--- a/src/HOL/Tools/refute_isar.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/refute_isar.ML Tue May 18 06:28:42 2010 -0700
@@ -12,19 +12,16 @@
(*optional list of arguments of the form [name1=value1, name2=value2, ...]*)
-val scan_parm =
- OuterParse.name
- -- (Scan.optional (OuterParse.$$$ "=" |-- OuterParse.name) "true")
-val scan_parms = Scan.optional
- (OuterParse.$$$ "[" |-- OuterParse.list scan_parm --| OuterParse.$$$ "]") [];
+val scan_parm = Parse.name -- (Scan.optional (Parse.$$$ "=" |-- Parse.name) "true")
+val scan_parms = Scan.optional (Parse.$$$ "[" |-- Parse.list scan_parm --| Parse.$$$ "]") [];
(* 'refute' command *)
val _ =
- OuterSyntax.improper_command "refute"
- "try to find a model that refutes a given subgoal" OuterKeyword.diag
- (scan_parms -- Scan.optional OuterParse.nat 1 >>
+ Outer_Syntax.improper_command "refute"
+ "try to find a model that refutes a given subgoal" Keyword.diag
+ (scan_parms -- Scan.optional Parse.nat 1 >>
(fn (parms, i) =>
Toplevel.keep (fn state =>
let
@@ -36,8 +33,8 @@
(* 'refute_params' command *)
val _ =
- OuterSyntax.command "refute_params"
- "show/store default parameters for the 'refute' command" OuterKeyword.thy_decl
+ Outer_Syntax.command "refute_params"
+ "show/store default parameters for the 'refute' command" Keyword.thy_decl
(scan_parms >> (fn parms =>
Toplevel.theory (fn thy =>
let
--- a/src/HOL/Tools/split_rule.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/split_rule.ML Tue May 18 06:28:42 2010 -0700
@@ -135,7 +135,7 @@
Attrib.setup @{binding split_format}
(Scan.lift
(Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
- OuterParse.and_list1 (Scan.repeat Args.name_source)
+ Parse.and_list1 (Scan.repeat Args.name_source)
>> (fn xss => Thm.rule_attribute (fn context =>
split_rule_goal (Context.proof_of context) xss))))
"split pair-typed subterms in premises, or function arguments" #>
--- a/src/HOL/Tools/typedef.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOL/Tools/typedef.ML Tue May 18 06:28:42 2010 -0700
@@ -296,22 +296,19 @@
(** outer syntax **)
-local structure P = OuterParse in
-
-val _ = OuterKeyword.keyword "morphisms";
+val _ = Keyword.keyword "morphisms";
val _ =
- OuterSyntax.local_theory_to_proof "typedef" "HOL type definition (requires non-emptiness proof)"
- OuterKeyword.thy_goal
- (Scan.optional (P.$$$ "(" |--
- ((P.$$$ "open" >> K false) -- Scan.option P.binding ||
- P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) --
- (P.type_args_constrained -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding))
+ Outer_Syntax.local_theory_to_proof "typedef" "HOL type definition (requires non-emptiness proof)"
+ Keyword.thy_goal
+ (Scan.optional (Parse.$$$ "(" |--
+ ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
+ Parse.binding >> (fn s => (true, SOME s))) --| Parse.$$$ ")") (true, NONE) --
+ (Parse.type_args_constrained -- Parse.binding) --
+ Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.term) --
+ Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))
>> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) =>
typedef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)));
end;
-end;
-
--- a/src/HOLCF/IOA/meta_theory/automaton.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOLCF/IOA/meta_theory/automaton.ML Tue May 18 06:28:42 2010 -0700
@@ -485,52 +485,50 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = List.app OuterKeyword.keyword ["signature", "actions", "inputs",
+val _ = List.app Keyword.keyword ["signature", "actions", "inputs",
"outputs", "internals", "states", "initially", "transitions", "pre",
"post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
"rename"];
-val actionlist = P.list1 P.term;
-val inputslist = P.$$$ "inputs" |-- P.!!! actionlist;
-val outputslist = P.$$$ "outputs" |-- P.!!! actionlist;
-val internalslist = P.$$$ "internals" |-- P.!!! actionlist;
-val stateslist = P.$$$ "states" |-- P.!!! (Scan.repeat1 (P.name --| P.$$$ "::" -- P.typ));
-val initial = P.$$$ "initially" |-- P.!!! P.term;
-val assign_list = P.list1 (P.name --| P.$$$ ":=" -- P.!!! P.term);
-val pre = P.$$$ "pre" |-- P.!!! P.term;
-val post = P.$$$ "post" |-- P.!!! assign_list;
+val actionlist = Parse.list1 Parse.term;
+val inputslist = Parse.$$$ "inputs" |-- Parse.!!! actionlist;
+val outputslist = Parse.$$$ "outputs" |-- Parse.!!! actionlist;
+val internalslist = Parse.$$$ "internals" |-- Parse.!!! actionlist;
+val stateslist =
+ Parse.$$$ "states" |-- Parse.!!! (Scan.repeat1 (Parse.name --| Parse.$$$ "::" -- Parse.typ));
+val initial = Parse.$$$ "initially" |-- Parse.!!! Parse.term;
+val assign_list = Parse.list1 (Parse.name --| Parse.$$$ ":=" -- Parse.!!! Parse.term);
+val pre = Parse.$$$ "pre" |-- Parse.!!! Parse.term;
+val post = Parse.$$$ "post" |-- Parse.!!! assign_list;
val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost;
val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost;
-val transrel = (P.$$$ "transrel" |-- P.!!! P.term) >> mk_trans_of_rel;
-val transition = P.term -- (transrel || pre1 || post1);
-val translist = P.$$$ "transitions" |-- P.!!! (Scan.repeat1 transition);
+val transrel = (Parse.$$$ "transrel" |-- Parse.!!! Parse.term) >> mk_trans_of_rel;
+val transition = Parse.term -- (transrel || pre1 || post1);
+val translist = Parse.$$$ "transitions" |-- Parse.!!! (Scan.repeat1 transition);
val ioa_decl =
- (P.name -- (P.$$$ "=" |--
- (P.$$$ "signature" |--
- P.!!! (P.$$$ "actions" |--
- (P.typ --
+ (Parse.name -- (Parse.$$$ "=" |--
+ (Parse.$$$ "signature" |--
+ Parse.!!! (Parse.$$$ "actions" |--
+ (Parse.typ --
(Scan.optional inputslist []) --
(Scan.optional outputslist []) --
(Scan.optional internalslist []) --
stateslist --
(Scan.optional initial "True") --
translist))))) >> mk_ioa_decl ||
- (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.!!! (P.list1 P.name))))
+ (Parse.name -- (Parse.$$$ "=" |-- (Parse.$$$ "compose" |-- Parse.!!! (Parse.list1 Parse.name))))
>> mk_composition_decl ||
- (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |--
- P.!!! (P.list1 P.term -- (P.$$$ "in" |-- P.name))))) >> mk_hiding_decl ||
- (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |--
- P.!!! (P.name -- (P.$$$ "to" |-- P.list1 P.term))))) >> mk_restriction_decl ||
- (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term))))))
+ (Parse.name -- (Parse.$$$ "=" |-- (Parse.$$$ "hide_action" |--
+ Parse.!!! (Parse.list1 Parse.term -- (Parse.$$$ "in" |-- Parse.name))))) >> mk_hiding_decl ||
+ (Parse.name -- (Parse.$$$ "=" |-- (Parse.$$$ "restrict" |--
+ Parse.!!! (Parse.name -- (Parse.$$$ "to" |-- Parse.list1 Parse.term))))) >> mk_restriction_decl ||
+ (Parse.name -- (Parse.$$$ "=" |--
+ (Parse.$$$ "rename" |-- (Parse.!!! (Parse.name -- (Parse.$$$ "to" |-- Parse.term))))))
>> mk_rename_decl;
val _ =
- OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl
+ Outer_Syntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" Keyword.thy_decl
(ioa_decl >> Toplevel.theory);
end;
-
-end;
--- a/src/HOLCF/Tools/Domain/domain_extender.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Tue May 18 06:28:42 2010 -0700
@@ -224,27 +224,25 @@
(** outer syntax **)
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = OuterKeyword.keyword "lazy";
+val _ = Keyword.keyword "lazy";
val dest_decl : (bool * binding option * string) parser =
- P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
- (P.binding >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1
- || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")"
+ Parse.$$$ "(" |-- Scan.optional (Parse.$$$ "lazy" >> K true) false --
+ (Parse.binding >> SOME) -- (Parse.$$$ "::" |-- Parse.typ) --| Parse.$$$ ")" >> Parse.triple1
+ || Parse.$$$ "(" |-- Parse.$$$ "lazy" |-- Parse.typ --| Parse.$$$ ")"
>> (fn t => (true,NONE,t))
- || P.typ >> (fn t => (false,NONE,t));
+ || Parse.typ >> (fn t => (false,NONE,t));
val cons_decl =
- P.binding -- Scan.repeat dest_decl -- P.opt_mixfix;
+ Parse.binding -- Scan.repeat dest_decl -- Parse.opt_mixfix;
val domain_decl =
- (P.type_args_constrained -- P.binding -- P.opt_mixfix) --
- (P.$$$ "=" |-- P.enum1 "|" cons_decl);
+ (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix) --
+ (Parse.$$$ "=" |-- Parse.enum1 "|" cons_decl);
val domains_decl =
- Scan.option (P.$$$ "(" |-- P.binding --| P.$$$ ")") --
- P.and_list1 domain_decl;
+ Scan.option (Parse.$$$ "(" |-- Parse.binding --| Parse.$$$ ")") --
+ Parse.and_list1 domain_decl;
fun mk_domain
(definitional : bool)
@@ -267,13 +265,11 @@
end;
val _ =
- OuterSyntax.command "domain" "define recursive domains (HOLCF)"
- K.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false));
+ Outer_Syntax.command "domain" "define recursive domains (HOLCF)"
+ Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain false));
val _ =
- OuterSyntax.command "new_domain" "define recursive domains (HOLCF)"
- K.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true));
+ Outer_Syntax.command "new_domain" "define recursive domains (HOLCF)"
+ Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain true));
end;
-
-end;
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Tue May 18 06:28:42 2010 -0700
@@ -707,21 +707,20 @@
local
-structure P = OuterParse and K = OuterKeyword
-
val parse_domain_iso :
(string list * binding * mixfix * string * (binding * binding) option)
parser =
- (P.type_args -- P.binding -- P.opt_mixfix -- (P.$$$ "=" |-- P.typ) --
- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding)))
+ (Parse.type_args -- Parse.binding -- Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
+ Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)))
>> (fn ((((vs, t), mx), rhs), morphs) => (vs, t, mx, rhs, morphs));
-val parse_domain_isos = P.and_list1 parse_domain_iso;
+val parse_domain_isos = Parse.and_list1 parse_domain_iso;
in
val _ =
- OuterSyntax.command "domain_isomorphism" "define domain isomorphisms (HOLCF)" K.thy_decl
+ Outer_Syntax.command "domain_isomorphism" "define domain isomorphisms (HOLCF)"
+ Keyword.thy_decl
(parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd));
end;
--- a/src/HOLCF/Tools/cont_consts.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOLCF/Tools/cont_consts.ML Tue May 18 06:28:42 2010 -0700
@@ -93,12 +93,8 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
val _ =
- OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl
- (Scan.repeat1 P.const_binding >> (Toplevel.theory o add_consts_cmd));
+ Outer_Syntax.command "consts" "declare constants (HOLCF)" Keyword.thy_decl
+ (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o add_consts_cmd));
end;
-
-end;
--- a/src/HOLCF/Tools/fixrec.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOLCF/Tools/fixrec.ML Tue May 18 06:28:42 2010 -0700
@@ -443,16 +443,14 @@
(******************************** Parsers ********************************)
(*************************************************************************)
-local structure P = OuterParse and K = OuterKeyword in
+val _ =
+ Outer_Syntax.local_theory "fixrec" "define recursive functions (HOLCF)" Keyword.thy_decl
+ ((Parse.opt_keyword "permissive" >> not) -- Parse.fixes -- Parse_Spec.where_alt_specs
+ >> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs));
-val _ = OuterSyntax.local_theory "fixrec" "define recursive functions (HOLCF)" K.thy_decl
- ((P.opt_keyword "permissive" >> not) -- P.fixes -- Parse_Spec.where_alt_specs
- >> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs));
-
-val _ = OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
- (Parse_Spec.specs >> (Toplevel.theory o add_fixpat_cmd));
-
-end;
+val _ =
+ Outer_Syntax.command "fixpat" "define rewrites for fixrec functions" Keyword.thy_decl
+ (Parse_Spec.specs >> (Toplevel.theory o add_fixpat_cmd));
val setup =
Attrib.setup @{binding fixrec_simp}
--- a/src/HOLCF/Tools/pcpodef.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOLCF/Tools/pcpodef.ML Tue May 18 06:28:42 2010 -0700
@@ -355,29 +355,29 @@
(** outer syntax **)
-local structure P = OuterParse and K = OuterKeyword in
-
val typedef_proof_decl =
- Scan.optional (P.$$$ "(" |--
- ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
- --| P.$$$ ")") (true, NONE) --
- (P.type_args_constrained -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
+ Scan.optional (Parse.$$$ "(" |--
+ ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
+ Parse.binding >> (fn s => (true, SOME s)))
+ --| Parse.$$$ ")") (true, NONE) --
+ (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix --
+ (Parse.$$$ "=" |-- Parse.term) --
+ Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding));
fun mk_pcpodef_proof pcpo ((((((def, opt_name), (args, t)), mx), A), morphs)) =
(if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
((def, the_default t opt_name), (t, args, mx), A, morphs);
val _ =
- OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
+ Outer_Syntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)"
+ Keyword.thy_goal
(typedef_proof_decl >>
(Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
val _ =
- OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
+ Outer_Syntax.command "cpodef" "HOLCF type definition (requires admissibility proof)"
+ Keyword.thy_goal
(typedef_proof_decl >>
(Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
end;
-
-end;
--- a/src/HOLCF/Tools/repdef.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/HOLCF/Tools/repdef.ML Tue May 18 06:28:42 2010 -0700
@@ -168,23 +168,21 @@
(** outer syntax **)
-local structure P = OuterParse and K = OuterKeyword in
-
val repdef_decl =
- Scan.optional (P.$$$ "(" |--
- ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
- --| P.$$$ ")") (true, NONE) --
- (P.type_args_constrained -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
- Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
+ Scan.optional (Parse.$$$ "(" |--
+ ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
+ Parse.binding >> (fn s => (true, SOME s)))
+ --| Parse.$$$ ")") (true, NONE) --
+ (Parse.type_args_constrained -- Parse.binding) --
+ Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.term) --
+ Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding));
fun mk_repdef ((((((def, opt_name), (args, t)), mx), A), morphs)) =
repdef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs);
val _ =
- OuterSyntax.command "repdef" "HOLCF definition of representable domains" K.thy_decl
+ Outer_Syntax.command "repdef" "HOLCF definition of representable domains" Keyword.thy_decl
(repdef_decl >>
(Toplevel.print oo (Toplevel.theory o mk_repdef)));
end;
-
-end;
--- a/src/Provers/blast.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Provers/blast.ML Tue May 18 06:28:42 2010 -0700
@@ -1309,7 +1309,7 @@
val setup =
setup_depth_limit #>
Method.setup @{binding blast}
- (Scan.lift (Scan.option OuterParse.nat) --| Method.sections Data.cla_modifiers >>
+ (Scan.lift (Scan.option Parse.nat) --| Method.sections Data.cla_modifiers >>
(fn NONE => Data.cla_meth' blast_tac
| SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim)))
"classical tableau prover";
--- a/src/Provers/clasimp.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Provers/clasimp.ML Tue May 18 06:28:42 2010 -0700
@@ -275,7 +275,7 @@
Method.sections clasimp_modifiers >> K (clasimp_meth' tac);
val auto_method =
- Scan.lift (Scan.option (OuterParse.nat -- OuterParse.nat)) --|
+ Scan.lift (Scan.option (Parse.nat -- Parse.nat)) --|
Method.sections clasimp_modifiers >>
(fn NONE => clasimp_meth (CHANGED_PROP o auto_tac)
| SOME (m, n) => clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n)));
--- a/src/Provers/classical.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Provers/classical.ML Tue May 18 06:28:42 2010 -0700
@@ -1015,8 +1015,8 @@
(** outer syntax **)
val _ =
- OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
- OuterKeyword.diag
+ Outer_Syntax.improper_command "print_claset" "print context of Classical Reasoner"
+ Keyword.diag
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
Toplevel.keep (print_cs o claset_of o Toplevel.context_of)));
--- a/src/Pure/General/scan.scala Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/General/scan.scala Tue May 18 06:28:42 2010 -0700
@@ -258,47 +258,44 @@
/* outer syntax tokens */
- def token(symbols: Symbol.Interpretation, is_command: String => Boolean):
- Parser[Outer_Lex.Token] =
+ def token(symbols: Symbol.Interpretation, is_command: String => Boolean): Parser[Token] =
{
- import Outer_Lex.Token_Kind, Outer_Lex.Token
-
val id = one(symbols.is_letter) ~ many(symbols.is_letdig) ^^ { case x ~ y => x + y }
val nat = many1(symbols.is_digit)
val id_nat = id ~ opt("." ~ nat) ^^ { case x ~ Some(y ~ z) => x + y + z case x ~ None => x }
val ident = id ~ rep("." ~> id) ^^
- { case x ~ Nil => Token(Token_Kind.IDENT, x)
- case x ~ ys => Token(Token_Kind.LONG_IDENT, (x :: ys).mkString(".")) }
+ { case x ~ Nil => Token(Token.Kind.IDENT, x)
+ case x ~ ys => Token(Token.Kind.LONG_IDENT, (x :: ys).mkString(".")) }
- val var_ = "?" ~ id_nat ^^ { case x ~ y => Token(Token_Kind.VAR, x + y) }
- val type_ident = "'" ~ id ^^ { case x ~ y => Token(Token_Kind.TYPE_IDENT, x + y) }
- val type_var = "?'" ~ id_nat ^^ { case x ~ y => Token(Token_Kind.TYPE_VAR, x + y) }
- val nat_ = nat ^^ (x => Token(Token_Kind.NAT, x))
+ val var_ = "?" ~ id_nat ^^ { case x ~ y => Token(Token.Kind.VAR, x + y) }
+ val type_ident = "'" ~ id ^^ { case x ~ y => Token(Token.Kind.TYPE_IDENT, x + y) }
+ val type_var = "?'" ~ id_nat ^^ { case x ~ y => Token(Token.Kind.TYPE_VAR, x + y) }
+ val nat_ = nat ^^ (x => Token(Token.Kind.NAT, x))
val sym_ident =
(many1(symbols.is_symbolic_char) |
one(sym => symbols.is_symbolic(sym) & Symbol.is_wellformed(sym))) ^^
- (x => Token(Token_Kind.SYM_IDENT, x))
+ (x => Token(Token.Kind.SYM_IDENT, x))
- val space = many1(symbols.is_blank) ^^ (x => Token(Token_Kind.SPACE, x))
+ val space = many1(symbols.is_blank) ^^ (x => Token(Token.Kind.SPACE, x))
- val string = quoted("\"") ^^ (x => Token(Token_Kind.STRING, x))
- val alt_string = quoted("`") ^^ (x => Token(Token_Kind.ALT_STRING, x))
+ val string = quoted("\"") ^^ (x => Token(Token.Kind.STRING, x))
+ val alt_string = quoted("`") ^^ (x => Token(Token.Kind.ALT_STRING, x))
val junk = many1(sym => !(symbols.is_blank(sym)))
val bad_delimiter =
- ("\"" | "`" | "{*" | "(*") ~ junk ^^ { case x ~ y => Token(Token_Kind.BAD_INPUT, x + y) }
- val bad = junk ^^ (x => Token(Token_Kind.BAD_INPUT, x))
+ ("\"" | "`" | "{*" | "(*") ~ junk ^^ { case x ~ y => Token(Token.Kind.BAD_INPUT, x + y) }
+ val bad = junk ^^ (x => Token(Token.Kind.BAD_INPUT, x))
/* tokens */
- (space | (string | (alt_string | (verbatim ^^ (x => Token(Token_Kind.VERBATIM, x)) |
- comment ^^ (x => Token(Token_Kind.COMMENT, x)))))) |
+ (space | (string | (alt_string | (verbatim ^^ (x => Token(Token.Kind.VERBATIM, x)) |
+ comment ^^ (x => Token(Token.Kind.COMMENT, x)))))) |
bad_delimiter |
((ident | (var_ | (type_ident | (type_var | (nat_ | sym_ident))))) |||
- keyword ^^ (x => Token(if (is_command(x)) Token_Kind.COMMAND else Token_Kind.KEYWORD, x))) |
+ keyword ^^ (x => Token(if (is_command(x)) Token.Kind.COMMAND else Token.Kind.KEYWORD, x))) |
bad
}
}
--- a/src/Pure/General/symbol_pos.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/General/symbol_pos.ML Tue May 18 06:28:42 2010 -0700
@@ -4,17 +4,12 @@
Symbols with explicit position information.
*)
-signature BASIC_SYMBOL_POS =
+signature SYMBOL_POS =
sig
type T = Symbol.symbol * Position.T
val symbol: T -> Symbol.symbol
val $$$ : Symbol.symbol -> T list -> T list * T list
val ~$$$ : Symbol.symbol -> T list -> T list * T list
-end
-
-signature SYMBOL_POS =
-sig
- include BASIC_SYMBOL_POS
val content: T list -> string
val untabify_content: T list -> string
val is_eof: T -> bool
@@ -185,5 +180,10 @@
end;
-structure Basic_Symbol_Pos: BASIC_SYMBOL_POS = Symbol_Pos; (*not open by default*)
+structure Basic_Symbol_Pos = (*not open by default*)
+struct
+ val symbol = Symbol_Pos.symbol;
+ val $$$ = Symbol_Pos.$$$;
+ val ~$$$ = Symbol_Pos.~$$$;
+end;
--- a/src/Pure/IsaMakefile Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/IsaMakefile Tue May 18 06:28:42 2010 -0700
@@ -67,24 +67,25 @@
Isar/expression.ML Isar/isar_cmd.ML Isar/isar_document.ML \
Isar/isar_syn.ML Isar/keyword.ML Isar/local_defs.ML \
Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML \
- Isar/method.ML Isar/object_logic.ML Isar/obtain.ML Isar/outer_lex.ML \
+ Isar/method.ML Isar/object_logic.ML Isar/obtain.ML \
Isar/outer_syntax.ML Isar/overloading.ML Isar/parse.ML \
Isar/parse_spec.ML Isar/parse_value.ML Isar/proof.ML \
Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \
Isar/rule_cases.ML Isar/rule_insts.ML Isar/runtime.ML \
Isar/skip_proof.ML Isar/spec_rules.ML Isar/specification.ML \
- Isar/theory_target.ML Isar/toplevel.ML Isar/typedecl.ML \
- ML/ml_antiquote.ML ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML \
- ML/ml_context.ML ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML \
- ML/ml_syntax.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \
- ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML \
- Proof/extraction.ML Proof/proof_rewrite_rules.ML \
- Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \
- ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML \
- ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML \
- ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML \
- ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML \
- ProofGeneral/preferences.ML ProofGeneral/proof_general_emacs.ML \
+ Isar/theory_target.ML Isar/token.ML Isar/toplevel.ML \
+ Isar/typedecl.ML ML/ml_antiquote.ML ML/ml_compiler.ML \
+ ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML \
+ ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML \
+ ML-Systems/install_pp_polyml.ML ML-Systems/install_pp_polyml-5.3.ML \
+ ML-Systems/use_context.ML Proof/extraction.ML \
+ Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \
+ Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/pgip.ML \
+ ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML \
+ ProofGeneral/pgip_markup.ML ProofGeneral/pgip_output.ML \
+ ProofGeneral/pgip_parser.ML ProofGeneral/pgip_tests.ML \
+ ProofGeneral/pgip_types.ML ProofGeneral/preferences.ML \
+ ProofGeneral/proof_general_emacs.ML \
ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML \
Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \
Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML \
--- a/src/Pure/Isar/args.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Isar/args.ML Tue May 18 06:28:42 2010 -0700
@@ -7,10 +7,9 @@
signature ARGS =
sig
- type token = OuterLex.token
type src
- val src: (string * token list) * Position.T -> src
- val dest_src: src -> (string * token list) * Position.T
+ val src: (string * Token.T list) * Position.T -> src
+ val dest_src: src -> (string * Token.T list) * Position.T
val pretty_src: Proof.context -> src -> Pretty.T
val map_name: (string -> string) -> src -> src
val morph_values: morphism -> src -> src
@@ -57,8 +56,8 @@
val const: bool -> string context_parser
val const_proper: bool -> string context_parser
val goal_spec: ((int -> tactic) -> tactic) context_parser
- val parse: token list parser
- val parse1: (string -> bool) -> token list parser
+ val parse: Token.T list parser
+ val parse1: (string -> bool) -> Token.T list parser
val attribs: (string -> string) -> src list parser
val opt_attribs: (string -> string) -> src list parser
val thm_name: (string -> string) -> string -> (binding * src list) parser
@@ -70,15 +69,9 @@
structure Args: ARGS =
struct
-structure T = OuterLex;
-
-type token = T.token;
-
-
-
(** datatype src **)
-datatype src = Src of (string * token list) * Position.T;
+datatype src = Src of (string * Token.T list) * Position.T;
val src = Src;
fun dest_src (Src src) = src;
@@ -87,12 +80,12 @@
let
val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
fun prt arg =
- (case T.get_value arg of
- SOME (T.Text s) => Pretty.str (quote s)
- | SOME (T.Typ T) => Syntax.pretty_typ ctxt T
- | SOME (T.Term t) => Syntax.pretty_term ctxt t
- | SOME (T.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
- | _ => Pretty.str (T.unparse arg));
+ (case Token.get_value arg of
+ SOME (Token.Text s) => Pretty.str (quote s)
+ | SOME (Token.Typ T) => Syntax.pretty_typ ctxt T
+ | SOME (Token.Term t) => Syntax.pretty_term ctxt t
+ | SOME (Token.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
+ | _ => Pretty.str (Token.unparse arg));
val (s, args) = #1 (dest_src src);
in Pretty.block (Pretty.breaks (Pretty.str s :: map prt args)) end;
@@ -102,15 +95,15 @@
(* values *)
-fun morph_values phi = map_args (T.map_value
- (fn T.Text s => T.Text s
- | T.Typ T => T.Typ (Morphism.typ phi T)
- | T.Term t => T.Term (Morphism.term phi t)
- | T.Fact ths => T.Fact (Morphism.fact phi ths)
- | T.Attribute att => T.Attribute (Morphism.transform phi att)));
+fun morph_values phi = map_args (Token.map_value
+ (fn Token.Text s => Token.Text s
+ | Token.Typ T => Token.Typ (Morphism.typ phi T)
+ | Token.Term t => Token.Term (Morphism.term phi t)
+ | Token.Fact ths => Token.Fact (Morphism.fact phi ths)
+ | Token.Attribute att => Token.Attribute (Morphism.transform phi att)));
-val assignable = map_args T.assignable;
-val closure = map_args T.closure;
+val assignable = map_args Token.assignable;
+val closure = map_args Token.closure;
@@ -134,7 +127,7 @@
val alt_string = token Parse.alt_string;
val symbolic = token Parse.keyword_ident_or_symbolic;
-fun $$$ x = (ident >> T.content_of || Parse.keyword)
+fun $$$ x = (ident >> Token.content_of || Parse.keyword)
:|-- (fn y => if x = y then Scan.succeed x else Scan.fail);
@@ -153,39 +146,40 @@
fun mode s = Scan.lift (Scan.optional (parens ($$$ s) >> K true) false);
fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
-val name_source = named >> T.source_of;
-val name_source_position = named >> T.source_position_of;
+val name_source = named >> Token.source_of;
+val name_source_position = named >> Token.source_position_of;
-val name = named >> T.content_of;
+val name = named >> Token.content_of;
val binding = Parse.position name >> Binding.make;
-val alt_name = alt_string >> T.content_of;
-val symbol = symbolic >> T.content_of;
+val alt_name = alt_string >> Token.content_of;
+val symbol = symbolic >> Token.content_of;
val liberal_name = symbol || name;
-val var = (ident >> T.content_of) :|-- (fn x =>
+val var = (ident >> Token.content_of) :|-- (fn x =>
(case Lexicon.read_variable x of SOME v => Scan.succeed v | NONE => Scan.fail));
(* values *)
fun value dest = Scan.some (fn arg =>
- (case T.get_value arg of SOME v => (SOME (dest v) handle Match => NONE) | NONE => NONE));
+ (case Token.get_value arg of SOME v => (SOME (dest v) handle Match => NONE) | NONE => NONE));
fun evaluate mk eval arg =
- let val x = eval arg in (T.assign (SOME (mk x)) arg; x) end;
+ let val x = eval arg in (Token.assign (SOME (mk x)) arg; x) end;
+
+val internal_text = value (fn Token.Text s => s);
+val internal_typ = value (fn Token.Typ T => T);
+val internal_term = value (fn Token.Term t => t);
+val internal_fact = value (fn Token.Fact ths => ths);
+val internal_attribute = value (fn Token.Attribute att => att);
-val internal_text = value (fn T.Text s => s);
-val internal_typ = value (fn T.Typ T => T);
-val internal_term = value (fn T.Term t => t);
-val internal_fact = value (fn T.Fact ths => ths);
-val internal_attribute = value (fn T.Attribute att => att);
-
-fun named_text intern = internal_text || named >> evaluate T.Text (intern o T.content_of);
-fun named_typ readT = internal_typ || named >> evaluate T.Typ (readT o T.source_of);
-fun named_term read = internal_term || named >> evaluate T.Term (read o T.source_of);
-fun named_fact get = internal_fact || named >> evaluate T.Fact (get o T.content_of) ||
- alt_string >> evaluate T.Fact (get o T.source_of);
-fun named_attribute att = internal_attribute || named >> evaluate T.Attribute (att o T.content_of);
+fun named_text intern = internal_text || named >> evaluate Token.Text (intern o Token.content_of);
+fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.source_of);
+fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.source_of);
+fun named_fact get = internal_fact || named >> evaluate Token.Fact (get o Token.content_of) ||
+ alt_string >> evaluate Token.Fact (get o Token.source_of);
+fun named_attribute att =
+ internal_attribute || named >> evaluate Token.Attribute (att o Token.content_of);
(* terms and types *)
@@ -243,7 +237,7 @@
(token (Parse.$$$ l) ::: Parse.!!! (args true @@@ (token (Parse.$$$ r) >> single))) x;
in (args, args1) end;
-val parse = #1 (parse_args T.ident_or_symbolic) false;
+val parse = #1 (parse_args Token.ident_or_symbolic) false;
fun parse1 is_symid = #2 (parse_args is_symid) false;
@@ -252,7 +246,7 @@
fun attribs intern =
let
val attrib_name = internal_text || (symbolic || named)
- >> evaluate T.Text (intern o T.content_of);
+ >> evaluate Token.Text (intern o Token.content_of);
val attrib = Parse.position (attrib_name -- Parse.!!! parse) >> src;
in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;
@@ -273,11 +267,11 @@
(** syntax wrapper **)
fun syntax kind scan (Src ((s, args), pos)) st =
- (case Scan.error (Scan.finite' T.stopper (Scan.option scan)) (st, args) of
+ (case Scan.error (Scan.finite' Token.stopper (Scan.option scan)) (st, args) of
(SOME x, (st', [])) => (x, st')
| (_, (_, args')) =>
error (kind ^ " " ^ quote s ^ Position.str_of pos ^ ": bad arguments\n " ^
- space_implode " " (map T.unparse args')));
+ space_implode " " (map Token.unparse args')));
fun context_syntax kind scan src = apsnd Context.the_proof o syntax kind scan src o Context.Proof;
--- a/src/Pure/Isar/attrib.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Isar/attrib.ML Tue May 18 06:28:42 2010 -0700
@@ -47,9 +47,6 @@
structure Attrib: ATTRIB =
struct
-structure T = OuterLex;
-
-
(* source and bindings *)
type src = Args.src;
@@ -216,7 +213,7 @@
(* internal *)
-fun internal att = Args.src (("Pure.attribute", [T.mk_attribute att]), Position.none);
+fun internal att = Args.src (("Pure.attribute", [Token.mk_attribute att]), Position.none);
(* rule composition *)
--- a/src/Pure/Isar/keyword.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Isar/keyword.ML Tue May 18 06:28:42 2010 -0700
@@ -210,7 +210,4 @@
end;
-(*legacy alias*)
-structure OuterKeyword = Keyword;
-
--- a/src/Pure/Isar/method.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Isar/method.ML Tue May 18 06:28:42 2010 -0700
@@ -411,7 +411,7 @@
(* outer parser *)
fun is_symid_meth s =
- s <> "|" andalso s <> "?" andalso s <> "+" andalso OuterLex.ident_or_symbolic s;
+ s <> "|" andalso s <> "?" andalso s <> "+" andalso Token.ident_or_symbolic s;
local
--- a/src/Pure/Isar/outer_lex.ML Mon May 17 18:59:59 2010 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,390 +0,0 @@
-(* Title: Pure/Isar/outer_lex.ML
- Author: Markus Wenzel, TU Muenchen
-
-Outer lexical syntax for Isabelle/Isar.
-*)
-
-signature OUTER_LEX =
-sig
- datatype token_kind =
- Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
- Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
- Malformed | Error of string | Sync | EOF
- datatype value =
- Text of string | Typ of typ | Term of term | Fact of thm list |
- Attribute of morphism -> attribute
- type token
- val str_of_kind: token_kind -> string
- val position_of: token -> Position.T
- val end_position_of: token -> Position.T
- val pos_of: token -> string
- val eof: token
- val is_eof: token -> bool
- val not_eof: token -> bool
- val not_sync: token -> bool
- val stopper: token Scan.stopper
- val kind_of: token -> token_kind
- val is_kind: token_kind -> token -> bool
- val keyword_with: (string -> bool) -> token -> bool
- val ident_with: (string -> bool) -> token -> bool
- val is_proper: token -> bool
- val is_semicolon: token -> bool
- val is_comment: token -> bool
- val is_begin_ignore: token -> bool
- val is_end_ignore: token -> bool
- val is_blank: token -> bool
- val is_newline: token -> bool
- val source_of: token -> string
- val source_position_of: token -> Symbol_Pos.text * Position.T
- val content_of: token -> string
- val unparse: token -> string
- val text_of: token -> string * string
- val get_value: token -> value option
- val map_value: (value -> value) -> token -> token
- val mk_text: string -> token
- val mk_typ: typ -> token
- val mk_term: term -> token
- val mk_fact: thm list -> token
- val mk_attribute: (morphism -> attribute) -> token
- val assignable: token -> token
- val assign: value option -> token -> unit
- val closure: token -> token
- val ident_or_symbolic: string -> bool
- val !!! : string -> (Symbol_Pos.T list -> 'a) -> Symbol_Pos.T list -> 'a
- val source_proper: (token, 'a) Source.source -> (token, (token, 'a) Source.source) Source.source
- val source': {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
- (Symbol_Pos.T, 'a) Source.source -> (token, (Symbol_Pos.T, 'a) Source.source) Source.source
- val source: {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
- Position.T -> (Symbol.symbol, 'a) Source.source -> (token,
- (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
- val read_antiq: Scan.lexicon -> (token list -> 'a * token list) ->
- Symbol_Pos.T list * Position.T -> 'a
-end;
-
-structure OuterLex: OUTER_LEX =
-struct
-
-(** tokens **)
-
-(* token values *)
-
-(*The value slot assigns an (optional) internal value to a token,
- usually as a side-effect of special scanner setup (see also
- args.ML). Note that an assignable ref designates an intermediate
- state of internalization -- it is NOT meant to persist.*)
-
-datatype value =
- Text of string |
- Typ of typ |
- Term of term |
- Fact of thm list |
- Attribute of morphism -> attribute;
-
-datatype slot =
- Slot |
- Value of value option |
- Assignable of value option Unsynchronized.ref;
-
-
-(* datatype token *)
-
-datatype token_kind =
- Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
- Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
- Malformed | Error of string | Sync | EOF;
-
-datatype token = Token of (Symbol_Pos.text * Position.range) * (token_kind * string) * slot;
-
-val str_of_kind =
- fn Command => "command"
- | Keyword => "keyword"
- | Ident => "identifier"
- | LongIdent => "long identifier"
- | SymIdent => "symbolic identifier"
- | Var => "schematic variable"
- | TypeIdent => "type variable"
- | TypeVar => "schematic type variable"
- | Nat => "number"
- | String => "string"
- | AltString => "back-quoted string"
- | Verbatim => "verbatim text"
- | Space => "white space"
- | Comment => "comment text"
- | InternalValue => "internal value"
- | Malformed => "malformed symbolic character"
- | Error _ => "bad input"
- | Sync => "sync marker"
- | EOF => "end-of-file";
-
-
-(* position *)
-
-fun position_of (Token ((_, (pos, _)), _, _)) = pos;
-fun end_position_of (Token ((_, (_, pos)), _, _)) = pos;
-
-val pos_of = Position.str_of o position_of;
-
-
-(* control tokens *)
-
-fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot);
-val eof = mk_eof Position.none;
-
-fun is_eof (Token (_, (EOF, _), _)) = true
- | is_eof _ = false;
-
-val not_eof = not o is_eof;
-
-fun not_sync (Token (_, (Sync, _), _)) = false
- | not_sync _ = true;
-
-val stopper =
- Scan.stopper (fn [] => eof | toks => mk_eof (end_position_of (List.last toks))) is_eof;
-
-
-(* kind of token *)
-
-fun kind_of (Token (_, (k, _), _)) = k;
-fun is_kind k (Token (_, (k', _), _)) = k = k';
-
-fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
- | keyword_with _ _ = false;
-
-fun ident_with pred (Token (_, (Ident, x), _)) = pred x
- | ident_with _ _ = false;
-
-fun is_proper (Token (_, (Space, _), _)) = false
- | is_proper (Token (_, (Comment, _), _)) = false
- | is_proper _ = true;
-
-fun is_semicolon (Token (_, (Keyword, ";"), _)) = true
- | is_semicolon _ = false;
-
-fun is_comment (Token (_, (Comment, _), _)) = true
- | is_comment _ = false;
-
-fun is_begin_ignore (Token (_, (Comment, "<"), _)) = true
- | is_begin_ignore _ = false;
-
-fun is_end_ignore (Token (_, (Comment, ">"), _)) = true
- | is_end_ignore _ = false;
-
-
-(* blanks and newlines -- space tokens obey lines *)
-
-fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x)
- | is_blank _ = false;
-
-fun is_newline (Token (_, (Space, x), _)) = String.isSuffix "\n" x
- | is_newline _ = false;
-
-
-(* token content *)
-
-fun source_of (Token ((source, (pos, _)), _, _)) =
- YXML.string_of (XML.Elem (Markup.tokenN, Position.properties_of pos, [XML.Text source]));
-
-fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
-
-fun content_of (Token (_, (_, x), _)) = x;
-
-
-(* unparse *)
-
-fun escape q =
- implode o map (fn s => if s = q orelse s = "\\" then "\\" ^ s else s) o Symbol.explode;
-
-fun unparse (Token (_, (kind, x), _)) =
- (case kind of
- String => x |> quote o escape "\""
- | AltString => x |> enclose "`" "`" o escape "`"
- | Verbatim => x |> enclose "{*" "*}"
- | Comment => x |> enclose "(*" "*)"
- | Malformed => space_implode " " (explode x)
- | Sync => ""
- | EOF => ""
- | _ => x);
-
-fun text_of tok =
- if is_semicolon tok then ("terminator", "")
- else
- let
- val k = str_of_kind (kind_of tok);
- val s = unparse tok
- handle ERROR _ => Symbol.separate_chars (content_of tok);
- in
- if s = "" then (k, "")
- else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ s, "")
- else (k, s)
- end;
-
-
-
-(** associated values **)
-
-(* access values *)
-
-fun get_value (Token (_, _, Value v)) = v
- | get_value _ = NONE;
-
-fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v)))
- | map_value _ tok = tok;
-
-
-(* make values *)
-
-fun mk_value k v = Token ((k, Position.no_range), (InternalValue, k), Value (SOME v));
-
-val mk_text = mk_value "<text>" o Text;
-val mk_typ = mk_value "<typ>" o Typ;
-val mk_term = mk_value "<term>" o Term;
-val mk_fact = mk_value "<fact>" o Fact;
-val mk_attribute = mk_value "<attribute>" o Attribute;
-
-
-(* static binding *)
-
-(*1st stage: make empty slots assignable*)
-fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE))
- | assignable tok = tok;
-
-(*2nd stage: assign values as side-effect of scanning*)
-fun assign v (Token (_, _, Assignable r)) = r := v
- | assign _ _ = ();
-
-(*3rd stage: static closure of final values*)
-fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v)
- | closure tok = tok;
-
-
-
-(** scanners **)
-
-open Basic_Symbol_Pos;
-
-fun !!! msg = Symbol_Pos.!!! ("Outer lexical error: " ^ msg);
-
-
-(* scan symbolic idents *)
-
-val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
-
-val scan_symid =
- Scan.many1 (is_sym_char o symbol) ||
- Scan.one (Symbol.is_symbolic o symbol) >> single;
-
-fun is_symid str =
- (case try Symbol.explode str of
- SOME [s] => Symbol.is_symbolic s orelse is_sym_char s
- | SOME ss => forall is_sym_char ss
- | _ => false);
-
-fun ident_or_symbolic "begin" = false
- | ident_or_symbolic ":" = true
- | ident_or_symbolic "::" = true
- | ident_or_symbolic s = Syntax.is_identifier s orelse is_symid s;
-
-
-(* scan verbatim text *)
-
-val scan_verb =
- $$$ "*" --| Scan.ahead (~$$$ "}") ||
- Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
-
-val scan_verbatim =
- (Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text"
- (Symbol_Pos.change_prompt
- ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
-
-
-(* scan space *)
-
-fun is_space s = Symbol.is_blank s andalso s <> "\n";
-
-val scan_space =
- Scan.many1 (is_space o symbol) @@@ Scan.optional ($$$ "\n") [] ||
- Scan.many (is_space o symbol) @@@ $$$ "\n";
-
-
-(* scan comment *)
-
-val scan_comment =
- Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body !!! -- Symbol_Pos.scan_pos);
-
-
-(* scan malformed symbols *)
-
-val scan_malformed =
- $$$ Symbol.malformed |--
- Symbol_Pos.change_prompt (Scan.many (Symbol.is_regular o symbol))
- --| Scan.option ($$$ Symbol.end_malformed);
-
-
-
-(** token sources **)
-
-fun source_proper src = src |> Source.filter is_proper;
-
-local
-
-fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
-
-fun token k ss =
- Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.untabify_content ss), Slot);
-
-fun token_range k (pos1, (ss, pos2)) =
- Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.untabify_content ss), Slot);
-
-fun scan (lex1, lex2) = !!! "bad input"
- (Symbol_Pos.scan_string >> token_range String ||
- Symbol_Pos.scan_alt_string >> token_range AltString ||
- scan_verbatim >> token_range Verbatim ||
- scan_comment >> token_range Comment ||
- scan_space >> token Space ||
- scan_malformed >> token Malformed ||
- Scan.one (Symbol.is_sync o symbol) >> (token Sync o single) ||
- (Scan.max token_leq
- (Scan.max token_leq
- (Scan.literal lex2 >> pair Command)
- (Scan.literal lex1 >> pair Keyword))
- (Syntax.scan_longid >> pair LongIdent ||
- Syntax.scan_id >> pair Ident ||
- Syntax.scan_var >> pair Var ||
- Syntax.scan_tid >> pair TypeIdent ||
- Syntax.scan_tvar >> pair TypeVar ||
- Syntax.scan_nat >> pair Nat ||
- scan_symid >> pair SymIdent) >> uncurry token));
-
-fun recover msg =
- Scan.many ((Symbol.is_regular andf (not o Symbol.is_blank)) o symbol)
- >> (single o token (Error msg));
-
-in
-
-fun source' {do_recover} get_lex =
- Source.source Symbol_Pos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
- (Option.map (rpair recover) do_recover);
-
-fun source do_recover get_lex pos src =
- Symbol_Pos.source pos src
- |> source' do_recover get_lex;
-
-end;
-
-
-(* read_antiq *)
-
-fun read_antiq lex scan (syms, pos) =
- let
- fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
- "@{" ^ Symbol_Pos.content syms ^ "}");
-
- val res =
- Source.of_list syms
- |> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
- |> source_proper
- |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE
- |> Source.exhaust;
- in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
-
-end;
--- a/src/Pure/Isar/outer_lex.scala Mon May 17 18:59:59 2010 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,94 +0,0 @@
-/* Title: Pure/Isar/outer_lex.scala
- Author: Makarius
-
-Outer lexical syntax for Isabelle/Isar.
-*/
-
-package isabelle
-
-
-object Outer_Lex
-{
- /* tokens */
-
- object Token_Kind extends Enumeration
- {
- val COMMAND = Value("command")
- val KEYWORD = Value("keyword")
- val IDENT = Value("identifier")
- val LONG_IDENT = Value("long identifier")
- val SYM_IDENT = Value("symbolic identifier")
- val VAR = Value("schematic variable")
- val TYPE_IDENT = Value("type variable")
- val TYPE_VAR = Value("schematic type variable")
- val NAT = Value("number")
- val STRING = Value("string")
- val ALT_STRING = Value("back-quoted string")
- val VERBATIM = Value("verbatim text")
- val SPACE = Value("white space")
- val COMMENT = Value("comment text")
- val BAD_INPUT = Value("bad input")
- val UNPARSED = Value("unparsed input")
- }
-
- sealed case class Token(val kind: Token_Kind.Value, val source: String)
- {
- def is_command: Boolean = kind == Token_Kind.COMMAND
- def is_delimited: Boolean =
- kind == Token_Kind.STRING ||
- kind == Token_Kind.ALT_STRING ||
- kind == Token_Kind.VERBATIM ||
- kind == Token_Kind.COMMENT
- def is_name: Boolean =
- kind == Token_Kind.IDENT ||
- kind == Token_Kind.SYM_IDENT ||
- kind == Token_Kind.STRING ||
- kind == Token_Kind.NAT
- def is_xname: Boolean = is_name || kind == Token_Kind.LONG_IDENT
- def is_text: Boolean = is_xname || kind == Token_Kind.VERBATIM
- def is_space: Boolean = kind == Token_Kind.SPACE
- def is_comment: Boolean = kind == Token_Kind.COMMENT
- def is_ignored: Boolean = is_space || is_comment
- def is_unparsed: Boolean = kind == Token_Kind.UNPARSED
-
- def content: String =
- if (kind == Token_Kind.STRING) Scan.Lexicon.empty.quoted_content("\"", source)
- else if (kind == Token_Kind.ALT_STRING) Scan.Lexicon.empty.quoted_content("`", source)
- else if (kind == Token_Kind.VERBATIM) Scan.Lexicon.empty.verbatim_content(source)
- else if (kind == Token_Kind.COMMENT) Scan.Lexicon.empty.comment_content(source)
- else source
-
- def text: (String, String) =
- if (kind == Token_Kind.COMMAND && source == ";") ("terminator", "")
- else (kind.toString, source)
- }
-
-
- /* token reader */
-
- class Line_Position(val line: Int) extends scala.util.parsing.input.Position
- {
- def column = 0
- def lineContents = ""
- override def toString = line.toString
-
- def advance(token: Token): Line_Position =
- {
- var n = 0
- for (c <- token.content if c == '\n') n += 1
- if (n == 0) this else new Line_Position(line + n)
- }
- }
-
- abstract class Reader extends scala.util.parsing.input.Reader[Token]
-
- private class Token_Reader(tokens: List[Token], val pos: Line_Position) extends Reader
- {
- def first = tokens.head
- def rest = new Token_Reader(tokens.tail, pos.advance(first))
- def atEnd = tokens.isEmpty
- }
-
- def reader(tokens: List[Token]): Reader = new Token_Reader(tokens, new Line_Position(1))
-}
-
--- a/src/Pure/Isar/outer_syntax.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Isar/outer_syntax.ML Tue May 18 06:28:42 2010 -0700
@@ -25,7 +25,7 @@
val local_theory_to_proof: string -> string -> Keyword.T ->
(local_theory -> Proof.state) parser -> unit
val print_outer_syntax: unit -> unit
- val scan: Position.T -> string -> OuterLex.token list
+ val scan: Position.T -> string -> Token.T list
val parse: Position.T -> string -> Toplevel.transition list
val process_file: Path.T -> theory -> theory
type isar
@@ -37,11 +37,6 @@
structure Outer_Syntax: OUTER_SYNTAX =
struct
-structure T = OuterLex;
-type 'a parser = 'a Parse.parser;
-
-
-
(** outer syntax **)
(* command parsers *)
@@ -171,17 +166,17 @@
fun toplevel_source term do_recover cmd src =
let
val no_terminator =
- Scan.unless Parse.semicolon (Scan.one (T.not_sync andf T.not_eof));
+ Scan.unless Parse.semicolon (Scan.one (Token.not_sync andf Token.not_eof));
fun recover int =
(int, fn _ => Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]);
in
src
- |> T.source_proper
- |> Source.source T.stopper
+ |> Token.source_proper
+ |> Source.source Token.stopper
(Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.doc_source >> K NONE || Parse.not_eof >> SOME))
(Option.map recover do_recover)
|> Source.map_filter I
- |> Source.source T.stopper
+ |> Source.source Token.stopper
(Scan.bulk (fn xs => Parse.!!! (parse_command term (cmd ())) xs))
(Option.map recover do_recover)
|> Source.map_filter I
@@ -193,13 +188,13 @@
fun scan pos str =
Source.of_string str
|> Symbol.source {do_recover = false}
- |> T.source {do_recover = SOME false} Keyword.get_lexicons pos
+ |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
|> Source.exhaust;
fun parse pos str =
Source.of_string str
|> Symbol.source {do_recover = false}
- |> T.source {do_recover = SOME false} Keyword.get_lexicons pos
+ |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos
|> toplevel_source false NONE get_command
|> Source.exhaust;
@@ -222,7 +217,7 @@
type isar =
(Toplevel.transition, (Toplevel.transition option,
- (OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token,
+ (Token.T, (Token.T option, (Token.T, (Token.T,
(Symbol_Pos.T, Position.T * (Symbol.symbol, (string, unit) Source.source)
Source.source) Source.source) Source.source) Source.source)
Source.source) Source.source) Source.source) Source.source;
@@ -230,7 +225,7 @@
fun isar term : isar =
Source.tty
|> Symbol.source {do_recover = true}
- |> T.source {do_recover = SOME true} Keyword.get_lexicons Position.none
+ |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
|> toplevel_source term (SOME true) get_command;
@@ -297,6 +292,3 @@
end;
-(*legacy alias*)
-structure OuterSyntax = Outer_Syntax;
-
--- a/src/Pure/Isar/outer_syntax.scala Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Isar/outer_syntax.scala Tue May 18 06:28:42 2010 -0700
@@ -39,7 +39,7 @@
/* tokenize */
- def scan(input: Reader[Char]): List[Outer_Lex.Token] =
+ def scan(input: Reader[Char]): List[Token] =
{
import lexicon._
@@ -49,6 +49,6 @@
}
}
- def scan(input: CharSequence): List[Outer_Lex.Token] =
+ def scan(input: CharSequence): List[Token] =
scan(new CharSequenceReader(input))
}
--- a/src/Pure/Isar/parse.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Isar/parse.ML Tue May 18 06:28:42 2010 -0700
@@ -6,17 +6,16 @@
signature PARSE =
sig
- type token = OuterLex.token
- type 'a parser = token list -> 'a * token list
- type 'a context_parser = Context.generic * token list -> 'a * (Context.generic * token list)
- val group: string -> (token list -> 'a) -> token list -> 'a
- val !!! : (token list -> 'a) -> token list -> 'a
- val !!!! : (token list -> 'a) -> token list -> 'a
+ type 'a parser = Token.T list -> 'a * Token.T list
+ type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list)
+ val group: string -> (Token.T list -> 'a) -> Token.T list -> 'a
+ val !!! : (Token.T list -> 'a) -> Token.T list -> 'a
+ val !!!! : (Token.T list -> 'a) -> Token.T list -> 'a
val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
- val not_eof: token parser
- val position: (token list -> 'a * 'b) -> token list -> ('a * Position.T) * 'b
+ val not_eof: Token.T parser
+ val position: (Token.T list -> 'a * 'b) -> Token.T list -> ('a * Position.T) * 'b
val command: string parser
val keyword: string parser
val short_ident: string parser
@@ -98,11 +97,8 @@
structure Parse: PARSE =
struct
-structure T = OuterLex;
-type token = T.token;
-
-type 'a parser = token list -> 'a * token list;
-type 'a context_parser = Context.generic * token list -> 'a * (Context.generic * token list);
+type 'a parser = Token.T list -> 'a * Token.T list;
+type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list);
(** error handling **)
@@ -112,9 +108,11 @@
fun fail_with s = Scan.fail_with
(fn [] => s ^ " expected (past end-of-file!)"
| (tok :: _) =>
- (case T.text_of tok of
- (txt, "") => s ^ " expected,\nbut " ^ txt ^ T.pos_of tok ^ " was found"
- | (txt1, txt2) => s ^ " expected,\nbut " ^ txt1 ^ T.pos_of tok ^ " was found:\n" ^ txt2));
+ (case Token.text_of tok of
+ (txt, "") =>
+ s ^ " expected,\nbut " ^ txt ^ Token.pos_of tok ^ " was found"
+ | (txt1, txt2) =>
+ s ^ " expected,\nbut " ^ txt1 ^ Token.pos_of tok ^ " was found:\n" ^ txt2));
fun group s scan = scan || fail_with s;
@@ -124,7 +122,7 @@
fun cut kind scan =
let
fun get_pos [] = " (past end-of-file!)"
- | get_pos (tok :: _) = T.pos_of tok;
+ | get_pos (tok :: _) = Token.pos_of tok;
fun err (toks, NONE) = kind ^ get_pos toks
| err (toks, SOME msg) =
@@ -149,42 +147,42 @@
(* tokens *)
fun RESET_VALUE atom = (*required for all primitive parsers*)
- Scan.ahead (Scan.one (K true)) -- atom >> (fn (arg, x) => (T.assign NONE arg; x));
+ Scan.ahead (Scan.one (K true)) -- atom >> (fn (arg, x) => (Token.assign NONE arg; x));
-val not_eof = RESET_VALUE (Scan.one T.not_eof);
+val not_eof = RESET_VALUE (Scan.one Token.not_eof);
-fun position scan = (Scan.ahead not_eof >> T.position_of) -- scan >> Library.swap;
-fun source_position atom = Scan.ahead atom |-- not_eof >> T.source_position_of;
-fun inner_syntax atom = Scan.ahead atom |-- not_eof >> T.source_of;
+fun position scan = (Scan.ahead not_eof >> Token.position_of) -- scan >> Library.swap;
+fun source_position atom = Scan.ahead atom |-- not_eof >> Token.source_position_of;
+fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.source_of;
fun kind k =
- group (T.str_of_kind k) (RESET_VALUE (Scan.one (T.is_kind k) >> T.content_of));
+ group (Token.str_of_kind k) (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.content_of));
-val command = kind T.Command;
-val keyword = kind T.Keyword;
-val short_ident = kind T.Ident;
-val long_ident = kind T.LongIdent;
-val sym_ident = kind T.SymIdent;
-val term_var = kind T.Var;
-val type_ident = kind T.TypeIdent;
-val type_var = kind T.TypeVar;
-val number = kind T.Nat;
-val string = kind T.String;
-val alt_string = kind T.AltString;
-val verbatim = kind T.Verbatim;
-val sync = kind T.Sync;
-val eof = kind T.EOF;
+val command = kind Token.Command;
+val keyword = kind Token.Keyword;
+val short_ident = kind Token.Ident;
+val long_ident = kind Token.LongIdent;
+val sym_ident = kind Token.SymIdent;
+val term_var = kind Token.Var;
+val type_ident = kind Token.TypeIdent;
+val type_var = kind Token.TypeVar;
+val number = kind Token.Nat;
+val string = kind Token.String;
+val alt_string = kind Token.AltString;
+val verbatim = kind Token.Verbatim;
+val sync = kind Token.Sync;
+val eof = kind Token.EOF;
-fun keyword_with pred = RESET_VALUE (Scan.one (T.keyword_with pred) >> T.content_of);
-val keyword_ident_or_symbolic = keyword_with T.ident_or_symbolic;
+fun keyword_with pred = RESET_VALUE (Scan.one (Token.keyword_with pred) >> Token.content_of);
+val keyword_ident_or_symbolic = keyword_with Token.ident_or_symbolic;
fun $$$ x =
- group (T.str_of_kind T.Keyword ^ " " ^ quote x) (keyword_with (fn y => x = y));
+ group (Token.str_of_kind Token.Keyword ^ " " ^ quote x) (keyword_with (fn y => x = y));
fun reserved x =
group ("reserved identifier " ^ quote x)
- (RESET_VALUE (Scan.one (T.ident_with (fn y => x = y)) >> T.content_of));
+ (RESET_VALUE (Scan.one (Token.ident_with (fn y => x = y)) >> Token.content_of));
val semicolon = $$$ ";";
@@ -341,6 +339,3 @@
type 'a parser = 'a Parse.parser;
type 'a context_parser = 'a Parse.context_parser;
-(*legacy alias*)
-structure OuterParse = Parse;
-
--- a/src/Pure/Isar/parse.scala Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Isar/parse.scala Tue May 18 06:28:42 2010 -0700
@@ -15,7 +15,7 @@
trait Parser extends Parsers
{
- type Elem = Outer_Lex.Token
+ type Elem = Token
def filter_proper = true
@@ -50,8 +50,8 @@
token(s, pred) ^^ (_.content)
def keyword(name: String): Parser[String] =
- atom(Outer_Lex.Token_Kind.KEYWORD.toString + " \"" + name + "\"",
- tok => tok.kind == Outer_Lex.Token_Kind.KEYWORD && tok.content == name)
+ atom(Token.Kind.KEYWORD.toString + " \"" + name + "\"",
+ tok => tok.kind == Token.Kind.KEYWORD && tok.content == name)
def name: Parser[String] = atom("name declaration", _.is_name)
def xname: Parser[String] = atom("name reference", _.is_xname)
@@ -62,16 +62,16 @@
private def tag_name: Parser[String] =
atom("tag name", tok =>
- tok.kind == Outer_Lex.Token_Kind.IDENT ||
- tok.kind == Outer_Lex.Token_Kind.STRING)
+ tok.kind == Token.Kind.IDENT ||
+ tok.kind == Token.Kind.STRING)
def tags: Parser[List[String]] = rep(keyword("%") ~> tag_name)
/* wrappers */
- def parse[T](p: Parser[T], in: Outer_Lex.Reader): ParseResult[T] = p(in)
- def parse_all[T](p: Parser[T], in: Outer_Lex.Reader): ParseResult[T] = parse(phrase(p), in)
+ def parse[T](p: Parser[T], in: Token.Reader): ParseResult[T] = p(in)
+ def parse_all[T](p: Parser[T], in: Token.Reader): ParseResult[T] = parse(phrase(p), in)
}
}
--- a/src/Pure/Isar/parse_spec.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Isar/parse_spec.ML Tue May 18 06:28:42 2010 -0700
@@ -162,6 +162,3 @@
end;
-(*legacy alias*)
-structure SpecParse = Parse_Spec;
-
--- a/src/Pure/Isar/rule_insts.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Isar/rule_insts.ML Tue May 18 06:28:42 2010 -0700
@@ -29,9 +29,6 @@
structure RuleInsts: RULE_INSTS =
struct
-structure T = OuterLex;
-
-
(** reading instantiations **)
local
@@ -100,11 +97,11 @@
val (type_insts, term_insts) = List.partition (is_tvar o fst) mixed_insts;
val internal_insts = term_insts |> map_filter
- (fn (xi, T.Term t) => SOME (xi, t)
- | (_, T.Text _) => NONE
+ (fn (xi, Token.Term t) => SOME (xi, t)
+ | (_, Token.Text _) => NONE
| (xi, _) => error_var "Term argument expected for " xi);
val external_insts = term_insts |> map_filter
- (fn (xi, T.Text s) => SOME (xi, s) | _ => NONE);
+ (fn (xi, Token.Text s) => SOME (xi, s) | _ => NONE);
(* mixed type instantiations *)
@@ -114,8 +111,8 @@
val S = the_sort tvars xi;
val T =
(case arg of
- T.Text s => Syntax.read_typ ctxt s
- | T.Typ T => T
+ Token.Text s => Syntax.read_typ ctxt s
+ | Token.Typ T => T
| _ => error_var "Type argument expected for " xi);
in
if Sign.of_sort thy (T, S) then ((xi, S), T)
@@ -172,9 +169,9 @@
val _ = (*assign internalized values*)
mixed_insts |> List.app (fn (arg, (xi, _)) =>
if is_tvar xi then
- T.assign (SOME (T.Typ (the (AList.lookup (op =) type_insts xi)))) arg
+ Token.assign (SOME (Token.Typ (the (AList.lookup (op =) type_insts xi)))) arg
else
- T.assign (SOME (T.Term (the (AList.lookup (op =) term_insts xi)))) arg);
+ Token.assign (SOME (Token.Term (the (AList.lookup (op =) term_insts xi)))) arg);
in
Drule.instantiate insts thm |> Rule_Cases.save thm
end;
@@ -197,7 +194,7 @@
fun read_instantiate ctxt args thm =
read_instantiate_mixed (ctxt |> ProofContext.set_mode ProofContext.mode_schematic) (* FIXME !? *)
- (map (fn (x, y) => (T.eof, (x, T.Text y))) args) thm;
+ (map (fn (x, y) => (Token.eof, (x, Token.Text y))) args) thm;
fun instantiate_tac ctxt args = PRIMITIVE (read_instantiate ctxt args);
@@ -210,9 +207,9 @@
local
val value =
- Args.internal_typ >> T.Typ ||
- Args.internal_term >> T.Term ||
- Args.name_source >> T.Text;
+ Args.internal_typ >> Token.Typ ||
+ Args.internal_term >> Token.Term ||
+ Args.name_source >> Token.Text;
val inst = Args.var -- (Args.$$$ "=" |-- Scan.ahead Parse.not_eof -- value)
>> (fn (xi, (a, v)) => (a, (xi, v)));
@@ -233,8 +230,8 @@
local
val value =
- Args.internal_term >> T.Term ||
- Args.name_source >> T.Text;
+ Args.internal_term >> Token.Term ||
+ Args.name_source >> Token.Text;
val inst = Scan.ahead Parse.not_eof -- Args.maybe value;
val concl = Args.$$$ "concl" -- Args.colon;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/token.ML Tue May 18 06:28:42 2010 -0700
@@ -0,0 +1,389 @@
+(* Title: Pure/Isar/token.ML
+ Author: Markus Wenzel, TU Muenchen
+
+Outer token syntax for Isabelle/Isar.
+*)
+
+signature TOKEN =
+sig
+ datatype kind =
+ Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
+ Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
+ Malformed | Error of string | Sync | EOF
+ datatype value =
+ Text of string | Typ of typ | Term of term | Fact of thm list |
+ Attribute of morphism -> attribute
+ type T
+ val str_of_kind: kind -> string
+ val position_of: T -> Position.T
+ val end_position_of: T -> Position.T
+ val pos_of: T -> string
+ val eof: T
+ val is_eof: T -> bool
+ val not_eof: T -> bool
+ val not_sync: T -> bool
+ val stopper: T Scan.stopper
+ val kind_of: T -> kind
+ val is_kind: kind -> T -> bool
+ val keyword_with: (string -> bool) -> T -> bool
+ val ident_with: (string -> bool) -> T -> bool
+ val is_proper: T -> bool
+ val is_semicolon: T -> bool
+ val is_comment: T -> bool
+ val is_begin_ignore: T -> bool
+ val is_end_ignore: T -> bool
+ val is_blank: T -> bool
+ val is_newline: T -> bool
+ val source_of: T -> string
+ val source_position_of: T -> Symbol_Pos.text * Position.T
+ val content_of: T -> string
+ val unparse: T -> string
+ val text_of: T -> string * string
+ val get_value: T -> value option
+ val map_value: (value -> value) -> T -> T
+ val mk_text: string -> T
+ val mk_typ: typ -> T
+ val mk_term: term -> T
+ val mk_fact: thm list -> T
+ val mk_attribute: (morphism -> attribute) -> T
+ val assignable: T -> T
+ val assign: value option -> T -> unit
+ val closure: T -> T
+ val ident_or_symbolic: string -> bool
+ val !!! : string -> (Symbol_Pos.T list -> 'a) -> Symbol_Pos.T list -> 'a
+ val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
+ val source': {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
+ (Symbol_Pos.T, 'a) Source.source -> (T, (Symbol_Pos.T, 'a) Source.source) Source.source
+ val source: {do_recover: bool Option.option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
+ Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
+ (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
+ val read_antiq: Scan.lexicon -> (T list -> 'a * T list) -> Symbol_Pos.T list * Position.T -> 'a
+end;
+
+structure Token: TOKEN =
+struct
+
+(** tokens **)
+
+(* token values *)
+
+(*The value slot assigns an (optional) internal value to a token,
+ usually as a side-effect of special scanner setup (see also
+ args.ML). Note that an assignable ref designates an intermediate
+ state of internalization -- it is NOT meant to persist.*)
+
+datatype value =
+ Text of string |
+ Typ of typ |
+ Term of term |
+ Fact of thm list |
+ Attribute of morphism -> attribute;
+
+datatype slot =
+ Slot |
+ Value of value option |
+ Assignable of value option Unsynchronized.ref;
+
+
+(* datatype token *)
+
+datatype kind =
+ Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
+ Nat | String | AltString | Verbatim | Space | Comment | InternalValue |
+ Malformed | Error of string | Sync | EOF;
+
+datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot;
+
+val str_of_kind =
+ fn Command => "command"
+ | Keyword => "keyword"
+ | Ident => "identifier"
+ | LongIdent => "long identifier"
+ | SymIdent => "symbolic identifier"
+ | Var => "schematic variable"
+ | TypeIdent => "type variable"
+ | TypeVar => "schematic type variable"
+ | Nat => "number"
+ | String => "string"
+ | AltString => "back-quoted string"
+ | Verbatim => "verbatim text"
+ | Space => "white space"
+ | Comment => "comment text"
+ | InternalValue => "internal value"
+ | Malformed => "malformed symbolic character"
+ | Error _ => "bad input"
+ | Sync => "sync marker"
+ | EOF => "end-of-file";
+
+
+(* position *)
+
+fun position_of (Token ((_, (pos, _)), _, _)) = pos;
+fun end_position_of (Token ((_, (_, pos)), _, _)) = pos;
+
+val pos_of = Position.str_of o position_of;
+
+
+(* control tokens *)
+
+fun mk_eof pos = Token (("", (pos, Position.none)), (EOF, ""), Slot);
+val eof = mk_eof Position.none;
+
+fun is_eof (Token (_, (EOF, _), _)) = true
+ | is_eof _ = false;
+
+val not_eof = not o is_eof;
+
+fun not_sync (Token (_, (Sync, _), _)) = false
+ | not_sync _ = true;
+
+val stopper =
+ Scan.stopper (fn [] => eof | toks => mk_eof (end_position_of (List.last toks))) is_eof;
+
+
+(* kind of token *)
+
+fun kind_of (Token (_, (k, _), _)) = k;
+fun is_kind k (Token (_, (k', _), _)) = k = k';
+
+fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
+ | keyword_with _ _ = false;
+
+fun ident_with pred (Token (_, (Ident, x), _)) = pred x
+ | ident_with _ _ = false;
+
+fun is_proper (Token (_, (Space, _), _)) = false
+ | is_proper (Token (_, (Comment, _), _)) = false
+ | is_proper _ = true;
+
+fun is_semicolon (Token (_, (Keyword, ";"), _)) = true
+ | is_semicolon _ = false;
+
+fun is_comment (Token (_, (Comment, _), _)) = true
+ | is_comment _ = false;
+
+fun is_begin_ignore (Token (_, (Comment, "<"), _)) = true
+ | is_begin_ignore _ = false;
+
+fun is_end_ignore (Token (_, (Comment, ">"), _)) = true
+ | is_end_ignore _ = false;
+
+
+(* blanks and newlines -- space tokens obey lines *)
+
+fun is_blank (Token (_, (Space, x), _)) = not (String.isSuffix "\n" x)
+ | is_blank _ = false;
+
+fun is_newline (Token (_, (Space, x), _)) = String.isSuffix "\n" x
+ | is_newline _ = false;
+
+
+(* token content *)
+
+fun source_of (Token ((source, (pos, _)), _, _)) =
+ YXML.string_of (XML.Elem (Markup.tokenN, Position.properties_of pos, [XML.Text source]));
+
+fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
+
+fun content_of (Token (_, (_, x), _)) = x;
+
+
+(* unparse *)
+
+fun escape q =
+ implode o map (fn s => if s = q orelse s = "\\" then "\\" ^ s else s) o Symbol.explode;
+
+fun unparse (Token (_, (kind, x), _)) =
+ (case kind of
+ String => x |> quote o escape "\""
+ | AltString => x |> enclose "`" "`" o escape "`"
+ | Verbatim => x |> enclose "{*" "*}"
+ | Comment => x |> enclose "(*" "*)"
+ | Malformed => space_implode " " (explode x)
+ | Sync => ""
+ | EOF => ""
+ | _ => x);
+
+fun text_of tok =
+ if is_semicolon tok then ("terminator", "")
+ else
+ let
+ val k = str_of_kind (kind_of tok);
+ val s = unparse tok
+ handle ERROR _ => Symbol.separate_chars (content_of tok);
+ in
+ if s = "" then (k, "")
+ else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ s, "")
+ else (k, s)
+ end;
+
+
+
+(** associated values **)
+
+(* access values *)
+
+fun get_value (Token (_, _, Value v)) = v
+ | get_value _ = NONE;
+
+fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v)))
+ | map_value _ tok = tok;
+
+
+(* make values *)
+
+fun mk_value k v = Token ((k, Position.no_range), (InternalValue, k), Value (SOME v));
+
+val mk_text = mk_value "<text>" o Text;
+val mk_typ = mk_value "<typ>" o Typ;
+val mk_term = mk_value "<term>" o Term;
+val mk_fact = mk_value "<fact>" o Fact;
+val mk_attribute = mk_value "<attribute>" o Attribute;
+
+
+(* static binding *)
+
+(*1st stage: make empty slots assignable*)
+fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE))
+ | assignable tok = tok;
+
+(*2nd stage: assign values as side-effect of scanning*)
+fun assign v (Token (_, _, Assignable r)) = r := v
+ | assign _ _ = ();
+
+(*3rd stage: static closure of final values*)
+fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v)
+ | closure tok = tok;
+
+
+
+(** scanners **)
+
+open Basic_Symbol_Pos;
+
+fun !!! msg = Symbol_Pos.!!! ("Outer lexical error: " ^ msg);
+
+
+(* scan symbolic idents *)
+
+val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
+
+val scan_symid =
+ Scan.many1 (is_sym_char o symbol) ||
+ Scan.one (Symbol.is_symbolic o symbol) >> single;
+
+fun is_symid str =
+ (case try Symbol.explode str of
+ SOME [s] => Symbol.is_symbolic s orelse is_sym_char s
+ | SOME ss => forall is_sym_char ss
+ | _ => false);
+
+fun ident_or_symbolic "begin" = false
+ | ident_or_symbolic ":" = true
+ | ident_or_symbolic "::" = true
+ | ident_or_symbolic s = Syntax.is_identifier s orelse is_symid s;
+
+
+(* scan verbatim text *)
+
+val scan_verb =
+ $$$ "*" --| Scan.ahead (~$$$ "}") ||
+ Scan.one (fn (s, _) => s <> "*" andalso Symbol.is_regular s) >> single;
+
+val scan_verbatim =
+ (Symbol_Pos.scan_pos --| $$$ "{" --| $$$ "*") -- !!! "missing end of verbatim text"
+ (Symbol_Pos.change_prompt
+ ((Scan.repeat scan_verb >> flat) -- ($$$ "*" |-- $$$ "}" |-- Symbol_Pos.scan_pos)));
+
+
+(* scan space *)
+
+fun is_space s = Symbol.is_blank s andalso s <> "\n";
+
+val scan_space =
+ Scan.many1 (is_space o symbol) @@@ Scan.optional ($$$ "\n") [] ||
+ Scan.many (is_space o symbol) @@@ $$$ "\n";
+
+
+(* scan comment *)
+
+val scan_comment =
+ Symbol_Pos.scan_pos -- (Symbol_Pos.scan_comment_body !!! -- Symbol_Pos.scan_pos);
+
+
+(* scan malformed symbols *)
+
+val scan_malformed =
+ $$$ Symbol.malformed |--
+ Symbol_Pos.change_prompt (Scan.many (Symbol.is_regular o symbol))
+ --| Scan.option ($$$ Symbol.end_malformed);
+
+
+
+(** token sources **)
+
+fun source_proper src = src |> Source.filter is_proper;
+
+local
+
+fun token_leq ((_, syms1), (_, syms2)) = length syms1 <= length syms2;
+
+fun token k ss =
+ Token ((Symbol_Pos.implode ss, Symbol_Pos.range ss), (k, Symbol_Pos.untabify_content ss), Slot);
+
+fun token_range k (pos1, (ss, pos2)) =
+ Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.untabify_content ss), Slot);
+
+fun scan (lex1, lex2) = !!! "bad input"
+ (Symbol_Pos.scan_string >> token_range String ||
+ Symbol_Pos.scan_alt_string >> token_range AltString ||
+ scan_verbatim >> token_range Verbatim ||
+ scan_comment >> token_range Comment ||
+ scan_space >> token Space ||
+ scan_malformed >> token Malformed ||
+ Scan.one (Symbol.is_sync o symbol) >> (token Sync o single) ||
+ (Scan.max token_leq
+ (Scan.max token_leq
+ (Scan.literal lex2 >> pair Command)
+ (Scan.literal lex1 >> pair Keyword))
+ (Syntax.scan_longid >> pair LongIdent ||
+ Syntax.scan_id >> pair Ident ||
+ Syntax.scan_var >> pair Var ||
+ Syntax.scan_tid >> pair TypeIdent ||
+ Syntax.scan_tvar >> pair TypeVar ||
+ Syntax.scan_nat >> pair Nat ||
+ scan_symid >> pair SymIdent) >> uncurry token));
+
+fun recover msg =
+ Scan.many ((Symbol.is_regular andf (not o Symbol.is_blank)) o symbol)
+ >> (single o token (Error msg));
+
+in
+
+fun source' {do_recover} get_lex =
+ Source.source Symbol_Pos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs))
+ (Option.map (rpair recover) do_recover);
+
+fun source do_recover get_lex pos src =
+ Symbol_Pos.source pos src
+ |> source' do_recover get_lex;
+
+end;
+
+
+(* read_antiq *)
+
+fun read_antiq lex scan (syms, pos) =
+ let
+ fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
+ "@{" ^ Symbol_Pos.content syms ^ "}");
+
+ val res =
+ Source.of_list syms
+ |> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
+ |> source_proper
+ |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE
+ |> Source.exhaust;
+ in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/token.scala Tue May 18 06:28:42 2010 -0700
@@ -0,0 +1,95 @@
+/* Title: Pure/Isar/token.scala
+ Author: Makarius
+
+Outer token syntax for Isabelle/Isar.
+*/
+
+package isabelle
+
+
+object Token
+{
+ /* tokens */
+
+ object Kind extends Enumeration
+ {
+ val COMMAND = Value("command")
+ val KEYWORD = Value("keyword")
+ val IDENT = Value("identifier")
+ val LONG_IDENT = Value("long identifier")
+ val SYM_IDENT = Value("symbolic identifier")
+ val VAR = Value("schematic variable")
+ val TYPE_IDENT = Value("type variable")
+ val TYPE_VAR = Value("schematic type variable")
+ val NAT = Value("number")
+ val STRING = Value("string")
+ val ALT_STRING = Value("back-quoted string")
+ val VERBATIM = Value("verbatim text")
+ val SPACE = Value("white space")
+ val COMMENT = Value("comment text")
+ val BAD_INPUT = Value("bad input")
+ val UNPARSED = Value("unparsed input")
+ }
+
+
+ /* token reader */
+
+ class Line_Position(val line: Int) extends scala.util.parsing.input.Position
+ {
+ def column = 0
+ def lineContents = ""
+ override def toString = line.toString
+
+ def advance(token: Token): Line_Position =
+ {
+ var n = 0
+ for (c <- token.content if c == '\n') n += 1
+ if (n == 0) this else new Line_Position(line + n)
+ }
+ }
+
+ abstract class Reader extends scala.util.parsing.input.Reader[Token]
+
+ private class Token_Reader(tokens: List[Token], val pos: Line_Position) extends Reader
+ {
+ def first = tokens.head
+ def rest = new Token_Reader(tokens.tail, pos.advance(first))
+ def atEnd = tokens.isEmpty
+ }
+
+ def reader(tokens: List[Token]): Reader = new Token_Reader(tokens, new Line_Position(1))
+}
+
+
+sealed case class Token(val kind: Token.Kind.Value, val source: String)
+{
+ def is_command: Boolean = kind == Token.Kind.COMMAND
+ def is_delimited: Boolean =
+ kind == Token.Kind.STRING ||
+ kind == Token.Kind.ALT_STRING ||
+ kind == Token.Kind.VERBATIM ||
+ kind == Token.Kind.COMMENT
+ def is_name: Boolean =
+ kind == Token.Kind.IDENT ||
+ kind == Token.Kind.SYM_IDENT ||
+ kind == Token.Kind.STRING ||
+ kind == Token.Kind.NAT
+ def is_xname: Boolean = is_name || kind == Token.Kind.LONG_IDENT
+ def is_text: Boolean = is_xname || kind == Token.Kind.VERBATIM
+ def is_space: Boolean = kind == Token.Kind.SPACE
+ def is_comment: Boolean = kind == Token.Kind.COMMENT
+ def is_ignored: Boolean = is_space || is_comment
+ def is_unparsed: Boolean = kind == Token.Kind.UNPARSED
+
+ def content: String =
+ if (kind == Token.Kind.STRING) Scan.Lexicon.empty.quoted_content("\"", source)
+ else if (kind == Token.Kind.ALT_STRING) Scan.Lexicon.empty.quoted_content("`", source)
+ else if (kind == Token.Kind.VERBATIM) Scan.Lexicon.empty.verbatim_content(source)
+ else if (kind == Token.Kind.COMMENT) Scan.Lexicon.empty.comment_content(source)
+ else source
+
+ def text: (String, String) =
+ if (kind == Token.Kind.COMMAND && source == ";") ("terminator", "")
+ else (kind.toString, source)
+}
+
--- a/src/Pure/ML/ml_context.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/ML/ml_context.ML Tue May 18 06:28:42 2010 -0700
@@ -112,8 +112,6 @@
local
-structure T = OuterLex;
-
val antiq =
Parse.!!! (Parse.position Parse.xname -- Args.parse --| Scan.ahead Parse.eof)
>> (fn ((x, pos), y) => Args.src ((x, y), pos));
@@ -144,7 +142,8 @@
| expand (Antiquote.Antiq (ss, range)) (scope, background) =
let
val context = Stack.top scope;
- val (f, context') = antiquotation (T.read_antiq lex antiq (ss, #1 range)) context;
+ val (f, context') =
+ antiquotation (Token.read_antiq lex antiq (ss, #1 range)) context;
val (decl, background') = f background;
val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
in (decl', (Stack.map_top (K context') scope, background')) end
--- a/src/Pure/PIDE/document.scala Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/PIDE/document.scala Tue May 18 06:28:42 2010 -0700
@@ -46,7 +46,7 @@
/* unparsed dummy commands */
def unparsed(source: String) =
- new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source)))
+ new Command(null, List(Token(Token.Kind.UNPARSED, source)))
def is_unparsed(command: Command) = command.id == null
--- a/src/Pure/ROOT.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/ROOT.ML Tue May 18 06:28:42 2010 -0700
@@ -167,7 +167,7 @@
use "Proof/proofchecker.ML";
(*outer syntax*)
-use "Isar/outer_lex.ML";
+use "Isar/token.ML";
use "Isar/keyword.ML";
use "Isar/parse.ML";
use "Isar/parse_value.ML";
@@ -292,3 +292,23 @@
use "pure_setup.ML";
+
+(* legacy aliases *)
+
+structure Legacy =
+struct
+
+structure OuterKeyword = Keyword;
+
+structure OuterLex =
+struct
+ open Token;
+ type token = T;
+end;
+
+structure OuterParse = Parse;
+structure OuterSyntax = Outer_Syntax;
+structure SpecParse = Parse_Spec;
+
+end;
+
--- a/src/Pure/Thy/latex.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Thy/latex.ML Tue May 18 06:28:42 2010 -0700
@@ -9,7 +9,7 @@
val output_known_symbols: (string -> bool) * (string -> bool) ->
Symbol.symbol list -> string
val output_symbols: Symbol.symbol list -> string
- val output_basic: OuterLex.token -> string
+ val output_basic: Token.T -> string
val output_markup: string -> string -> string
val output_markup_env: string -> string -> string
val output_verbatim: string -> string
@@ -99,24 +99,22 @@
(* token output *)
-structure T = OuterLex;
-
-val invisible_token = T.keyword_with (fn s => s = ";") orf T.is_kind T.Comment;
+val invisible_token = Token.keyword_with (fn s => s = ";") orf Token.is_kind Token.Comment;
fun output_basic tok =
- let val s = T.content_of tok in
+ let val s = Token.content_of tok in
if invisible_token tok then ""
- else if T.is_kind T.Command tok then
+ else if Token.is_kind Token.Command tok then
"\\isacommand{" ^ output_syms s ^ "}"
- else if T.is_kind T.Keyword tok andalso Syntax.is_ascii_identifier s then
+ else if Token.is_kind Token.Keyword tok andalso Syntax.is_ascii_identifier s then
"\\isakeyword{" ^ output_syms s ^ "}"
- else if T.is_kind T.String tok then
+ else if Token.is_kind Token.String tok then
enclose "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" (output_syms s)
- else if T.is_kind T.AltString tok then
+ else if Token.is_kind Token.AltString tok then
enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
- else if T.is_kind T.Verbatim tok then
+ else if Token.is_kind Token.Verbatim tok then
let
- val (txt, pos) = T.source_position_of tok;
+ val (txt, pos) = Token.source_position_of tok;
val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
val out = implode (map output_syms_antiq ants);
in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
--- a/src/Pure/Thy/thy_header.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Thy/thy_header.ML Tue May 18 06:28:42 2010 -0700
@@ -6,17 +6,13 @@
signature THY_HEADER =
sig
- val args: OuterLex.token list ->
- (string * string list * (string * bool) list) * OuterLex.token list
+ val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
val read: Position.T -> (string, 'a) Source.source -> string * string list * (string * bool) list
end;
structure Thy_Header: THY_HEADER =
struct
-structure T = OuterLex;
-
-
(* keywords *)
val headerN = "header";
@@ -58,9 +54,9 @@
let val res =
src
|> Symbol.source {do_recover = false}
- |> T.source {do_recover = NONE} (fn () => (header_lexicon, Scan.empty_lexicon)) pos
- |> T.source_proper
- |> Source.source T.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
+ |> Token.source {do_recover = NONE} (fn () => (header_lexicon, Scan.empty_lexicon)) pos
+ |> Token.source_proper
+ |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
|> Source.get_single;
in
(case res of SOME (x, _) => x
--- a/src/Pure/Thy/thy_header.scala Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Thy/thy_header.scala Tue May 18 06:28:42 2010 -0700
@@ -59,14 +59,14 @@
def read(file: File): Header =
{
val token = lexicon.token(symbols, _ => false)
- val toks = new mutable.ListBuffer[Outer_Lex.Token]
+ val toks = new mutable.ListBuffer[Token]
def scan_to_begin(in: Reader[Char])
{
token(in) match {
case lexicon.Success(tok, rest) =>
toks += tok
- if (!(tok.kind == Outer_Lex.Token_Kind.KEYWORD && tok.content == BEGIN))
+ if (!(tok.kind == Token.Kind.KEYWORD && tok.content == BEGIN))
scan_to_begin(rest)
case _ =>
}
@@ -74,7 +74,7 @@
val reader = Scan.byte_reader(file)
try { scan_to_begin(reader) } finally { reader.close }
- parse(commit(header), Outer_Lex.reader(toks.toList)) match {
+ parse(commit(header), Token.reader(toks.toList)) match {
case Success(result, _) => result
case bad => error(bad.toString)
}
--- a/src/Pure/Thy/thy_output.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Thy/thy_output.ML Tue May 18 06:28:42 2010 -0700
@@ -24,7 +24,7 @@
val modes: string list Unsynchronized.ref
val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
- (Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
+ (Toplevel.transition * Toplevel.state) list -> (Token.T, 'a) Source.source -> Buffer.T
val pretty_text: string -> Pretty.T
val pretty_term: Proof.context -> term -> Pretty.T
val pretty_thm: Proof.context -> thm -> Pretty.T
@@ -36,9 +36,6 @@
structure ThyOutput: THY_OUTPUT =
struct
-structure T = OuterLex;
-
-
(** global options **)
val display = Unsynchronized.ref false;
@@ -154,7 +151,7 @@
let
fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
| expand (Antiquote.Antiq (ss, (pos, _))) =
- let val (opts, src) = T.read_antiq lex antiq (ss, pos) in
+ let val (opts, src) = Token.read_antiq lex antiq (ss, pos) in
options opts (fn () => command src state) (); (*preview errors!*)
PrintMode.with_modes (! modes @ Latex.modes)
(Output.no_warnings_CRITICAL (options opts (fn () => command src state))) ()
@@ -178,7 +175,7 @@
datatype token =
NoToken
- | BasicToken of T.token
+ | BasicToken of Token.T
| MarkupToken of string * (string * Position.T)
| MarkupEnvToken of string * (string * Position.T)
| VerbatimToken of string * Position.T;
@@ -195,10 +192,10 @@
fun basic_token pred (BasicToken tok) = pred tok
| basic_token _ _ = false;
-val improper_token = basic_token (not o T.is_proper);
-val comment_token = basic_token T.is_comment;
-val blank_token = basic_token T.is_blank;
-val newline_token = basic_token T.is_newline;
+val improper_token = basic_token (not o Token.is_proper);
+val comment_token = basic_token Token.is_comment;
+val blank_token = basic_token Token.is_blank;
+val newline_token = basic_token Token.is_newline;
(* command spans *)
@@ -303,19 +300,19 @@
local
val space_proper =
- Scan.one T.is_blank -- Scan.many T.is_comment -- Scan.one T.is_proper;
+ Scan.one Token.is_blank -- Scan.many Token.is_comment -- Scan.one Token.is_proper;
-val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore);
+val is_improper = not o (Token.is_proper orf Token.is_begin_ignore orf Token.is_end_ignore);
val improper = Scan.many is_improper;
val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper));
-val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one T.is_blank));
+val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one Token.is_blank));
-val opt_newline = Scan.option (Scan.one T.is_newline);
+val opt_newline = Scan.option (Scan.one Token.is_newline);
val ignore =
- Scan.depend (fn d => opt_newline |-- Scan.one T.is_begin_ignore
+ Scan.depend (fn d => opt_newline |-- Scan.one Token.is_begin_ignore
>> pair (d + 1)) ||
- Scan.depend (fn d => Scan.one T.is_end_ignore --|
+ Scan.depend (fn d => Scan.one Token.is_end_ignore --|
(if d = 0 then Scan.fail_with (K "Bad nesting of meta-comments") else opt_newline)
>> pair (d - 1));
@@ -336,18 +333,19 @@
fun markup mark mk flag = Scan.peek (fn d =>
improper |--
- Parse.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.content_of)) --
+ Parse.position
+ (Scan.one (Token.is_kind Token.Command andf is_markup mark o Token.content_of)) --
Scan.repeat tag --
Parse.!!!! ((improper -- locale -- improper) |-- Parse.doc_source --| improper_end)
>> (fn (((tok, pos), tags), txt) =>
- let val name = T.content_of tok
+ let val name = Token.content_of tok
in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
val command = Scan.peek (fn d =>
- Parse.position (Scan.one (T.is_kind T.Command)) --
+ Parse.position (Scan.one (Token.is_kind Token.Command)) --
Scan.repeat tag
>> (fn ((tok, pos), tags) =>
- let val name = T.content_of tok
+ let val name = Token.content_of tok
in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
val cmt = Scan.peek (fn d =>
@@ -367,8 +365,8 @@
(* spans *)
- val is_eof = fn (_, (BasicToken x, _)) => T.is_eof x | _ => false;
- val stopper = Scan.stopper (K (NONE, (BasicToken T.eof, ("", 0)))) is_eof;
+ val is_eof = fn (_, (BasicToken x, _)) => Token.is_eof x | _ => false;
+ val stopper = Scan.stopper (K (NONE, (BasicToken Token.eof, ("", 0)))) is_eof;
val cmd = Scan.one (is_some o fst);
val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2;
@@ -390,8 +388,8 @@
val spans =
src
- |> Source.filter (not o T.is_semicolon)
- |> Source.source' 0 T.stopper (Scan.error (Scan.bulk token)) NONE
+ |> Source.filter (not o Token.is_semicolon)
+ |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk token)) NONE
|> Source.source stopper (Scan.error (Scan.bulk span)) NONE
|> Source.exhaust;
@@ -490,7 +488,7 @@
(* default output *)
-val str_of_source = space_implode " " o map T.unparse o #2 o #1 o Args.dest_src;
+val str_of_source = space_implode " " o map Token.unparse o #2 o #1 o Args.dest_src;
fun maybe_pretty_source pretty src xs =
map pretty xs (*always pretty in order to exhibit errors!*)
--- a/src/Pure/Thy/thy_syntax.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Thy/thy_syntax.ML Tue May 18 06:28:42 2010 -0700
@@ -7,18 +7,17 @@
signature THY_SYNTAX =
sig
val token_source: Scan.lexicon * Scan.lexicon -> Position.T -> (string, 'a) Source.source ->
- (OuterLex.token, (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, 'a)
+ (Token.T, (Symbol_Pos.T, Position.T * (Symbol.symbol, (string, 'a)
Source.source) Source.source) Source.source) Source.source
- val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> OuterLex.token list
- val present_token: OuterLex.token -> output
- val report_token: OuterLex.token -> unit
+ val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
+ val present_token: Token.T -> output
+ val report_token: Token.T -> unit
datatype span_kind = Command of string | Ignored | Malformed
type span
val span_kind: span -> span_kind
- val span_content: span -> OuterLex.token list
+ val span_content: span -> Token.T list
val span_range: span -> Position.range
- val span_source: (OuterLex.token, 'a) Source.source ->
- (span, (OuterLex.token, 'a) Source.source) Source.source
+ val span_source: (Token.T, 'a) Source.source -> (span, (Token.T, 'a) Source.source) Source.source
val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
val present_span: span -> output
val report_span: span -> unit
@@ -29,16 +28,13 @@
structure ThySyntax: THY_SYNTAX =
struct
-structure T = OuterLex;
-
-
(** tokens **)
(* parse *)
fun token_source lexs pos src =
Symbol.source {do_recover = true} src
- |> T.source {do_recover = SOME false} (K lexs) pos;
+ |> Token.source {do_recover = SOME false} (K lexs) pos;
fun parse_tokens lexs pos str =
Source.of_string str
@@ -51,33 +47,33 @@
local
val token_kind_markup =
- fn T.Command => (Markup.commandN, [])
- | T.Keyword => (Markup.keywordN, [])
- | T.Ident => Markup.ident
- | T.LongIdent => Markup.ident
- | T.SymIdent => Markup.ident
- | T.Var => Markup.var
- | T.TypeIdent => Markup.tfree
- | T.TypeVar => Markup.tvar
- | T.Nat => Markup.ident
- | T.String => Markup.string
- | T.AltString => Markup.altstring
- | T.Verbatim => Markup.verbatim
- | T.Space => Markup.none
- | T.Comment => Markup.comment
- | T.InternalValue => Markup.none
- | T.Malformed => Markup.malformed
- | T.Error _ => Markup.malformed
- | T.Sync => Markup.control
- | T.EOF => Markup.control;
+ fn Token.Command => (Markup.commandN, [])
+ | Token.Keyword => (Markup.keywordN, [])
+ | Token.Ident => Markup.ident
+ | Token.LongIdent => Markup.ident
+ | Token.SymIdent => Markup.ident
+ | Token.Var => Markup.var
+ | Token.TypeIdent => Markup.tfree
+ | Token.TypeVar => Markup.tvar
+ | Token.Nat => Markup.ident
+ | Token.String => Markup.string
+ | Token.AltString => Markup.altstring
+ | Token.Verbatim => Markup.verbatim
+ | Token.Space => Markup.none
+ | Token.Comment => Markup.comment
+ | Token.InternalValue => Markup.none
+ | Token.Malformed => Markup.malformed
+ | Token.Error _ => Markup.malformed
+ | Token.Sync => Markup.control
+ | Token.EOF => Markup.control;
in
fun present_token tok =
- Markup.enclose (token_kind_markup (T.kind_of tok)) (Output.output (T.unparse tok));
+ Markup.enclose (token_kind_markup (Token.kind_of tok)) (Output.output (Token.unparse tok));
fun report_token tok =
- Position.report (token_kind_markup (T.kind_of tok)) (T.position_of tok);
+ Position.report (token_kind_markup (Token.kind_of tok)) (Token.position_of tok);
end;
@@ -88,7 +84,7 @@
(* type span *)
datatype span_kind = Command of string | Ignored | Malformed;
-datatype span = Span of span_kind * OuterLex.token list;
+datatype span = Span of span_kind * Token.T list;
fun span_kind (Span (k, _)) = k;
fun span_content (Span (_, toks)) = toks;
@@ -98,8 +94,8 @@
[] => (Position.none, Position.none)
| toks =>
let
- val start_pos = T.position_of (hd toks);
- val end_pos = T.end_position_of (List.last toks);
+ val start_pos = Token.position_of (hd toks);
+ val end_pos = Token.end_position_of (List.last toks);
in (start_pos, end_pos) end);
@@ -107,7 +103,7 @@
local
-val is_whitespace = T.is_kind T.Space orf T.is_kind T.Comment;
+val is_whitespace = Token.is_kind Token.Space orf Token.is_kind Token.Comment;
val body =
Scan.unless (Scan.many is_whitespace -- Scan.ahead (Parse.command || Parse.eof)) Parse.not_eof;
@@ -120,7 +116,7 @@
in
-fun span_source src = Source.source T.stopper (Scan.bulk span) NONE src;
+fun span_source src = Source.source Token.stopper (Scan.bulk span) NONE src;
end;
--- a/src/Pure/Thy/thy_syntax.scala Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/Thy/thy_syntax.scala Tue May 18 06:28:42 2010 -0700
@@ -22,13 +22,13 @@
}
}
- type Span = List[Outer_Lex.Token]
+ type Span = List[Token]
- def parse_spans(toks: List[Outer_Lex.Token]): List[Span] =
+ def parse_spans(toks: List[Token]): List[Span] =
{
import parser._
- parse(rep(command_span), Outer_Lex.reader(toks)) match {
+ parse(rep(command_span), Token.reader(toks)) match {
case Success(spans, rest) if rest.atEnd => spans
case bad => error(bad.toString)
}
--- a/src/Pure/build-jars Mon May 17 18:59:59 2010 -0700
+++ b/src/Pure/build-jars Tue May 18 06:28:42 2010 -0700
@@ -34,9 +34,9 @@
General/yxml.scala
Isar/isar_document.scala
Isar/keyword.scala
- Isar/outer_lex.scala
Isar/outer_syntax.scala
Isar/parse.scala
+ Isar/token.scala
PIDE/change.scala
PIDE/command.scala
PIDE/document.scala
--- a/src/Tools/Code/code_eval.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/Code/code_eval.ML Tue May 18 06:28:42 2010 -0700
@@ -204,26 +204,24 @@
local
-structure P = OuterParse
-and K = OuterKeyword
-
val datatypesK = "datatypes";
val functionsK = "functions";
val fileK = "file";
val andK = "and"
-val _ = List.app K.keyword [datatypesK, functionsK];
+val _ = List.app Keyword.keyword [datatypesK, functionsK];
-val parse_datatype = (P.name --| P.$$$ "=" -- (P.term ::: (Scan.repeat (P.$$$ "|" |-- P.term))));
+val parse_datatype =
+ Parse.name --| Parse.$$$ "=" -- (Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term)));
in
val _ =
- OuterSyntax.command "code_reflect" "enrich runtime environment with generated code"
- K.thy_decl (P.name -- Scan.optional (P.$$$ datatypesK |-- (parse_datatype
- ::: Scan.repeat (P.$$$ andK |-- parse_datatype))) []
- -- Scan.optional (P.$$$ functionsK |-- Scan.repeat1 P.name) []
- -- Scan.option (P.$$$ fileK |-- P.name)
+ Outer_Syntax.command "code_reflect" "enrich runtime environment with generated code"
+ Keyword.thy_decl (Parse.name -- Scan.optional (Parse.$$$ datatypesK |-- (parse_datatype
+ ::: Scan.repeat (Parse.$$$ andK |-- parse_datatype))) []
+ -- Scan.optional (Parse.$$$ functionsK |-- Scan.repeat1 Parse.name) []
+ -- Scan.option (Parse.$$$ fileK |-- Parse.name)
>> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
(code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
--- a/src/Tools/Code/code_haskell.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/Code/code_haskell.ML Tue May 18 06:28:42 2010 -0700
@@ -469,8 +469,8 @@
serialize_haskell module_prefix module_name string_classes));
val _ =
- OuterSyntax.command "code_monad" "define code syntax for monads" OuterKeyword.thy_decl (
- OuterParse.term_group -- OuterParse.name >> (fn (raw_bind, target) =>
+ Outer_Syntax.command "code_monad" "define code syntax for monads" Keyword.thy_decl (
+ Parse.term_group -- Parse.name >> (fn (raw_bind, target) =>
Toplevel.theory (add_monad target raw_bind))
);
--- a/src/Tools/Code/code_preproc.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/Code/code_preproc.ML Tue May 18 06:28:42 2010 -0700
@@ -479,8 +479,8 @@
end;
val _ =
- OuterSyntax.improper_command "print_codeproc" "print code preprocessor setup"
- OuterKeyword.diag (Scan.succeed
+ Outer_Syntax.improper_command "print_codeproc" "print code preprocessor setup"
+ Keyword.diag (Scan.succeed
(Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
(print_codeproc o Toplevel.theory_of)));
--- a/src/Tools/Code/code_printer.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/Code/code_printer.ML Tue May 18 06:28:42 2010 -0700
@@ -72,9 +72,9 @@
val parse_infix: ('a -> 'b) -> lrx * int -> string
-> int * ((fixity -> 'b -> Pretty.T)
-> fixity -> 'a list -> Pretty.T)
- val parse_syntax: ('a -> 'b) -> OuterParse.token list
+ val parse_syntax: ('a -> 'b) -> Token.T list
-> (int * ((fixity -> 'b -> Pretty.T)
- -> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list
+ -> fixity -> 'a list -> Pretty.T)) option * Token.T list
val simple_const_syntax: simple_const_syntax -> proto_const_syntax
val activate_const_syntax: theory -> literals
-> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming
@@ -329,15 +329,15 @@
fun parse_syntax prep_arg xs =
Scan.option ((
- ((OuterParse.$$$ infixK >> K X)
- || (OuterParse.$$$ infixlK >> K L)
- || (OuterParse.$$$ infixrK >> K R))
- -- OuterParse.nat >> parse_infix prep_arg
+ ((Parse.$$$ infixK >> K X)
+ || (Parse.$$$ infixlK >> K L)
+ || (Parse.$$$ infixrK >> K R))
+ -- Parse.nat >> parse_infix prep_arg
|| Scan.succeed (parse_mixfix prep_arg))
- -- OuterParse.string
+ -- Parse.string
>> (fn (parse, s) => parse s)) xs;
-val _ = List.app OuterKeyword.keyword [infixK, infixlK, infixrK];
+val _ = List.app Keyword.keyword [infixK, infixlK, infixrK];
(** module name spaces **)
--- a/src/Tools/Code/code_target.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/Code/code_target.ML Tue May 18 06:28:42 2010 -0700
@@ -19,14 +19,13 @@
type destination
type serialization
- val parse_args: (OuterLex.token list -> 'a * OuterLex.token list)
- -> OuterLex.token list -> 'a
+ val parse_args: 'a parser -> Token.T list -> 'a
val stmt_names_of_destination: destination -> string list
val mk_serialization: string -> ('a -> unit) option
-> (Path.T option -> 'a -> unit)
-> ('a -> string * string option list)
-> 'a -> serialization
- val serialize: theory -> string -> int option -> string option -> OuterLex.token list
+ val serialize: theory -> string -> int option -> string option -> Token.T list
-> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
val serialize_custom: theory -> string * (serializer * literals)
-> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
@@ -105,7 +104,7 @@
type serializer =
string option (*module name*)
- -> OuterLex.token list (*arguments*)
+ -> Token.T list (*arguments*)
-> (string -> string) (*labelled_name*)
-> string list (*reserved symbols*)
-> (string * Pretty.T) list (*includes*)
@@ -464,9 +463,6 @@
local
-structure P = OuterParse
-and K = OuterKeyword
-
fun zip_list (x::xs) f g =
f
#-> (fn y =>
@@ -474,9 +470,9 @@
#-> (fn xys => pair ((x, y) :: xys)));
fun parse_multi_syntax parse_thing parse_syntax =
- P.and_list1 parse_thing
- #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
- (zip_list things parse_syntax (P.$$$ "and")) --| P.$$$ ")"));
+ Parse.and_list1 parse_thing
+ #-> (fn things => Scan.repeat1 (Parse.$$$ "(" |-- Parse.name --
+ (zip_list things parse_syntax (Parse.$$$ "and")) --| Parse.$$$ ")"));
in
@@ -498,7 +494,7 @@
val allow_abort_cmd = gen_allow_abort Code.read_const;
fun parse_args f args =
- case Scan.read OuterLex.stopper f args
+ case Scan.read Token.stopper f args
of SOME x => x
| NONE => error "Bad serializer arguments";
@@ -508,75 +504,79 @@
val (inK, module_nameK, fileK) = ("in", "module_name", "file");
val code_exprP =
- (Scan.repeat1 P.term_group
- -- Scan.repeat (P.$$$ inK |-- P.name
- -- Scan.option (P.$$$ module_nameK |-- P.name)
- -- Scan.option (P.$$$ fileK |-- P.name)
- -- Scan.optional (P.$$$ "(" |-- Args.parse --| P.$$$ ")") []
+ (Scan.repeat1 Parse.term_group
+ -- Scan.repeat (Parse.$$$ inK |-- Parse.name
+ -- Scan.option (Parse.$$$ module_nameK |-- Parse.name)
+ -- Scan.option (Parse.$$$ fileK |-- Parse.name)
+ -- Scan.optional (Parse.$$$ "(" |-- Args.parse --| Parse.$$$ ")") []
) >> (fn (raw_cs, seris) => export_code_cmd raw_cs seris));
-val _ = List.app OuterKeyword.keyword [inK, module_nameK, fileK];
+val _ = List.app Keyword.keyword [inK, module_nameK, fileK];
val _ =
- OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl (
- parse_multi_syntax P.xname (Scan.option P.string)
+ Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (
+ parse_multi_syntax Parse.xname (Scan.option Parse.string)
>> (Toplevel.theory oo fold) (fn (target, syns) =>
fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
);
val _ =
- OuterSyntax.command "code_instance" "define code syntax for instance" K.thy_decl (
- parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname) (Scan.option (P.minus >> K ()))
+ Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl (
+ parse_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
+ (Scan.option (Parse.minus >> K ()))
>> (Toplevel.theory oo fold) (fn (target, syns) =>
fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
);
val _ =
- OuterSyntax.command "code_type" "define code syntax for type constructor" K.thy_decl (
- parse_multi_syntax P.xname (Code_Printer.parse_syntax I)
+ Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl (
+ parse_multi_syntax Parse.xname (Code_Printer.parse_syntax I)
>> (Toplevel.theory oo fold) (fn (target, syns) =>
fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
);
val _ =
- OuterSyntax.command "code_const" "define code syntax for constant" K.thy_decl (
- parse_multi_syntax P.term_group (Code_Printer.parse_syntax fst)
+ Outer_Syntax.command "code_const" "define code syntax for constant" Keyword.thy_decl (
+ parse_multi_syntax Parse.term_group (Code_Printer.parse_syntax fst)
>> (Toplevel.theory oo fold) (fn (target, syns) =>
fold (fn (raw_const, syn) => add_syntax_const_simple_cmd target raw_const syn) syns)
);
val _ =
- OuterSyntax.command "code_reserved" "declare words as reserved for target language" K.thy_decl (
- P.name -- Scan.repeat1 P.name
+ Outer_Syntax.command "code_reserved" "declare words as reserved for target language"
+ Keyword.thy_decl (
+ Parse.name -- Scan.repeat1 Parse.name
>> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)
);
val _ =
- OuterSyntax.command "code_include" "declare piece of code to be included in generated code" K.thy_decl (
- P.name -- P.name -- (P.text :|-- (fn "-" => Scan.succeed NONE
- | s => Scan.optional (P.$$$ "attach" |-- Scan.repeat1 P.term) [] >> pair s >> SOME))
+ Outer_Syntax.command "code_include" "declare piece of code to be included in generated code"
+ Keyword.thy_decl (
+ Parse.name -- Parse.name -- (Parse.text :|-- (fn "-" => Scan.succeed NONE
+ | s => Scan.optional (Parse.$$$ "attach" |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME))
>> (fn ((target, name), content_consts) =>
(Toplevel.theory o add_include_cmd target) (name, content_consts))
);
val _ =
- OuterSyntax.command "code_modulename" "alias module to other name" K.thy_decl (
- P.name -- Scan.repeat1 (P.name -- P.name)
+ Outer_Syntax.command "code_modulename" "alias module to other name" Keyword.thy_decl (
+ Parse.name -- Scan.repeat1 (Parse.name -- Parse.name)
>> (fn (target, modlnames) => (Toplevel.theory o fold (add_module_alias target)) modlnames)
);
val _ =
- OuterSyntax.command "code_abort" "permit constant to be implemented as program abort" K.thy_decl (
- Scan.repeat1 P.term_group >> (Toplevel.theory o fold allow_abort_cmd)
+ Outer_Syntax.command "code_abort" "permit constant to be implemented as program abort"
+ Keyword.thy_decl (
+ Scan.repeat1 Parse.term_group >> (Toplevel.theory o fold allow_abort_cmd)
);
val _ =
- OuterSyntax.command "export_code" "generate executable code for constants"
- K.diag (P.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
+ Outer_Syntax.command "export_code" "generate executable code for constants"
+ Keyword.diag (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
fun shell_command thyname cmd = Toplevel.program (fn _ =>
- (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! code_exprP)
- ((filter OuterLex.is_proper o OuterSyntax.scan Position.none) cmd)
+ (use_thy thyname; case Scan.read Token.stopper (Parse.!!! code_exprP)
+ ((filter Token.is_proper o Outer_Syntax.scan Position.none) cmd)
of SOME f => (writeln "Now generating code..."; f (theory thyname))
| NONE => error ("Bad directive " ^ quote cmd)))
handle Runtime.TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
--- a/src/Tools/Code/code_thingol.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/Code/code_thingol.ML Tue May 18 06:28:42 2010 -0700
@@ -915,23 +915,21 @@
local
-structure P = OuterParse
-and K = OuterKeyword
-
fun code_thms_cmd thy = code_thms thy o op @ o read_const_exprs thy;
fun code_deps_cmd thy = code_deps thy o op @ o read_const_exprs thy;
in
val _ =
- OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag
- (Scan.repeat1 P.term_group
+ Outer_Syntax.improper_command "code_thms" "print system of code equations for code" Keyword.diag
+ (Scan.repeat1 Parse.term_group
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
val _ =
- OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag
- (Scan.repeat1 P.term_group
+ Outer_Syntax.improper_command "code_deps" "visualize dependencies of code equations for code"
+ Keyword.diag
+ (Scan.repeat1 Parse.term_group
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
--- a/src/Tools/WWW_Find/find_theorems.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/WWW_Find/find_theorems.ML Tue May 18 06:28:42 2010 -0700
@@ -158,21 +158,17 @@
end;
-structure P = OuterParse
- and K = OuterKeyword
- and FT = Find_Theorems;
-
val criterion =
- P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Find_Theorems.Name ||
- P.reserved "intro" >> K Find_Theorems.Intro ||
- P.reserved "elim" >> K Find_Theorems.Elim ||
- P.reserved "dest" >> K Find_Theorems.Dest ||
- P.reserved "solves" >> K Find_Theorems.Solves ||
- P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> Find_Theorems.Simp ||
- P.term >> Find_Theorems.Pattern;
+ Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Find_Theorems.Name ||
+ Parse.reserved "intro" >> K Find_Theorems.Intro ||
+ Parse.reserved "elim" >> K Find_Theorems.Elim ||
+ Parse.reserved "dest" >> K Find_Theorems.Dest ||
+ Parse.reserved "solves" >> K Find_Theorems.Solves ||
+ Parse.reserved "simp" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.term) >> Find_Theorems.Simp ||
+ Parse.term >> Find_Theorems.Pattern;
val parse_query =
- Scan.repeat (((Scan.option P.minus >> is_none) -- criterion));
+ Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
fun app_index f xs = fold_index (fn x => K (f x)) xs ();
@@ -194,8 +190,8 @@
fun get_query () =
query
|> (fn s => s ^ ";")
- |> OuterSyntax.scan Position.start
- |> filter OuterLex.is_proper
+ |> Outer_Syntax.scan Position.start
+ |> filter Token.is_proper
|> Scan.error parse_query
|> fst;
--- a/src/Tools/WWW_Find/unicode_symbols.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/WWW_Find/unicode_symbols.ML Tue May 18 06:28:42 2010 -0700
@@ -114,8 +114,6 @@
local (* Parser *)
-structure P = OuterParse;
-
fun $$$ kw = Scan.one (is_keyword kw) >> str_of_token;
val hex_code = Scan.one is_hex_code >> int_of_code;
val ascii_sym = Scan.one is_ascii_sym >> str_of_token;
@@ -129,7 +127,7 @@
in
-val line = (symbol -- unicode --| font -- abbr) >> P.triple1;
+val line = (symbol -- unicode --| font -- abbr) >> Parse.triple1;
val symbols_path =
[getenv "ISABELLE_HOME", "etc", "symbols"]
--- a/src/Tools/eqsubst.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/eqsubst.ML Tue May 18 06:28:42 2010 -0700
@@ -556,7 +556,7 @@
(Scan.succeed false);
val ith_syntax =
- Scan.optional (Args.parens (Scan.repeat OuterParse.nat)) [0];
+ Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0];
(* combination method that takes a flag (true indicates that subst
should be done to an assumption, false = apply to the conclusion of
--- a/src/Tools/induct.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/induct.ML Tue May 18 06:28:42 2010 -0700
@@ -254,8 +254,8 @@
end;
val _ =
- OuterSyntax.improper_command "print_induct_rules" "print induction and cases rules"
- OuterKeyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+ Outer_Syntax.improper_command "print_induct_rules" "print induction and cases rules"
+ Keyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
Toplevel.keep (print_rules o Toplevel.context_of)));
@@ -845,8 +845,6 @@
(** concrete syntax **)
-structure P = OuterParse;
-
val arbitraryN = "arbitrary";
val takingN = "taking";
val ruleN = "rule";
@@ -892,7 +890,7 @@
Args.$$$ predN || Args.$$$ setN || Args.$$$ ruleN) -- Args.colon)) scan;
val arbitrary = Scan.optional (Scan.lift (Args.$$$ arbitraryN -- Args.colon) |--
- P.and_list1' (Scan.repeat (unless_more_args free))) [];
+ Parse.and_list1' (Scan.repeat (unless_more_args free))) [];
val taking = Scan.optional (Scan.lift (Args.$$$ takingN -- Args.colon) |--
Scan.repeat1 (unless_more_args inst)) [];
@@ -902,7 +900,7 @@
val cases_setup =
Method.setup @{binding cases}
(Args.mode no_simpN --
- (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
+ (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
(fn (no_simp, (insts, opt_rule)) => fn ctxt =>
METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
(cases_tac ctxt (not no_simp) insts opt_rule facts)))))
@@ -910,11 +908,12 @@
val induct_setup =
Method.setup @{binding induct}
- (Args.mode no_simpN -- (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
+ (Args.mode no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
(arbitrary -- taking -- Scan.option induct_rule)) >>
(fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt =>
RAW_METHOD_CASES (fn facts =>
- Seq.DETERM (HEADGOAL (induct_tac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
+ Seq.DETERM
+ (HEADGOAL (induct_tac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
"induction on types or predicates/sets";
val coinduct_setup =
--- a/src/Tools/induct_tacs.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/induct_tacs.ML Tue May 18 06:28:42 2010 -0700
@@ -116,8 +116,7 @@
val opt_rules = Scan.option (rule_spec |-- Attrib.thms);
val varss =
- OuterParse.and_list'
- (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source))));
+ Parse.and_list' (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source))));
in
--- a/src/Tools/intuitionistic.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/intuitionistic.ML Tue May 18 06:28:42 2010 -0700
@@ -71,7 +71,7 @@
val destN = "dest";
fun modifier name kind kind' att =
- Args.$$$ name |-- (kind >> K NONE || kind' |-- OuterParse.nat --| Args.colon >> SOME)
+ Args.$$$ name |-- (kind >> K NONE || kind' |-- Parse.nat --| Args.colon >> SOME)
>> (pair (I: Proof.context -> Proof.context) o att);
val modifiers =
@@ -87,7 +87,7 @@
fun method_setup name =
Method.setup name
- (Scan.lift (Scan.option OuterParse.nat) --| Method.sections modifiers >>
+ (Scan.lift (Scan.option Parse.nat) --| Method.sections modifiers >>
(fn opt_lim => fn ctxt =>
SIMPLE_METHOD' (Object_Logic.atomize_prems_tac THEN' prover_tac ctxt opt_lim)))
"intuitionistic proof search";
--- a/src/Tools/nbe.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/nbe.ML Tue May 18 06:28:42 2010 -0700
@@ -625,15 +625,12 @@
val setup = Value.add_evaluator ("nbe", norm o ProofContext.theory_of);
-local structure P = OuterParse and K = OuterKeyword in
-
-val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
+val opt_modes =
+ Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
val _ =
- OuterSyntax.improper_command "normal_form" "normalize term by evaluation" K.diag
- (opt_modes -- P.term >> (Toplevel.keep o norm_print_term_cmd));
-
-end;
+ Outer_Syntax.improper_command "normal_form" "normalize term by evaluation" Keyword.diag
+ (opt_modes -- Parse.term >> (Toplevel.keep o norm_print_term_cmd));
end;
\ No newline at end of file
--- a/src/Tools/quickcheck.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/quickcheck.ML Tue May 18 06:28:42 2010 -0700
@@ -315,27 +315,25 @@
test_goal quiet report generator_name size iterations default_type no_assms insts i assms state
end;
-fun quickcheck args i state = fst (gen_quickcheck args i state)
+fun quickcheck args i state = fst (gen_quickcheck args i state);
fun quickcheck_cmd args i state =
gen_quickcheck args i (Toplevel.proof_of state)
|> Pretty.writeln o pretty_counterex_and_reports (Toplevel.context_of state);
-local structure P = OuterParse and K = OuterKeyword in
+val parse_arg = Parse.name -- (Scan.optional (Parse.$$$ "=" |-- Parse.name) "true");
-val parse_arg = P.name -- (Scan.optional (P.$$$ "=" |-- P.name) "true")
-
-val parse_args = P.$$$ "[" |-- P.list1 parse_arg --| P.$$$ "]"
+val parse_args = Parse.$$$ "[" |-- Parse.list1 parse_arg --| Parse.$$$ "]"
|| Scan.succeed [];
-val _ = OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl
- (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
+val _ =
+ Outer_Syntax.command "quickcheck_params" "set parameters for random testing" Keyword.thy_decl
+ (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
-val _ = OuterSyntax.improper_command "quickcheck" "try to find counterexample for subgoal" K.diag
- (parse_args -- Scan.optional P.nat 1
- >> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i)));
-
-end; (*local*)
+val _ =
+ Outer_Syntax.improper_command "quickcheck" "try to find counterexample for subgoal" Keyword.diag
+ (parse_args -- Scan.optional Parse.nat 1
+ >> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i)));
end;
--- a/src/Tools/value.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/Tools/value.ML Tue May 18 06:28:42 2010 -0700
@@ -52,15 +52,13 @@
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
in Pretty.writeln p end;
-local structure P = OuterParse and K = OuterKeyword in
-
-val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
+val opt_modes =
+ Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
-val _ = OuterSyntax.improper_command "value" "evaluate and print term" K.diag
- (Scan.option (P.$$$ "[" |-- P.xname --| P.$$$ "]") -- opt_modes -- P.term
- >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
- (value_cmd some_name modes t)));
-
-end; (*local*)
+val _ =
+ Outer_Syntax.improper_command "value" "evaluate and print term" Keyword.diag
+ (Scan.option (Parse.$$$ "[" |-- Parse.xname --| Parse.$$$ "]") -- opt_modes -- Parse.term
+ >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
+ (value_cmd some_name modes t)));
end;
--- a/src/ZF/Tools/datatype_package.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/ZF/Tools/datatype_package.ML Tue May 18 06:28:42 2010 -0700
@@ -419,29 +419,26 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
fun mk_datatype ((((dom, dts), monos), type_intrs), type_elims) =
#1 o add_datatype (dom, map fst dts) (map snd dts) (monos, type_intrs, type_elims);
val con_decl =
- P.name -- Scan.optional (P.$$$ "(" |-- P.list1 P.term --| P.$$$ ")") [] -- P.opt_mixfix
- >> P.triple1;
+ Parse.name -- Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.term --| Parse.$$$ ")") [] --
+ Parse.opt_mixfix >> Parse.triple1;
val datatype_decl =
- (Scan.optional ((P.$$$ "\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term) "") --
- P.and_list1 (P.term -- (P.$$$ "=" |-- P.enum1 "|" con_decl)) --
- Scan.optional (P.$$$ "monos" |-- P.!!! Parse_Spec.xthms1) [] --
- Scan.optional (P.$$$ "type_intros" |-- P.!!! Parse_Spec.xthms1) [] --
- Scan.optional (P.$$$ "type_elims" |-- P.!!! Parse_Spec.xthms1) []
+ (Scan.optional ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<=") |-- Parse.!!! Parse.term) "") --
+ Parse.and_list1 (Parse.term -- (Parse.$$$ "=" |-- Parse.enum1 "|" con_decl)) --
+ Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) [] --
+ Scan.optional (Parse.$$$ "type_intros" |-- Parse.!!! Parse_Spec.xthms1) [] --
+ Scan.optional (Parse.$$$ "type_elims" |-- Parse.!!! Parse_Spec.xthms1) []
>> (Toplevel.theory o mk_datatype);
val coind_prefix = if coind then "co" else "";
-val _ = OuterSyntax.command (coind_prefix ^ "datatype")
- ("define " ^ coind_prefix ^ "datatype") K.thy_decl datatype_decl;
+val _ =
+ Outer_Syntax.command (coind_prefix ^ "datatype")
+ ("define " ^ coind_prefix ^ "datatype") Keyword.thy_decl datatype_decl;
end;
-end;
-
--- a/src/ZF/Tools/ind_cases.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/ZF/Tools/ind_cases.ML Tue May 18 06:28:42 2010 -0700
@@ -64,15 +64,11 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
val _ =
- OuterSyntax.command "inductive_cases"
- "create simplified instances of elimination rules (improper)" K.thy_script
- (P.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 P.prop)
+ Outer_Syntax.command "inductive_cases"
+ "create simplified instances of elimination rules (improper)" Keyword.thy_script
+ (Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 Parse.prop)
>> (Toplevel.theory o inductive_cases));
end;
-end;
-
--- a/src/ZF/Tools/induct_tacs.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/ZF/Tools/induct_tacs.ML Tue May 18 06:28:42 2010 -0700
@@ -186,25 +186,20 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = List.app OuterKeyword.keyword ["elimination", "induction", "case_eqns", "recursor_eqns"];
+val _ = List.app Keyword.keyword ["elimination", "induction", "case_eqns", "recursor_eqns"];
val rep_datatype_decl =
- (P.$$$ "elimination" |-- P.!!! Parse_Spec.xthm) --
- (P.$$$ "induction" |-- P.!!! Parse_Spec.xthm) --
- (P.$$$ "case_eqns" |-- P.!!! Parse_Spec.xthms1) --
- Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! Parse_Spec.xthms1) []
+ (Parse.$$$ "elimination" |-- Parse.!!! Parse_Spec.xthm) --
+ (Parse.$$$ "induction" |-- Parse.!!! Parse_Spec.xthm) --
+ (Parse.$$$ "case_eqns" |-- Parse.!!! Parse_Spec.xthms1) --
+ Scan.optional (Parse.$$$ "recursor_eqns" |-- Parse.!!! Parse_Spec.xthms1) []
>> (fn (((x, y), z), w) => rep_datatype x y z w);
val _ =
- OuterSyntax.command "rep_datatype" "represent existing set inductively" K.thy_decl
+ Outer_Syntax.command "rep_datatype" "represent existing set inductively" Keyword.thy_decl
(rep_datatype_decl >> Toplevel.theory);
end;
-end;
-
-
val exhaust_tac = DatatypeTactics.exhaust_tac;
val induct_tac = DatatypeTactics.induct_tac;
--- a/src/ZF/Tools/inductive_package.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/ZF/Tools/inductive_package.ML Tue May 18 06:28:42 2010 -0700
@@ -576,29 +576,26 @@
(* outer syntax *)
-local structure P = OuterParse and K = OuterKeyword in
-
-val _ = List.app OuterKeyword.keyword
+val _ = List.app Keyword.keyword
["domains", "intros", "monos", "con_defs", "type_intros", "type_elims"];
fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) =
- #1 o add_inductive doms (map P.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
+ #1 o add_inductive doms (map Parse.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
val ind_decl =
- (P.$$$ "domains" |-- P.!!! (P.enum1 "+" P.term --
- ((P.$$$ "\<subseteq>" || P.$$$ "<=") |-- P.term))) --
- (P.$$$ "intros" |--
- P.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- P.prop))) --
- Scan.optional (P.$$$ "monos" |-- P.!!! Parse_Spec.xthms1) [] --
- Scan.optional (P.$$$ "con_defs" |-- P.!!! Parse_Spec.xthms1) [] --
- Scan.optional (P.$$$ "type_intros" |-- P.!!! Parse_Spec.xthms1) [] --
- Scan.optional (P.$$$ "type_elims" |-- P.!!! Parse_Spec.xthms1) []
+ (Parse.$$$ "domains" |-- Parse.!!! (Parse.enum1 "+" Parse.term --
+ ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<=") |-- Parse.term))) --
+ (Parse.$$$ "intros" |--
+ Parse.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop))) --
+ Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) [] --
+ Scan.optional (Parse.$$$ "con_defs" |-- Parse.!!! Parse_Spec.xthms1) [] --
+ Scan.optional (Parse.$$$ "type_intros" |-- Parse.!!! Parse_Spec.xthms1) [] --
+ Scan.optional (Parse.$$$ "type_elims" |-- Parse.!!! Parse_Spec.xthms1) []
>> (Toplevel.theory o mk_ind);
-val _ = OuterSyntax.command (co_prefix ^ "inductive")
- ("define " ^ co_prefix ^ "inductive sets") K.thy_decl ind_decl;
+val _ =
+ Outer_Syntax.command (co_prefix ^ "inductive")
+ ("define " ^ co_prefix ^ "inductive sets") Keyword.thy_decl ind_decl;
end;
-end;
-
--- a/src/ZF/Tools/primrec_package.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/ZF/Tools/primrec_package.ML Tue May 18 06:28:42 2010 -0700
@@ -194,12 +194,11 @@
(* outer syntax *)
-structure P = OuterParse and K = OuterKeyword;
-
val _ =
- OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
- (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- P.prop)
- >> (Toplevel.theory o (#1 oo (add_primrec o map P.triple_swap))));
+ Outer_Syntax.command "primrec" "define primitive recursive functions on datatypes"
+ Keyword.thy_decl
+ (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
+ >> (Toplevel.theory o (#1 oo (add_primrec o map Parse.triple_swap))));
end;
--- a/src/ZF/Tools/typechk.ML Mon May 17 18:59:59 2010 -0700
+++ b/src/ZF/Tools/typechk.ML Tue May 18 06:28:42 2010 -0700
@@ -118,7 +118,7 @@
"ZF type-checking";
val _ =
- OuterSyntax.improper_command "print_tcset" "print context of ZF typecheck" OuterKeyword.diag
+ Outer_Syntax.improper_command "print_tcset" "print context of ZF typecheck" Keyword.diag
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
Toplevel.keep (print_tcset o Toplevel.context_of)));