refer directly to structure Keyword and Parse;
eliminated old-style structure aliases K and P;
--- a/src/Pure/Isar/args.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/args.ML Sat May 15 23:16:32 2010 +0200
@@ -71,7 +71,6 @@
struct
structure T = OuterLex;
-structure P = OuterParse;
type token = T.token;
@@ -125,17 +124,17 @@
(* basic *)
-fun token atom = Scan.ahead P.not_eof --| atom;
+fun token atom = Scan.ahead Parse.not_eof --| atom;
val ident = token
- (P.short_ident || P.long_ident || P.sym_ident || P.term_var ||
- P.type_ident || P.type_var || P.number);
+ (Parse.short_ident || Parse.long_ident || Parse.sym_ident || Parse.term_var ||
+ Parse.type_ident || Parse.type_var || Parse.number);
-val string = token (P.string || P.verbatim);
-val alt_string = token P.alt_string;
-val symbolic = token P.keyword_ident_or_symbolic;
+val string = token (Parse.string || Parse.verbatim);
+val alt_string = token Parse.alt_string;
+val symbolic = token Parse.keyword_ident_or_symbolic;
-fun $$$ x = (ident >> T.content_of || P.keyword)
+fun $$$ x = (ident >> T.content_of || Parse.keyword)
:|-- (fn y => if x = y then Scan.succeed x else Scan.fail);
@@ -158,7 +157,7 @@
val name_source_position = named >> T.source_position_of;
val name = named >> T.content_of;
-val binding = P.position name >> Binding.make;
+val binding = Parse.position name >> Binding.make;
val alt_name = alt_string >> T.content_of;
val symbol = symbolic >> T.content_of;
val liberal_name = symbol || name;
@@ -216,12 +215,12 @@
(* improper method arguments *)
val from_to =
- P.nat -- ($$$ "-" |-- P.nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
- P.nat --| $$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) ||
- P.nat >> (fn i => fn tac => tac i) ||
+ Parse.nat -- ($$$ "-" |-- Parse.nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
+ Parse.nat --| $$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) ||
+ Parse.nat >> (fn i => fn tac => tac i) ||
$$$ "!" >> K ALLGOALS;
-val goal = $$$ "[" |-- P.!!! (from_to --| $$$ "]");
+val goal = $$$ "[" |-- Parse.!!! (from_to --| $$$ "]");
fun goal_spec x = Scan.lift (Scan.optional goal (fn tac => tac 1)) x;
@@ -229,10 +228,10 @@
fun parse_args is_symid =
let
- val keyword_symid = token (P.keyword_with is_symid);
- fun atom blk = P.group "argument"
+ val keyword_symid = token (Parse.keyword_with is_symid);
+ fun atom blk = Parse.group "argument"
(ident || keyword_symid || string || alt_string ||
- (if blk then token (P.$$$ ",") else Scan.fail));
+ (if blk then token (Parse.$$$ ",") else Scan.fail));
fun args blk x = Scan.optional (args1 blk) [] x
and args1 blk x =
@@ -240,7 +239,8 @@
(Scan.repeat1 (atom blk) ||
argsp "(" ")" ||
argsp "[" "]")) >> flat) x
- and argsp l r x = (token (P.$$$ l) ::: P.!!! (args true @@@ (token (P.$$$ r) >> single))) x;
+ and argsp l r x =
+ (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;
@@ -253,8 +253,8 @@
let
val attrib_name = internal_text || (symbolic || named)
>> evaluate T.Text (intern o T.content_of);
- val attrib = P.position (attrib_name -- P.!!! parse) >> src;
- in $$$ "[" |-- P.!!! (P.list attrib --| $$$ "]") end;
+ val attrib = Parse.position (attrib_name -- Parse.!!! parse) >> src;
+ in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;
fun opt_attribs intern = Scan.optional (attribs intern) [];
--- a/src/Pure/Isar/attrib.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/attrib.ML Sat May 15 23:16:32 2010 +0200
@@ -48,7 +48,6 @@
struct
structure T = OuterLex;
-structure P = OuterParse;
(* source and bindings *)
@@ -168,10 +167,10 @@
(** parsing attributed theorems **)
-val thm_sel = P.$$$ "(" |-- P.list1
- (P.nat --| P.minus -- P.nat >> Facts.FromTo ||
- P.nat --| P.minus >> Facts.From ||
- P.nat >> Facts.Single) --| P.$$$ ")";
+val thm_sel = Parse.$$$ "(" |-- Parse.list1
+ (Parse.nat --| Parse.minus -- Parse.nat >> Facts.FromTo ||
+ Parse.nat --| Parse.minus >> Facts.From ||
+ Parse.nat >> Facts.Single) --| Parse.$$$ ")";
local
@@ -184,7 +183,7 @@
val get_fact = get o Facts.Fact;
fun get_named pos name = get (Facts.Named ((name, pos), NONE));
in
- P.$$$ "[" |-- Args.attribs (intern thy) --| P.$$$ "]" >> (fn srcs =>
+ Parse.$$$ "[" |-- Args.attribs (intern thy) --| Parse.$$$ "]" >> (fn srcs =>
let
val atts = map (attribute_i thy) srcs;
val (context', th') = Library.apply atts (context, Drule.dummy_thm);
@@ -192,7 +191,7 @@
||
(Scan.ahead Args.alt_name -- Args.named_fact get_fact
>> (fn (s, fact) => ("", Facts.Fact s, fact)) ||
- Scan.ahead (P.position fact_name) :|-- (fn (name, pos) =>
+ Scan.ahead (Parse.position fact_name) :|-- (fn (name, pos) =>
Args.named_fact (get_named pos) -- Scan.option thm_sel
>> (fn (fact, sel) => (name, Facts.Named ((name, pos), sel), fact))))
-- Args.opt_attribs (intern thy) >> (fn ((name, thmref, fact), srcs) =>
@@ -223,11 +222,11 @@
(* rule composition *)
val COMP_att =
- Scan.lift (Scan.optional (Args.bracks P.nat) 1) -- thm
+ Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- thm
>> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => Drule.compose_single (A, i, B)));
val THEN_att =
- Scan.lift (Scan.optional (Args.bracks P.nat) 1) -- thm
+ Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- thm
>> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)));
val OF_att =
@@ -267,7 +266,7 @@
val eta_long =
Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion));
-val rotated = Scan.optional P.int 1 >> (fn n => Thm.rule_attribute (K (rotate_prems n)));
+val rotated = Scan.optional Parse.int 1 >> (fn n => Thm.rule_attribute (K (rotate_prems n)));
(* theory setup *)
@@ -285,9 +284,9 @@
"rename bound variables in abstractions" #>
setup (Binding.name "unfolded") unfolded "unfolded definitions" #>
setup (Binding.name "folded") folded "folded definitions" #>
- setup (Binding.name "consumes") (Scan.lift (Scan.optional P.nat 1) >> Rule_Cases.consumes)
+ setup (Binding.name "consumes") (Scan.lift (Scan.optional Parse.nat 1) >> Rule_Cases.consumes)
"number of consumed facts" #>
- setup (Binding.name "constraints") (Scan.lift P.nat >> Rule_Cases.constraints)
+ setup (Binding.name "constraints") (Scan.lift Parse.nat >> Rule_Cases.constraints)
"number of equality constraints" #>
setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> Rule_Cases.case_names)
"named rule cases" #>
@@ -295,7 +294,7 @@
(Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
"named conclusion of rule cases" #>
setup (Binding.name "params")
- (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
+ (Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
"named rule parameters" #>
setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.export_without_context)))
"result put into standard form (legacy)" #>
@@ -345,13 +344,13 @@
local
-val equals = P.$$$ "=";
+val equals = Parse.$$$ "=";
fun scan_value (Config.Bool _) =
equals -- Args.$$$ "false" >> K (Config.Bool false) ||
equals -- Args.$$$ "true" >> K (Config.Bool true) ||
Scan.succeed (Config.Bool true)
- | scan_value (Config.Int _) = equals |-- P.int >> Config.Int
+ | scan_value (Config.Int _) = equals |-- Parse.int >> Config.Int
| scan_value (Config.String _) = equals |-- Args.name >> Config.String;
fun scan_config thy config =
--- a/src/Pure/Isar/context_rules.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/context_rules.ML Sat May 15 23:16:32 2010 +0200
@@ -203,7 +203,7 @@
fun add a b c x =
(Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) --
- Scan.option OuterParse.nat) >> (fn (f, n) => f n)) x;
+ Scan.option Parse.nat) >> (fn (f, n) => f n)) x;
val _ = Context.>> (Context.map_theory
(Attrib.setup (Binding.name "intro") (add intro_bang intro intro_query)
--- a/src/Pure/Isar/isar_cmd.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Sat May 15 23:16:32 2010 +0200
@@ -507,7 +507,7 @@
fun check_text (txt, pos) state =
(Position.report Markup.doc_source pos;
- ignore (ThyOutput.eval_antiquote (#1 (OuterKeyword.get_lexicons ())) state (txt, pos)));
+ ignore (ThyOutput.eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
fun header_markup txt = Toplevel.keep (fn state =>
if Toplevel.is_toplevel state then check_text txt state
--- a/src/Pure/Isar/isar_document.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/isar_document.ML Sat May 15 23:16:32 2010 +0200
@@ -275,27 +275,28 @@
(** concrete syntax **)
-local structure P = OuterParse structure V = ValueParse in
+local structure V = ValueParse in
val _ =
OuterSyntax.internal_command "Isar.define_command"
- (P.string -- P.string >> (fn (id, text) =>
+ (Parse.string -- Parse.string >> (fn (id, text) =>
Toplevel.position (Position.id_only id) o
Toplevel.imperative (fn () =>
define_command id (OuterSyntax.prepare_command (Position.id id) text))));
val _ =
OuterSyntax.internal_command "Isar.begin_document"
- (P.string -- P.string >> (fn (id, path) =>
+ (Parse.string -- Parse.string >> (fn (id, path) =>
Toplevel.imperative (fn () => begin_document id (Path.explode path))));
val _ =
OuterSyntax.internal_command "Isar.end_document"
- (P.string >> (fn id => Toplevel.imperative (fn () => end_document id)));
+ (Parse.string >> (fn id => Toplevel.imperative (fn () => end_document id)));
val _ =
OuterSyntax.internal_command "Isar.edit_document"
- (P.string -- P.string -- V.list (P.string -- (P.string >> SOME) || P.string >> rpair NONE)
+ (Parse.string -- Parse.string --
+ V.list (Parse.string -- (Parse.string >> SOME) || Parse.string >> rpair NONE)
>> (fn ((id, new_id), edits) =>
Toplevel.position (Position.id_only new_id) o
Toplevel.imperative (fn () => edit_document id new_id edits)));
--- a/src/Pure/Isar/isar_syn.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML Sat May 15 23:16:32 2010 +0200
@@ -7,15 +7,12 @@
structure IsarSyn: sig end =
struct
-structure P = OuterParse and K = OuterKeyword;
-
-
(** keywords **)
(*keep keywords consistent with the parsers, otherwise be prepared for
unexpected errors*)
-val _ = List.app OuterKeyword.keyword
+val _ = List.app Keyword.keyword
["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
"=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
"\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
@@ -30,54 +27,54 @@
(** init and exit **)
val _ =
- OuterSyntax.command "theory" "begin theory" (K.tag_theory K.thy_begin)
+ OuterSyntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
(Thy_Header.args >> (Toplevel.print oo IsarCmd.init_theory));
val _ =
- OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end)
+ OuterSyntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
(Scan.succeed (Toplevel.exit o Toplevel.end_local_theory));
(** markup commands **)
-val _ = OuterSyntax.markup_command ThyOutput.Markup "header" "theory header" K.diag
- (P.doc_source >> IsarCmd.header_markup);
+val _ = OuterSyntax.markup_command ThyOutput.Markup "header" "theory header" Keyword.diag
+ (Parse.doc_source >> IsarCmd.header_markup);
val _ = OuterSyntax.markup_command ThyOutput.Markup "chapter" "chapter heading"
- K.thy_heading (P.opt_target -- P.doc_source >> IsarCmd.local_theory_markup);
+ Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
val _ = OuterSyntax.markup_command ThyOutput.Markup "section" "section heading"
- K.thy_heading (P.opt_target -- P.doc_source >> IsarCmd.local_theory_markup);
+ Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
val _ = OuterSyntax.markup_command ThyOutput.Markup "subsection" "subsection heading"
- K.thy_heading (P.opt_target -- P.doc_source >> IsarCmd.local_theory_markup);
+ Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
val _ =
OuterSyntax.markup_command ThyOutput.Markup "subsubsection" "subsubsection heading"
- K.thy_heading (P.opt_target -- P.doc_source >> IsarCmd.local_theory_markup);
+ Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
val _ = OuterSyntax.markup_command ThyOutput.MarkupEnv "text" "formal comment (theory)"
- K.thy_decl (P.opt_target -- P.doc_source >> IsarCmd.local_theory_markup);
+ Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
val _ = OuterSyntax.markup_command ThyOutput.Verbatim "text_raw" "raw document preparation text"
- K.thy_decl (P.opt_target -- P.doc_source >> IsarCmd.local_theory_markup);
+ Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
val _ = OuterSyntax.markup_command ThyOutput.Markup "sect" "formal comment (proof)"
- (K.tag_proof K.prf_heading) (P.doc_source >> IsarCmd.proof_markup);
+ (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
val _ = OuterSyntax.markup_command ThyOutput.Markup "subsect" "formal comment (proof)"
- (K.tag_proof K.prf_heading) (P.doc_source >> IsarCmd.proof_markup);
+ (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
val _ = OuterSyntax.markup_command ThyOutput.Markup "subsubsect" "formal comment (proof)"
- (K.tag_proof K.prf_heading) (P.doc_source >> IsarCmd.proof_markup);
+ (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
val _ = OuterSyntax.markup_command ThyOutput.MarkupEnv "txt" "formal comment (proof)"
- (K.tag_proof K.prf_decl) (P.doc_source >> IsarCmd.proof_markup);
+ (Keyword.tag_proof Keyword.prf_decl) (Parse.doc_source >> IsarCmd.proof_markup);
val _ = OuterSyntax.markup_command ThyOutput.Verbatim "txt_raw"
- "raw document preparation text (proof)" (K.tag_proof K.prf_decl)
- (P.doc_source >> IsarCmd.proof_markup);
+ "raw document preparation text (proof)" (Keyword.tag_proof Keyword.prf_decl)
+ (Parse.doc_source >> IsarCmd.proof_markup);
@@ -86,175 +83,185 @@
(* classes and sorts *)
val _ =
- OuterSyntax.command "classes" "declare type classes" K.thy_decl
- (Scan.repeat1 (P.binding -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
- P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
+ OuterSyntax.command "classes" "declare type classes" Keyword.thy_decl
+ (Scan.repeat1 (Parse.binding -- Scan.optional ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |--
+ Parse.!!! (Parse.list1 Parse.xname)) [])
+ >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
val _ =
- OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl
- (P.and_list1 (P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname))
+ OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" Keyword.thy_decl
+ (Parse.and_list1 (Parse.xname -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<")
+ |-- Parse.!!! Parse.xname))
>> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
val _ =
OuterSyntax.local_theory "default_sort" "declare default sort for explicit type variables"
- K.thy_decl
- (P.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
+ Keyword.thy_decl
+ (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
(* types *)
val _ =
- OuterSyntax.local_theory "typedecl" "type declaration" K.thy_decl
- (P.type_args -- P.binding -- P.opt_mixfix
+ OuterSyntax.local_theory "typedecl" "type declaration" Keyword.thy_decl
+ (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
>> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
val _ =
- OuterSyntax.local_theory "types" "declare type abbreviations" K.thy_decl
+ OuterSyntax.local_theory "types" "declare type abbreviations" Keyword.thy_decl
(Scan.repeat1
- (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_mixfix')))
+ (Parse.type_args -- Parse.binding --
+ (Parse.$$$ "=" |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix')))
>> (fold (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)));
val _ =
OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
- K.thy_decl (Scan.repeat1 P.binding >> (Toplevel.theory o Sign.add_nonterminals));
+ Keyword.thy_decl (Scan.repeat1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals));
val _ =
- OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
- (Scan.repeat1 P.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity_cmd));
+ OuterSyntax.command "arities" "state type arities (axiomatic!)" Keyword.thy_decl
+ (Scan.repeat1 Parse.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity_cmd));
(* consts and syntax *)
val _ =
- OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl
- (P.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
+ OuterSyntax.command "judgment" "declare object-logic judgment" Keyword.thy_decl
+ (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
val _ =
- OuterSyntax.command "consts" "declare constants" K.thy_decl
- (Scan.repeat1 P.const_binding >> (Toplevel.theory o Sign.add_consts));
+ OuterSyntax.command "consts" "declare constants" Keyword.thy_decl
+ (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts));
-val opt_overloaded = P.opt_keyword "overloaded";
+val opt_overloaded = Parse.opt_keyword "overloaded";
val _ =
- OuterSyntax.command "finalconsts" "declare constants as final" K.thy_decl
- (opt_overloaded -- Scan.repeat1 P.term >> (uncurry (Toplevel.theory oo Theory.add_finals)));
+ OuterSyntax.command "finalconsts" "declare constants as final" Keyword.thy_decl
+ (opt_overloaded -- Scan.repeat1 Parse.term >> (uncurry (Toplevel.theory oo Theory.add_finals)));
val mode_spec =
- (P.$$$ "output" >> K ("", false)) || P.name -- Scan.optional (P.$$$ "output" >> K false) true;
+ (Parse.$$$ "output" >> K ("", false)) ||
+ Parse.name -- Scan.optional (Parse.$$$ "output" >> K false) true;
val opt_mode =
- Scan.optional (P.$$$ "(" |-- P.!!! (mode_spec --| P.$$$ ")")) Syntax.mode_default;
+ Scan.optional (Parse.$$$ "(" |-- Parse.!!! (mode_spec --| Parse.$$$ ")")) Syntax.mode_default;
val _ =
- OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl
- (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.add_modesyntax));
+ OuterSyntax.command "syntax" "declare syntactic constants" Keyword.thy_decl
+ (opt_mode -- Scan.repeat1 Parse.const >> (Toplevel.theory o uncurry Sign.add_modesyntax));
val _ =
- OuterSyntax.command "no_syntax" "delete syntax declarations" K.thy_decl
- (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Sign.del_modesyntax));
+ OuterSyntax.command "no_syntax" "delete syntax declarations" Keyword.thy_decl
+ (opt_mode -- Scan.repeat1 Parse.const >> (Toplevel.theory o uncurry Sign.del_modesyntax));
(* translations *)
val trans_pat =
- Scan.optional (P.$$$ "(" |-- P.!!! (P.xname --| P.$$$ ")")) "logic" -- P.string;
+ Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.xname --| Parse.$$$ ")")) "logic"
+ -- Parse.string;
fun trans_arrow toks =
- ((P.$$$ "\\<rightharpoonup>" || P.$$$ "=>") >> K Syntax.ParseRule ||
- (P.$$$ "\\<leftharpoondown>" || P.$$$ "<=") >> K Syntax.PrintRule ||
- (P.$$$ "\\<rightleftharpoons>" || P.$$$ "==") >> K Syntax.ParsePrintRule) toks;
+ ((Parse.$$$ "\\<rightharpoonup>" || Parse.$$$ "=>") >> K Syntax.ParseRule ||
+ (Parse.$$$ "\\<leftharpoondown>" || Parse.$$$ "<=") >> K Syntax.PrintRule ||
+ (Parse.$$$ "\\<rightleftharpoons>" || Parse.$$$ "==") >> K Syntax.ParsePrintRule) toks;
val trans_line =
- trans_pat -- P.!!! (trans_arrow -- trans_pat)
+ trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
>> (fn (left, (arr, right)) => arr (left, right));
val _ =
- OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl
+ OuterSyntax.command "translations" "declare syntax translation rules" Keyword.thy_decl
(Scan.repeat1 trans_line >> (Toplevel.theory o Sign.add_trrules));
val _ =
- OuterSyntax.command "no_translations" "remove syntax translation rules" K.thy_decl
+ OuterSyntax.command "no_translations" "remove syntax translation rules" Keyword.thy_decl
(Scan.repeat1 trans_line >> (Toplevel.theory o Sign.del_trrules));
(* axioms and definitions *)
val _ =
- OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
+ OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" Keyword.thy_decl
(Scan.repeat1 SpecParse.spec >>
(Toplevel.theory o
(IsarCmd.add_axioms o
tap (fn _ => legacy_feature "Old 'axioms' command -- use 'axiomatization' instead"))));
val opt_unchecked_overloaded =
- Scan.optional (P.$$$ "(" |-- P.!!!
- (((P.$$$ "unchecked" >> K true) -- Scan.optional (P.$$$ "overloaded" >> K true) false ||
- P.$$$ "overloaded" >> K (false, true)) --| P.$$$ ")")) (false, false);
+ Scan.optional (Parse.$$$ "(" |-- Parse.!!!
+ (((Parse.$$$ "unchecked" >> K true) -- Scan.optional (Parse.$$$ "overloaded" >> K true) false ||
+ Parse.$$$ "overloaded" >> K (false, true)) --| Parse.$$$ ")")) (false, false);
val _ =
- OuterSyntax.command "defs" "define constants" K.thy_decl
+ OuterSyntax.command "defs" "define constants" Keyword.thy_decl
(opt_unchecked_overloaded --
- Scan.repeat1 (SpecParse.thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y)))
+ Scan.repeat1 (SpecParse.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
>> (Toplevel.theory o IsarCmd.add_defs));
(* old constdefs *)
val old_constdecl =
- P.binding --| P.where_ >> (fn x => (x, NONE, NoSyn)) ||
- P.binding -- (P.$$$ "::" |-- P.!!! P.typ >> SOME) -- P.opt_mixfix'
- --| Scan.option P.where_ >> P.triple1 ||
- P.binding -- (P.mixfix >> pair NONE) --| Scan.option P.where_ >> P.triple2;
+ Parse.binding --| Parse.where_ >> (fn x => (x, NONE, NoSyn)) ||
+ Parse.binding -- (Parse.$$$ "::" |-- Parse.!!! Parse.typ >> SOME) -- Parse.opt_mixfix'
+ --| Scan.option Parse.where_ >> Parse.triple1 ||
+ Parse.binding -- (Parse.mixfix >> pair NONE) --| Scan.option Parse.where_ >> Parse.triple2;
-val old_constdef = Scan.option old_constdecl -- (SpecParse.opt_thm_name ":" -- P.prop);
+val old_constdef = Scan.option old_constdecl -- (SpecParse.opt_thm_name ":" -- Parse.prop);
val structs =
- Scan.optional ((P.$$$ "(" -- P.$$$ "structure") |-- P.!!! (P.simple_fixes --| P.$$$ ")")) [];
+ Scan.optional ((Parse.$$$ "(" -- Parse.$$$ "structure")
+ |-- Parse.!!! (Parse.simple_fixes --| Parse.$$$ ")")) [];
val _ =
- OuterSyntax.command "constdefs" "old-style constant definition" K.thy_decl
+ OuterSyntax.command "constdefs" "old-style constant definition" Keyword.thy_decl
(structs -- Scan.repeat1 old_constdef >> (Toplevel.theory o Constdefs.add_constdefs));
(* constant definitions and abbreviations *)
val _ =
- OuterSyntax.local_theory "definition" "constant definition" K.thy_decl
+ OuterSyntax.local_theory "definition" "constant definition" Keyword.thy_decl
(SpecParse.constdef >> (fn args => #2 o Specification.definition_cmd args));
val _ =
- OuterSyntax.local_theory "abbreviation" "constant abbreviation" K.thy_decl
- (opt_mode -- (Scan.option SpecParse.constdecl -- P.prop)
- >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
+ OuterSyntax.local_theory "abbreviation" "constant abbreviation" Keyword.thy_decl
+ (opt_mode -- (Scan.option SpecParse.constdecl -- Parse.prop)
+ >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
val _ =
- OuterSyntax.local_theory "type_notation" "add concrete syntax for type constructors" K.thy_decl
- (opt_mode -- P.and_list1 (P.xname -- P.mixfix)
- >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
+ OuterSyntax.local_theory "type_notation" "add concrete syntax for type constructors"
+ Keyword.thy_decl
+ (opt_mode -- Parse.and_list1 (Parse.xname -- Parse.mixfix)
+ >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
val _ =
- OuterSyntax.local_theory "no_type_notation" "delete concrete syntax for type constructors" K.thy_decl
- (opt_mode -- P.and_list1 (P.xname -- P.mixfix)
- >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
+ OuterSyntax.local_theory "no_type_notation" "delete concrete syntax for type constructors"
+ Keyword.thy_decl
+ (opt_mode -- Parse.and_list1 (Parse.xname -- Parse.mixfix)
+ >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
val _ =
- OuterSyntax.local_theory "notation" "add concrete syntax for constants / fixed variables" K.thy_decl
- (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
- >> (fn (mode, args) => Specification.notation_cmd true mode args));
+ OuterSyntax.local_theory "notation" "add concrete syntax for constants / fixed variables"
+ Keyword.thy_decl
+ (opt_mode -- Parse.and_list1 (Parse.xname -- SpecParse.locale_mixfix)
+ >> (fn (mode, args) => Specification.notation_cmd true mode args));
val _ =
- OuterSyntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables" K.thy_decl
- (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
- >> (fn (mode, args) => Specification.notation_cmd false mode args));
+ OuterSyntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables"
+ Keyword.thy_decl
+ (opt_mode -- Parse.and_list1 (Parse.xname -- SpecParse.locale_mixfix)
+ >> (fn (mode, args) => Specification.notation_cmd false mode args));
(* constant specifications *)
val _ =
- OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl
- (Scan.optional P.fixes [] --
- Scan.optional (P.where_ |-- P.!!! (P.and_list1 SpecParse.specs)) []
- >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
+ OuterSyntax.command "axiomatization" "axiomatic constant specification" Keyword.thy_decl
+ (Scan.optional Parse.fixes [] --
+ Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 SpecParse.specs)) []
+ >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
(* theorems *)
@@ -263,30 +270,30 @@
SpecParse.name_facts >> (fn args => #2 o Specification.theorems_cmd kind args);
val _ =
- OuterSyntax.local_theory "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK);
+ OuterSyntax.local_theory "theorems" "define theorems" Keyword.thy_decl (theorems Thm.theoremK);
val _ =
- OuterSyntax.local_theory "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK);
+ OuterSyntax.local_theory "lemmas" "define lemmas" Keyword.thy_decl (theorems Thm.lemmaK);
val _ =
- OuterSyntax.local_theory "declare" "declare theorems" K.thy_decl
- (P.and_list1 SpecParse.xthms1
+ OuterSyntax.local_theory "declare" "declare theorems" Keyword.thy_decl
+ (Parse.and_list1 SpecParse.xthms1
>> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.empty_binding, flat args)]));
(* name space entry path *)
val _ =
- OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl
+ OuterSyntax.command "global" "disable prefixing of theory name" Keyword.thy_decl
(Scan.succeed (Toplevel.theory Sign.root_path));
val _ =
- OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl
+ OuterSyntax.command "local" "enable prefixing of theory name" Keyword.thy_decl
(Scan.succeed (Toplevel.theory Sign.local_path));
fun hide_names name hide what =
- OuterSyntax.command name ("hide " ^ what ^ " from name space") K.thy_decl
- ((P.opt_keyword "open" >> not) -- Scan.repeat1 P.xname >>
+ OuterSyntax.command name ("hide " ^ what ^ " from name space") Keyword.thy_decl
+ ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 Parse.xname >>
(Toplevel.theory o uncurry hide));
val _ = hide_names "hide_class" IsarCmd.hide_class "classes";
@@ -305,101 +312,104 @@
(Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf;
val _ =
- OuterSyntax.command "use" "ML text from file" (K.tag_ml K.thy_decl)
- (P.path >> (fn path => Toplevel.generic_theory (ThyInfo.exec_file false path #> propagate_env)));
+ OuterSyntax.command "use" "ML text from file" (Keyword.tag_ml Keyword.thy_decl)
+ (Parse.path >>
+ (fn path => Toplevel.generic_theory (ThyInfo.exec_file false path #> propagate_env)));
val _ =
- OuterSyntax.command "ML" "ML text within theory or local theory" (K.tag_ml K.thy_decl)
- (P.ML_source >> (fn (txt, pos) =>
+ OuterSyntax.command "ML" "ML text within theory or local theory"
+ (Keyword.tag_ml Keyword.thy_decl)
+ (Parse.ML_source >> (fn (txt, pos) =>
Toplevel.generic_theory
(ML_Context.exec (fn () => ML_Context.eval true pos txt) #> propagate_env)));
val _ =
- OuterSyntax.command "ML_prf" "ML text within proof" (K.tag_proof K.prf_decl)
- (P.ML_source >> (fn (txt, pos) =>
+ OuterSyntax.command "ML_prf" "ML text within proof" (Keyword.tag_proof Keyword.prf_decl)
+ (Parse.ML_source >> (fn (txt, pos) =>
Toplevel.proof (Proof.map_context (Context.proof_map
(ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf)));
val _ =
- OuterSyntax.command "ML_val" "diagnostic ML text" (K.tag_ml K.diag)
- (P.ML_source >> IsarCmd.ml_diag true);
+ OuterSyntax.command "ML_val" "diagnostic ML text" (Keyword.tag_ml Keyword.diag)
+ (Parse.ML_source >> IsarCmd.ml_diag true);
val _ =
- OuterSyntax.command "ML_command" "diagnostic ML text (silent)" (K.tag_ml K.diag)
- (P.ML_source >> (Toplevel.no_timing oo IsarCmd.ml_diag false));
+ OuterSyntax.command "ML_command" "diagnostic ML text (silent)" (Keyword.tag_ml Keyword.diag)
+ (Parse.ML_source >> (Toplevel.no_timing oo IsarCmd.ml_diag false));
val _ =
- OuterSyntax.command "setup" "ML theory setup" (K.tag_ml K.thy_decl)
- (P.ML_source >> (Toplevel.theory o IsarCmd.global_setup));
+ OuterSyntax.command "setup" "ML theory setup" (Keyword.tag_ml Keyword.thy_decl)
+ (Parse.ML_source >> (Toplevel.theory o IsarCmd.global_setup));
val _ =
- OuterSyntax.local_theory "local_setup" "ML local theory setup" (K.tag_ml K.thy_decl)
- (P.ML_source >> IsarCmd.local_setup);
+ OuterSyntax.local_theory "local_setup" "ML local theory setup" (Keyword.tag_ml Keyword.thy_decl)
+ (Parse.ML_source >> IsarCmd.local_setup);
val _ =
- OuterSyntax.command "attribute_setup" "define attribute in ML" (K.tag_ml K.thy_decl)
- (P.position P.name -- P.!!! (P.$$$ "=" |-- P.ML_source -- P.text)
- >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
+ OuterSyntax.command "attribute_setup" "define attribute in ML" (Keyword.tag_ml Keyword.thy_decl)
+ (Parse.position Parse.name -- Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Parse.text)
+ >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
val _ =
- OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)
- (P.position P.name -- P.!!! (P.$$$ "=" |-- P.ML_source -- P.text)
- >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
+ OuterSyntax.command "method_setup" "define proof method in ML" (Keyword.tag_ml Keyword.thy_decl)
+ (Parse.position Parse.name -- Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Parse.text)
+ >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
val _ =
- OuterSyntax.local_theory "declaration" "generic ML declaration" (K.tag_ml K.thy_decl)
- (P.opt_keyword "pervasive" -- P.ML_source >> uncurry IsarCmd.declaration);
+ OuterSyntax.local_theory "declaration" "generic ML declaration" (Keyword.tag_ml Keyword.thy_decl)
+ (Parse.opt_keyword "pervasive" -- Parse.ML_source >> uncurry IsarCmd.declaration);
val _ =
- OuterSyntax.local_theory "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl)
- (P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") --
- P.ML_source -- Scan.optional (P.$$$ "identifier" |-- Scan.repeat1 P.xname) []
+ OuterSyntax.local_theory "simproc_setup" "define simproc in ML" (Keyword.tag_ml Keyword.thy_decl)
+ (Parse.name --
+ (Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")" --| Parse.$$$ "=") --
+ Parse.ML_source -- Scan.optional (Parse.$$$ "identifier" |-- Scan.repeat1 Parse.xname) []
>> (fn (((a, b), c), d) => IsarCmd.simproc_setup a b c d));
(* translation functions *)
-val trfun = P.opt_keyword "advanced" -- P.ML_source;
+val trfun = Parse.opt_keyword "advanced" -- Parse.ML_source;
val _ =
OuterSyntax.command "parse_ast_translation" "install parse ast translation functions"
- (K.tag_ml K.thy_decl)
+ (Keyword.tag_ml Keyword.thy_decl)
(trfun >> (Toplevel.theory o IsarCmd.parse_ast_translation));
val _ =
OuterSyntax.command "parse_translation" "install parse translation functions"
- (K.tag_ml K.thy_decl)
+ (Keyword.tag_ml Keyword.thy_decl)
(trfun >> (Toplevel.theory o IsarCmd.parse_translation));
val _ =
OuterSyntax.command "print_translation" "install print translation functions"
- (K.tag_ml K.thy_decl)
+ (Keyword.tag_ml Keyword.thy_decl)
(trfun >> (Toplevel.theory o IsarCmd.print_translation));
val _ =
OuterSyntax.command "typed_print_translation" "install typed print translation functions"
- (K.tag_ml K.thy_decl)
+ (Keyword.tag_ml Keyword.thy_decl)
(trfun >> (Toplevel.theory o IsarCmd.typed_print_translation));
val _ =
OuterSyntax.command "print_ast_translation" "install print ast translation functions"
- (K.tag_ml K.thy_decl)
+ (Keyword.tag_ml Keyword.thy_decl)
(trfun >> (Toplevel.theory o IsarCmd.print_ast_translation));
(* oracles *)
val _ =
- OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl)
- (P.position P.name -- (P.$$$ "=" |-- P.ML_source) >>
+ OuterSyntax.command "oracle" "declare oracle" (Keyword.tag_ml Keyword.thy_decl)
+ (Parse.position Parse.name -- (Parse.$$$ "=" |-- Parse.ML_source) >>
(fn (x, y) => Toplevel.theory (IsarCmd.oracle x y)));
(* local theories *)
val _ =
- OuterSyntax.command "context" "enter local theory context" K.thy_decl
- (P.name --| P.begin >> (fn name =>
+ OuterSyntax.command "context" "enter local theory context" Keyword.thy_decl
+ (Parse.name --| Parse.begin >> (fn name =>
Toplevel.print o Toplevel.begin_local_theory true (Theory_Target.context_cmd name)));
@@ -407,36 +417,38 @@
val locale_val =
SpecParse.locale_expression false --
- Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
+ Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
Scan.repeat1 SpecParse.context_element >> pair ([], []);
val _ =
- OuterSyntax.command "locale" "define named proof context" K.thy_decl
- (P.binding -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin
+ OuterSyntax.command "locale" "define named proof context" Keyword.thy_decl
+ (Parse.binding --
+ Scan.optional (Parse.$$$ "=" |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
>> (fn ((name, (expr, elems)), begin) =>
(begin ? Toplevel.print) o Toplevel.begin_local_theory begin
(Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
val _ =
OuterSyntax.command "sublocale"
- "prove sublocale relation between a locale and a locale expression" K.thy_goal
- (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! (SpecParse.locale_expression false)
+ "prove sublocale relation between a locale and a locale expression" Keyword.thy_goal
+ (Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
+ Parse.!!! (SpecParse.locale_expression false)
>> (fn (loc, expr) =>
Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr)));
val _ =
OuterSyntax.command "interpretation"
- "prove interpretation of locale expression in theory" K.thy_goal
- (P.!!! (SpecParse.locale_expression true) --
- Scan.optional (P.where_ |-- P.and_list1 (SpecParse.opt_thm_name ":" -- P.prop)) []
+ "prove interpretation of locale expression in theory" Keyword.thy_goal
+ (Parse.!!! (SpecParse.locale_expression true) --
+ Scan.optional (Parse.where_ |-- Parse.and_list1 (SpecParse.opt_thm_name ":" -- Parse.prop)) []
>> (fn (expr, equations) => Toplevel.print o
Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations)));
val _ =
OuterSyntax.command "interpret"
"prove interpretation of locale expression in proof context"
- (K.tag_proof K.prf_goal)
- (P.!!! (SpecParse.locale_expression true)
+ (Keyword.tag_proof Keyword.prf_goal)
+ (Parse.!!! (SpecParse.locale_expression true)
>> (fn expr => Toplevel.print o Toplevel.proof' (Expression.interpret_cmd expr)));
@@ -444,41 +456,43 @@
val class_val =
SpecParse.class_expr --
- Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
+ Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
Scan.repeat1 SpecParse.context_element >> pair [];
val _ =
- OuterSyntax.command "class" "define type class" K.thy_decl
- (P.binding -- Scan.optional (P.$$$ "=" |-- class_val) ([], []) -- P.opt_begin
+ OuterSyntax.command "class" "define type class" Keyword.thy_decl
+ (Parse.binding -- Scan.optional (Parse.$$$ "=" |-- class_val) ([], []) -- Parse.opt_begin
>> (fn ((name, (supclasses, elems)), begin) =>
(begin ? Toplevel.print) o Toplevel.begin_local_theory begin
(Class.class_cmd name supclasses elems #> snd)));
val _ =
- OuterSyntax.local_theory_to_proof "subclass" "prove a subclass relation" K.thy_goal
- (P.xname >> Class.subclass_cmd);
+ OuterSyntax.local_theory_to_proof "subclass" "prove a subclass relation" Keyword.thy_goal
+ (Parse.xname >> Class.subclass_cmd);
val _ =
- OuterSyntax.command "instantiation" "instantiate and prove type arity" K.thy_decl
- (P.multi_arity --| P.begin
+ OuterSyntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl
+ (Parse.multi_arity --| Parse.begin
>> (fn arities => Toplevel.print o
Toplevel.begin_local_theory true (Theory_Target.instantiation_cmd arities)));
val _ =
- OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
- ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
- P.multi_arity >> Class.instance_arity_cmd)
- >> (Toplevel.print oo Toplevel.theory_to_proof)
- || Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
+ OuterSyntax.command "instance" "prove type arity or subclass relation" Keyword.thy_goal
+ ((Parse.xname -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |-- Parse.!!! Parse.xname)
+ >> Class.classrel_cmd ||
+ Parse.multi_arity >> Class.instance_arity_cmd)
+ >> (Toplevel.print oo Toplevel.theory_to_proof) ||
+ Scan.succeed
+ (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
(* arbitrary overloading *)
val _ =
- OuterSyntax.command "overloading" "overloaded definitions" K.thy_decl
- (Scan.repeat1 (P.name --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term --
- Scan.optional (P.$$$ "(" |-- (P.$$$ "unchecked" >> K false) --| P.$$$ ")") true
- >> P.triple1) --| P.begin
+ OuterSyntax.command "overloading" "overloaded definitions" Keyword.thy_decl
+ (Scan.repeat1 (Parse.name --| (Parse.$$$ "\\<equiv>" || Parse.$$$ "==") -- Parse.term --
+ Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unchecked" >> K false) --| Parse.$$$ ")") true
+ >> Parse.triple1) --| Parse.begin
>> (fn operations => Toplevel.print o
Toplevel.begin_local_theory true (Theory_Target.overloading_cmd operations)));
@@ -486,8 +500,8 @@
(* code generation *)
val _ =
- OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl
- (Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd));
+ OuterSyntax.command "code_datatype" "define set of code datatype constructors" Keyword.thy_decl
+ (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
@@ -499,7 +513,7 @@
OuterSyntax.local_theory_to_proof'
(if schematic then "schematic_" ^ kind else kind)
("state " ^ (if schematic then "schematic " ^ kind else kind))
- (if schematic then K.thy_schematic_goal else K.thy_goal)
+ (if schematic then Keyword.thy_schematic_goal else Keyword.thy_goal)
(Scan.optional (SpecParse.opt_thm_name ":" --|
Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) Attrib.empty_binding --
SpecParse.general_statement >> (fn (a, (elems, concl)) =>
@@ -515,64 +529,64 @@
val _ =
OuterSyntax.local_theory_to_proof "example_proof"
- "example proof body, without any result" K.thy_schematic_goal
+ "example proof body, without any result" Keyword.thy_schematic_goal
(Scan.succeed
(Specification.schematic_theorem_cmd "" NONE (K I)
Attrib.empty_binding [] (Element.Shows []) false #> Proof.enter_forward));
val _ =
OuterSyntax.command "have" "state local goal"
- (K.tag_proof K.prf_goal)
+ (Keyword.tag_proof Keyword.prf_goal)
(SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));
val _ =
OuterSyntax.command "hence" "abbreviates \"then have\""
- (K.tag_proof K.prf_goal)
+ (Keyword.tag_proof Keyword.prf_goal)
(SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence));
val _ =
OuterSyntax.command "show" "state local goal, solving current obligation"
- (K.tag_proof K.prf_asm_goal)
+ (Keyword.tag_proof Keyword.prf_asm_goal)
(SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show));
val _ =
OuterSyntax.command "thus" "abbreviates \"then show\""
- (K.tag_proof K.prf_asm_goal)
+ (Keyword.tag_proof Keyword.prf_asm_goal)
(SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus));
(* facts *)
-val facts = P.and_list1 SpecParse.xthms1;
+val facts = Parse.and_list1 SpecParse.xthms1;
val _ =
OuterSyntax.command "then" "forward chaining"
- (K.tag_proof K.prf_chain)
+ (Keyword.tag_proof Keyword.prf_chain)
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain));
val _ =
OuterSyntax.command "from" "forward chaining from given facts"
- (K.tag_proof K.prf_chain)
+ (Keyword.tag_proof Keyword.prf_chain)
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss_cmd)));
val _ =
OuterSyntax.command "with" "forward chaining from given and current facts"
- (K.tag_proof K.prf_chain)
+ (Keyword.tag_proof Keyword.prf_chain)
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss_cmd)));
val _ =
OuterSyntax.command "note" "define facts"
- (K.tag_proof K.prf_decl)
+ (Keyword.tag_proof Keyword.prf_decl)
(SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));
val _ =
OuterSyntax.command "using" "augment goal facts"
- (K.tag_proof K.prf_decl)
+ (Keyword.tag_proof Keyword.prf_decl)
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_cmd)));
val _ =
OuterSyntax.command "unfolding" "unfold definitions in goal and facts"
- (K.tag_proof K.prf_decl)
+ (Keyword.tag_proof Keyword.prf_decl)
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding_cmd)));
@@ -580,57 +594,59 @@
val _ =
OuterSyntax.command "fix" "fix local variables (Skolem constants)"
- (K.tag_proof K.prf_asm)
- (P.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd)));
+ (Keyword.tag_proof Keyword.prf_asm)
+ (Parse.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd)));
val _ =
OuterSyntax.command "assume" "assume propositions"
- (K.tag_proof K.prf_asm)
+ (Keyword.tag_proof Keyword.prf_asm)
(SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
val _ =
OuterSyntax.command "presume" "assume propositions, to be established later"
- (K.tag_proof K.prf_asm)
+ (Keyword.tag_proof Keyword.prf_asm)
(SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
val _ =
OuterSyntax.command "def" "local definition"
- (K.tag_proof K.prf_asm)
- (P.and_list1
+ (Keyword.tag_proof Keyword.prf_asm)
+ (Parse.and_list1
(SpecParse.opt_thm_name ":" --
- ((P.binding -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
+ ((Parse.binding -- Parse.opt_mixfix) --
+ ((Parse.$$$ "\\<equiv>" || Parse.$$$ "==") |-- Parse.!!! Parse.termp)))
>> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
val _ =
OuterSyntax.command "obtain" "generalized existence"
- (K.tag_proof K.prf_asm_goal)
- (P.parname -- Scan.optional (P.fixes --| P.where_) [] -- SpecParse.statement
+ (Keyword.tag_proof Keyword.prf_asm_goal)
+ (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- SpecParse.statement
>> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z)));
val _ =
OuterSyntax.command "guess" "wild guessing (unstructured)"
- (K.tag_proof K.prf_asm_goal)
- (Scan.optional P.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));
+ (Keyword.tag_proof Keyword.prf_asm_goal)
+ (Scan.optional Parse.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));
val _ =
OuterSyntax.command "let" "bind text variables"
- (K.tag_proof K.prf_decl)
- (P.and_list1 (P.and_list1 P.term -- (P.$$$ "=" |-- P.term))
+ (Keyword.tag_proof Keyword.prf_decl)
+ (Parse.and_list1 (Parse.and_list1 Parse.term -- (Parse.$$$ "=" |-- Parse.term))
>> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));
val _ =
OuterSyntax.command "write" "add concrete syntax for constants / fixed variables"
- (K.tag_proof K.prf_decl)
- (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
+ (Keyword.tag_proof Keyword.prf_decl)
+ (opt_mode -- Parse.and_list1 (Parse.xname -- SpecParse.locale_mixfix)
>> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
val case_spec =
- (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.maybe P.name) --| P.$$$ ")") ||
- P.xname >> rpair []) -- SpecParse.opt_attribs >> P.triple1;
+ (Parse.$$$ "(" |--
+ Parse.!!! (Parse.xname -- Scan.repeat1 (Parse.maybe Parse.name) --| Parse.$$$ ")") ||
+ Parse.xname >> rpair []) -- SpecParse.opt_attribs >> Parse.triple1;
val _ =
OuterSyntax.command "case" "invoke local context"
- (K.tag_proof K.prf_asm)
+ (Keyword.tag_proof Keyword.prf_asm)
(case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case_cmd)));
@@ -638,17 +654,17 @@
val _ =
OuterSyntax.command "{" "begin explicit proof block"
- (K.tag_proof K.prf_open)
+ (Keyword.tag_proof Keyword.prf_open)
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block));
val _ =
OuterSyntax.command "}" "end explicit proof block"
- (K.tag_proof K.prf_close)
+ (Keyword.tag_proof Keyword.prf_close)
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));
val _ =
OuterSyntax.command "next" "enter next proof block"
- (K.tag_proof K.prf_block)
+ (Keyword.tag_proof Keyword.prf_block)
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block));
@@ -656,37 +672,37 @@
val _ =
OuterSyntax.command "qed" "conclude (sub-)proof"
- (K.tag_proof K.qed_block)
+ (Keyword.tag_proof Keyword.qed_block)
(Scan.option Method.parse >> IsarCmd.qed);
val _ =
OuterSyntax.command "by" "terminal backward proof"
- (K.tag_proof K.qed)
+ (Keyword.tag_proof Keyword.qed)
(Method.parse -- Scan.option Method.parse >> IsarCmd.terminal_proof);
val _ =
OuterSyntax.command ".." "default proof"
- (K.tag_proof K.qed)
+ (Keyword.tag_proof Keyword.qed)
(Scan.succeed IsarCmd.default_proof);
val _ =
OuterSyntax.command "." "immediate proof"
- (K.tag_proof K.qed)
+ (Keyword.tag_proof Keyword.qed)
(Scan.succeed IsarCmd.immediate_proof);
val _ =
OuterSyntax.command "done" "done proof"
- (K.tag_proof K.qed)
+ (Keyword.tag_proof Keyword.qed)
(Scan.succeed IsarCmd.done_proof);
val _ =
OuterSyntax.command "sorry" "skip proof (quick-and-dirty mode only!)"
- (K.tag_proof K.qed)
+ (Keyword.tag_proof Keyword.qed)
(Scan.succeed IsarCmd.skip_proof);
val _ =
OuterSyntax.command "oops" "forget proof"
- (K.tag_proof K.qed_global)
+ (Keyword.tag_proof Keyword.qed_global)
(Scan.succeed Toplevel.forget_proof);
@@ -694,27 +710,27 @@
val _ =
OuterSyntax.command "defer" "shuffle internal proof state"
- (K.tag_proof K.prf_script)
- (Scan.option P.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer)));
+ (Keyword.tag_proof Keyword.prf_script)
+ (Scan.option Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer)));
val _ =
OuterSyntax.command "prefer" "shuffle internal proof state"
- (K.tag_proof K.prf_script)
- (P.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer)));
+ (Keyword.tag_proof Keyword.prf_script)
+ (Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer)));
val _ =
OuterSyntax.command "apply" "initial refinement step (unstructured)"
- (K.tag_proof K.prf_script)
+ (Keyword.tag_proof Keyword.prf_script)
(Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply)));
val _ =
OuterSyntax.command "apply_end" "terminal refinement (unstructured)"
- (K.tag_proof K.prf_script)
+ (Keyword.tag_proof Keyword.prf_script)
(Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end)));
val _ =
OuterSyntax.command "proof" "backward proof"
- (K.tag_proof K.prf_block)
+ (Keyword.tag_proof Keyword.prf_block)
(Scan.option Method.parse >> (fn m => Toplevel.print o
Toplevel.actual_proof (Proof_Node.applys (Proof.proof m)) o
Toplevel.skip_proof (fn i => i + 1)));
@@ -723,26 +739,26 @@
(* calculational proof commands *)
val calc_args =
- Scan.option (P.$$$ "(" |-- P.!!! ((SpecParse.xthms1 --| P.$$$ ")")));
+ Scan.option (Parse.$$$ "(" |-- Parse.!!! ((SpecParse.xthms1 --| Parse.$$$ ")")));
val _ =
OuterSyntax.command "also" "combine calculation and current facts"
- (K.tag_proof K.prf_decl)
+ (Keyword.tag_proof Keyword.prf_decl)
(calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
val _ =
OuterSyntax.command "finally" "combine calculation and current facts, exhibit result"
- (K.tag_proof K.prf_chain)
+ (Keyword.tag_proof Keyword.prf_chain)
(calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
val _ =
OuterSyntax.command "moreover" "augment calculation by current facts"
- (K.tag_proof K.prf_decl)
+ (Keyword.tag_proof Keyword.prf_decl)
(Scan.succeed (Toplevel.proof' Calculation.moreover));
val _ =
OuterSyntax.command "ultimately" "augment calculation by current facts, exhibit result"
- (K.tag_proof K.prf_chain)
+ (Keyword.tag_proof Keyword.prf_chain)
(Scan.succeed (Toplevel.proof' Calculation.ultimately));
@@ -750,18 +766,19 @@
val _ =
OuterSyntax.command "back" "backtracking of proof command"
- (K.tag_proof K.prf_script)
+ (Keyword.tag_proof Keyword.prf_script)
(Scan.succeed (Toplevel.print o Toplevel.actual_proof Proof_Node.back o Toplevel.skip_proof I));
(* nested commands *)
val props_text =
- Scan.optional ValueParse.properties [] -- P.position P.string >> (fn (props, (str, pos)) =>
- (Position.of_properties (Position.default_properties pos props), str));
+ Scan.optional ValueParse.properties [] -- Parse.position Parse.string
+ >> (fn (props, (str, pos)) =>
+ (Position.of_properties (Position.default_properties pos props), str));
val _ =
- OuterSyntax.improper_command "Isabelle.command" "nested Isabelle command" K.control
+ OuterSyntax.improper_command "Isabelle.command" "nested Isabelle command" Keyword.control
(props_text :|-- (fn (pos, str) =>
(case OuterSyntax.parse pos str of
[tr] => Scan.succeed (K tr)
@@ -772,151 +789,153 @@
(** diagnostic commands (for interactive mode only) **)
-val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
-val opt_bang = Scan.optional (P.$$$ "!" >> K true) false;
+val opt_modes =
+ Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
+
+val opt_bang = Scan.optional (Parse.$$$ "!" >> K true) false;
val _ =
OuterSyntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
- K.diag (P.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin));
+ Keyword.diag (Parse.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin));
val _ =
- OuterSyntax.improper_command "help" "print outer syntax commands" K.diag
+ OuterSyntax.improper_command "help" "print outer syntax commands" Keyword.diag
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax));
val _ =
- OuterSyntax.improper_command "print_commands" "print outer syntax commands" K.diag
+ OuterSyntax.improper_command "print_commands" "print outer syntax commands" Keyword.diag
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative OuterSyntax.print_outer_syntax));
val _ =
- OuterSyntax.improper_command "print_configs" "print configuration options" K.diag
+ OuterSyntax.improper_command "print_configs" "print configuration options" Keyword.diag
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_configs));
val _ =
- OuterSyntax.improper_command "print_context" "print theory context name" K.diag
+ OuterSyntax.improper_command "print_context" "print theory context name" Keyword.diag
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_context));
val _ =
- OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag
- (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory));
+ OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)"
+ Keyword.diag (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory));
val _ =
- OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)" K.diag
- (Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax));
+ OuterSyntax.improper_command "print_syntax" "print inner syntax of context (verbose!)"
+ Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax));
val _ =
- OuterSyntax.improper_command "print_abbrevs" "print constant abbreviation of context" K.diag
- (Scan.succeed (Toplevel.no_timing o IsarCmd.print_abbrevs));
+ OuterSyntax.improper_command "print_abbrevs" "print constant abbreviation of context"
+ Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.print_abbrevs));
val _ =
OuterSyntax.improper_command "print_theorems"
- "print theorems of local theory or proof context" K.diag
+ "print theorems of local theory or proof context" Keyword.diag
(opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theorems));
val _ =
- OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag
+ OuterSyntax.improper_command "print_locales" "print locales of this theory" Keyword.diag
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales));
val _ =
- OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag
+ OuterSyntax.improper_command "print_classes" "print classes of this theory" Keyword.diag
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
o Toplevel.keep (Class.print_classes o Toplevel.theory_of)));
val _ =
- OuterSyntax.improper_command "print_locale" "print locale of this theory" K.diag
- (opt_bang -- P.xname >> (Toplevel.no_timing oo IsarCmd.print_locale));
+ OuterSyntax.improper_command "print_locale" "print locale of this theory" Keyword.diag
+ (opt_bang -- Parse.xname >> (Toplevel.no_timing oo IsarCmd.print_locale));
val _ =
OuterSyntax.improper_command "print_interps"
- "print interpretations of locale for this theory" K.diag
- (P.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations));
+ "print interpretations of locale for this theory" Keyword.diag
+ (Parse.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations));
val _ =
- OuterSyntax.improper_command "print_attributes" "print attributes of this theory" K.diag
+ OuterSyntax.improper_command "print_attributes" "print attributes of this theory" Keyword.diag
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
val _ =
- OuterSyntax.improper_command "print_simpset" "print context of Simplifier" K.diag
+ OuterSyntax.improper_command "print_simpset" "print context of Simplifier" Keyword.diag
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_simpset));
val _ =
- OuterSyntax.improper_command "print_rules" "print intro/elim rules" K.diag
+ OuterSyntax.improper_command "print_rules" "print intro/elim rules" Keyword.diag
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_rules));
val _ =
- OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" K.diag
+ OuterSyntax.improper_command "print_trans_rules" "print transitivity rules" Keyword.diag
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules));
val _ =
- OuterSyntax.improper_command "print_methods" "print methods of this theory" K.diag
+ OuterSyntax.improper_command "print_methods" "print methods of this theory" Keyword.diag
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods));
val _ =
- OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" K.diag
+ OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" Keyword.diag
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
val _ =
OuterSyntax.improper_command "thy_deps" "visualize theory dependencies"
- K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.thy_deps));
+ Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.thy_deps));
val _ =
OuterSyntax.improper_command "class_deps" "visualize class dependencies"
- K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps));
+ Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps));
val _ =
OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
- K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
+ Keyword.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
val _ =
- OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
+ OuterSyntax.improper_command "print_binds" "print term bindings of proof context" Keyword.diag
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
val _ =
- OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag
+ OuterSyntax.improper_command "print_facts" "print facts of proof context" Keyword.diag
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts));
val _ =
- OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag
+ OuterSyntax.improper_command "print_cases" "print cases of proof context" Keyword.diag
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases));
val _ =
- OuterSyntax.improper_command "print_statement" "print theorems as long statements" K.diag
+ OuterSyntax.improper_command "print_statement" "print theorems as long statements" Keyword.diag
(opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts));
val _ =
- OuterSyntax.improper_command "thm" "print theorems" K.diag
+ OuterSyntax.improper_command "thm" "print theorems" Keyword.diag
(opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
val _ =
- OuterSyntax.improper_command "prf" "print proof terms of theorems" K.diag
+ OuterSyntax.improper_command "prf" "print proof terms of theorems" Keyword.diag
(opt_modes -- Scan.option SpecParse.xthms1
>> (Toplevel.no_timing oo IsarCmd.print_prfs false));
val _ =
- OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" K.diag
+ OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" Keyword.diag
(opt_modes -- Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true));
val _ =
- OuterSyntax.improper_command "prop" "read and print proposition" K.diag
- (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_prop));
+ OuterSyntax.improper_command "prop" "read and print proposition" Keyword.diag
+ (opt_modes -- Parse.term >> (Toplevel.no_timing oo IsarCmd.print_prop));
val _ =
- OuterSyntax.improper_command "term" "read and print term" K.diag
- (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_term));
+ OuterSyntax.improper_command "term" "read and print term" Keyword.diag
+ (opt_modes -- Parse.term >> (Toplevel.no_timing oo IsarCmd.print_term));
val _ =
- OuterSyntax.improper_command "typ" "read and print type" K.diag
- (opt_modes -- P.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
+ OuterSyntax.improper_command "typ" "read and print type" Keyword.diag
+ (opt_modes -- Parse.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
val _ =
- OuterSyntax.improper_command "print_codesetup" "print code generator setup" K.diag
+ OuterSyntax.improper_command "print_codesetup" "print code generator setup" Keyword.diag
(Scan.succeed
(Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
(Code.print_codesetup o Toplevel.theory_of)));
val _ =
- OuterSyntax.improper_command "unused_thms" "find unused theorems" K.diag
- (Scan.option ((Scan.repeat1 (Scan.unless P.minus P.name) --| P.minus) --
- Scan.option (Scan.repeat1 (Scan.unless P.minus P.name))) >>
+ OuterSyntax.improper_command "unused_thms" "find unused theorems" Keyword.diag
+ (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
+ Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >>
(Toplevel.no_timing oo IsarCmd.unused_thms));
@@ -924,66 +943,66 @@
(** system commands (for interactive mode only) **)
val _ =
- OuterSyntax.improper_command "cd" "change current working directory" K.diag
- (P.path >> (Toplevel.no_timing oo IsarCmd.cd));
+ OuterSyntax.improper_command "cd" "change current working directory" Keyword.diag
+ (Parse.path >> (Toplevel.no_timing oo IsarCmd.cd));
val _ =
- OuterSyntax.improper_command "pwd" "print current working directory" K.diag
+ OuterSyntax.improper_command "pwd" "print current working directory" Keyword.diag
(Scan.succeed (Toplevel.no_timing o IsarCmd.pwd));
val _ =
- OuterSyntax.improper_command "use_thy" "use theory file" K.diag
- (P.name >> (fn name =>
+ OuterSyntax.improper_command "use_thy" "use theory file" Keyword.diag
+ (Parse.name >> (fn name =>
Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.use_thy name)));
val _ =
- OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag
- (P.name >> (fn name =>
+ OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" Keyword.diag
+ (Parse.name >> (fn name =>
Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.touch_thy name)));
val _ =
- OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag
- (P.name >> (fn name =>
+ OuterSyntax.improper_command "remove_thy" "remove theory from loader database" Keyword.diag
+ (Parse.name >> (fn name =>
Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.remove_thy name)));
val _ =
OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
- K.diag (P.name >> (fn name =>
+ Keyword.diag (Parse.name >> (fn name =>
Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.kill_thy name)));
val _ =
OuterSyntax.improper_command "display_drafts" "display raw source files with symbols"
- K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.display_drafts));
+ Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo IsarCmd.display_drafts));
val _ =
OuterSyntax.improper_command "print_drafts" "print raw source files with symbols"
- K.diag (Scan.repeat1 P.path >> (Toplevel.no_timing oo IsarCmd.print_drafts));
+ Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo IsarCmd.print_drafts));
val opt_limits =
- Scan.option P.nat -- Scan.option (P.$$$ "," |-- P.!!! P.nat);
+ Scan.option Parse.nat -- Scan.option (Parse.$$$ "," |-- Parse.!!! Parse.nat);
val _ =
- OuterSyntax.improper_command "pr" "print current proof state (if present)" K.diag
+ OuterSyntax.improper_command "pr" "print current proof state (if present)" Keyword.diag
(opt_modes -- opt_limits >> (Toplevel.no_timing oo IsarCmd.pr));
val _ =
- OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" K.diag
+ OuterSyntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.diag
(Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr));
val _ =
- OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag
+ OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.diag
(Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr));
val _ =
- OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag
- (P.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit));
+ OuterSyntax.improper_command "commit" "commit current session to ML database" Keyword.diag
+ (Parse.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit));
val _ =
- OuterSyntax.improper_command "quit" "quit Isabelle" K.control
- (P.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit));
+ OuterSyntax.improper_command "quit" "quit Isabelle" Keyword.control
+ (Parse.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit));
val _ =
- OuterSyntax.improper_command "exit" "exit Isar loop" K.control
+ OuterSyntax.improper_command "exit" "exit Isar loop" Keyword.control
(Scan.succeed (Toplevel.no_timing o IsarCmd.exit));
end;
--- a/src/Pure/Isar/method.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/method.ML Sat May 15 23:16:32 2010 +0200
@@ -382,9 +382,6 @@
(** concrete syntax **)
-structure P = OuterParse;
-
-
(* sections *)
type modifier = (Proof.context -> Proof.context) * attribute;
@@ -407,7 +404,7 @@
(* extra rule methods *)
fun xrule_meth m =
- Scan.lift (Scan.optional (Args.parens OuterParse.nat) 0) -- Attrib.thms >>
+ Scan.lift (Scan.optional (Args.parens Parse.nat) 0) -- Attrib.thms >>
(fn (n, ths) => K (m n ths));
@@ -419,18 +416,18 @@
local
fun meth4 x =
- (P.position (P.xname >> rpair []) >> (Source o Args.src) ||
- P.$$$ "(" |-- P.!!! (meth0 --| P.$$$ ")")) x
+ (Parse.position (Parse.xname >> rpair []) >> (Source o Args.src) ||
+ Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x
and meth3 x =
- (meth4 --| P.$$$ "?" >> Try ||
- meth4 --| P.$$$ "+" >> Repeat1 ||
- meth4 -- (P.$$$ "[" |-- Scan.optional P.nat 1 --| P.$$$ "]") >> (SelectGoals o swap) ||
+ (meth4 --| Parse.$$$ "?" >> Try ||
+ meth4 --| Parse.$$$ "+" >> Repeat1 ||
+ meth4 -- (Parse.$$$ "[" |-- Scan.optional Parse.nat 1 --| Parse.$$$ "]") >> (SelectGoals o swap) ||
meth4) x
and meth2 x =
- (P.position (P.xname -- Args.parse1 is_symid_meth) >> (Source o Args.src) ||
+ (Parse.position (Parse.xname -- Args.parse1 is_symid_meth) >> (Source o Args.src) ||
meth3) x
-and meth1 x = (P.enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
-and meth0 x = (P.enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
+and meth1 x = (Parse.enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
+and meth0 x = (Parse.enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
in val parse = meth3 end;
@@ -463,12 +460,12 @@
setup (Binding.name "rename_tac") (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name) >>
(fn (quant, xs) => K (SIMPLE_METHOD'' quant (Tactic.rename_tac xs))))
"rename parameters of goal" #>
- setup (Binding.name "rotate_tac") (Args.goal_spec -- Scan.lift (Scan.optional P.int 1) >>
+ setup (Binding.name "rotate_tac") (Args.goal_spec -- Scan.lift (Scan.optional Parse.int 1) >>
(fn (quant, i) => K (SIMPLE_METHOD'' quant (Tactic.rotate_tac i))))
"rotate assumptions of goal" #>
- setup (Binding.name "tactic") (Scan.lift (P.position Args.name) >> tactic)
+ setup (Binding.name "tactic") (Scan.lift (Parse.position Args.name) >> tactic)
"ML tactic as proof method" #>
- setup (Binding.name "raw_tactic") (Scan.lift (P.position Args.name) >> raw_tactic)
+ setup (Binding.name "raw_tactic") (Scan.lift (Parse.position Args.name) >> raw_tactic)
"ML tactic as raw proof method"));
--- a/src/Pure/Isar/outer_syntax.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Sat May 15 23:16:32 2010 +0200
@@ -9,20 +9,20 @@
signature OUTER_SYNTAX =
sig
- val command: string -> string -> OuterKeyword.T ->
+ val command: string -> string -> Keyword.T ->
(Toplevel.transition -> Toplevel.transition) parser -> unit
- val markup_command: ThyOutput.markup -> string -> string -> OuterKeyword.T ->
+ val markup_command: ThyOutput.markup -> string -> string -> Keyword.T ->
(Toplevel.transition -> Toplevel.transition) parser -> unit
- val improper_command: string -> string -> OuterKeyword.T ->
+ val improper_command: string -> string -> Keyword.T ->
(Toplevel.transition -> Toplevel.transition) parser -> unit
val internal_command: string -> (Toplevel.transition -> Toplevel.transition) parser -> unit
- val local_theory': string -> string -> OuterKeyword.T ->
+ val local_theory': string -> string -> Keyword.T ->
(bool -> local_theory -> local_theory) parser -> unit
- val local_theory: string -> string -> OuterKeyword.T ->
+ val local_theory: string -> string -> Keyword.T ->
(local_theory -> local_theory) parser -> unit
- val local_theory_to_proof': string -> string -> OuterKeyword.T ->
+ val local_theory_to_proof': string -> string -> Keyword.T ->
(bool -> local_theory -> Proof.state) parser -> unit
- val local_theory_to_proof: string -> string -> OuterKeyword.T ->
+ 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
@@ -38,8 +38,7 @@
struct
structure T = OuterLex;
-structure P = OuterParse;
-type 'a parser = 'a P.parser;
+type 'a parser = 'a Parse.parser;
@@ -62,20 +61,20 @@
local
fun terminate false = Scan.succeed ()
- | terminate true = P.group "end of input" (Scan.option P.sync -- P.semicolon >> K ());
+ | terminate true = Parse.group "end of input" (Scan.option Parse.sync -- Parse.semicolon >> K ());
fun body cmd (name, _) =
(case cmd name of
SOME (Command {int_only, parse, ...}) =>
- P.!!! (Scan.prompt (name ^ "# ") (P.tags |-- parse >> pair int_only))
+ Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only))
| NONE => sys_error ("no parser for outer syntax command " ^ quote name));
in
fun parse_command do_terminate cmd =
- P.semicolon >> K NONE ||
- P.sync >> K NONE ||
- (P.position P.command :-- body cmd) --| terminate do_terminate
+ Parse.semicolon >> K NONE ||
+ Parse.sync >> K NONE ||
+ (Parse.position Parse.command :-- body cmd) --| terminate do_terminate
>> (fn ((name, pos), (int_only, f)) =>
SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
Toplevel.interactive int_only |> f));
@@ -105,7 +104,7 @@
fun get_markups () = ! global_markups;
fun get_command () = Symtab.lookup (get_commands ());
-fun get_syntax () = CRITICAL (fn () => (OuterKeyword.get_lexicons (), get_command ()));
+fun get_syntax () = CRITICAL (fn () => (Keyword.get_lexicons (), get_command ()));
fun is_markup kind name = AList.lookup (op =) (get_markups ()) name = SOME kind;
@@ -113,7 +112,7 @@
(* augment syntax *)
fun add_command name kind cmd = CRITICAL (fn () =>
- (OuterKeyword.command name kind;
+ (Keyword.command name kind;
if not (Symtab.defined (get_commands ()) name) then ()
else warning ("Redefining outer syntax command " ^ quote name);
change_commands (Symtab.update (name, cmd))));
@@ -130,13 +129,13 @@
end;
fun internal_command name parse =
- command name "(internal)" OuterKeyword.control (parse >> (fn tr => Toplevel.no_timing o tr));
+ command name "(internal)" Keyword.control (parse >> (fn tr => Toplevel.no_timing o tr));
(* local_theory commands *)
fun local_theory_command do_print trans name comment kind parse =
- command name comment kind (P.opt_target -- parse
+ command name comment kind (Parse.opt_target -- parse
>> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
val local_theory' = local_theory_command false Toplevel.local_theory';
@@ -157,7 +156,7 @@
Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
val (int_cmds, cmds) = List.partition #3 (dest_commands ());
in
- [Pretty.strs ("syntax keywords:" :: map quote (OuterKeyword.dest_keywords ())),
+ [Pretty.strs ("syntax keywords:" :: map quote (Keyword.dest_keywords ())),
Pretty.big_list "commands:" (map pretty_cmd cmds),
Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)]
|> Pretty.chunks |> Pretty.writeln
@@ -172,18 +171,18 @@
fun toplevel_source term do_recover cmd src =
let
val no_terminator =
- Scan.unless P.semicolon (Scan.one (T.not_sync andf T.not_eof));
+ Scan.unless Parse.semicolon (Scan.one (T.not_sync andf T.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
- (Scan.bulk (P.$$$ "--" -- P.!!! P.doc_source >> K NONE || P.not_eof >> SOME))
+ (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
- (Scan.bulk (fn xs => P.!!! (parse_command term (cmd ())) xs))
+ (Scan.bulk (fn xs => Parse.!!! (parse_command term (cmd ())) xs))
(Option.map recover do_recover)
|> Source.map_filter I
end;
@@ -194,13 +193,13 @@
fun scan pos str =
Source.of_string str
|> Symbol.source {do_recover = false}
- |> T.source {do_recover = SOME false} OuterKeyword.get_lexicons pos
+ |> T.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} OuterKeyword.get_lexicons pos
+ |> T.source {do_recover = SOME false} Keyword.get_lexicons pos
|> toplevel_source false NONE get_command
|> Source.exhaust;
@@ -231,7 +230,7 @@
fun isar term : isar =
Source.tty
|> Symbol.source {do_recover = true}
- |> T.source {do_recover = SOME true} OuterKeyword.get_lexicons Position.none
+ |> T.source {do_recover = SOME true} Keyword.get_lexicons Position.none
|> toplevel_source term (SOME true) get_command;
@@ -291,7 +290,7 @@
val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
fun after_load () =
- ThyOutput.present_thy (#1 lexs) OuterKeyword.command_tags is_markup (Lazy.force results) toks
+ ThyOutput.present_thy (#1 lexs) Keyword.command_tags is_markup (Lazy.force results) toks
|> Buffer.content
|> Present.theory_output name;
in after_load end;
--- a/src/Pure/Isar/rule_insts.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/rule_insts.ML Sat May 15 23:16:32 2010 +0200
@@ -30,7 +30,6 @@
struct
structure T = OuterLex;
-structure P = OuterParse;
(** reading instantiations **)
@@ -215,14 +214,14 @@
Args.internal_term >> T.Term ||
Args.name_source >> T.Text;
-val inst = Args.var -- (Args.$$$ "=" |-- Scan.ahead P.not_eof -- value)
+val inst = Args.var -- (Args.$$$ "=" |-- Scan.ahead Parse.not_eof -- value)
>> (fn (xi, (a, v)) => (a, (xi, v)));
in
val _ = Context.>> (Context.map_theory
(Attrib.setup (Binding.name "where")
- (Scan.lift (P.and_list inst) >> (fn args =>
+ (Scan.lift (Parse.and_list inst) >> (fn args =>
Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)))
"named instantiation of theorem"));
@@ -237,7 +236,7 @@
Args.internal_term >> T.Term ||
Args.name_source >> T.Text;
-val inst = Scan.ahead P.not_eof -- Args.maybe value;
+val inst = Scan.ahead Parse.not_eof -- Args.maybe value;
val concl = Args.$$$ "concl" -- Args.colon;
val insts =
@@ -387,7 +386,8 @@
fun method inst_tac tac =
Args.goal_spec --
Scan.optional (Scan.lift
- (P.and_list1 (Args.var -- (Args.$$$ "=" |-- P.!!! Args.name_source)) --| Args.$$$ "in")) [] --
+ (Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_source)) --|
+ Args.$$$ "in")) [] --
Attrib.thms >>
(fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts =>
if null insts then quant (Method.insert_tac facts THEN' tac ctxt thms)
@@ -425,5 +425,5 @@
end;
-structure BasicRuleInsts: BASIC_RULE_INSTS = RuleInsts;
-open BasicRuleInsts;
+structure Basic_Rule_Insts: BASIC_RULE_INSTS = RuleInsts;
+open Basic_Rule_Insts;
--- a/src/Pure/Isar/spec_parse.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/spec_parse.ML Sat May 15 23:16:32 2010 +0200
@@ -35,121 +35,129 @@
structure SpecParse: SPEC_PARSE =
struct
-structure P = OuterParse;
-
-
(* theorem specifications *)
-val attrib = P.position ((P.keyword_ident_or_symbolic || P.xname) -- P.!!! Args.parse) >> Args.src;
-val attribs = P.$$$ "[" |-- P.list attrib --| P.$$$ "]";
+val attrib =
+ Parse.position ((Parse.keyword_ident_or_symbolic || Parse.xname) -- Parse.!!! Args.parse)
+ >> Args.src;
+
+val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
val opt_attribs = Scan.optional attribs [];
-fun thm_name s = P.binding -- opt_attribs --| P.$$$ s;
+fun thm_name s = Parse.binding -- opt_attribs --| Parse.$$$ s;
fun opt_thm_name s =
- Scan.optional ((P.binding -- opt_attribs || attribs >> pair Binding.empty) --| P.$$$ s)
+ Scan.optional ((Parse.binding -- opt_attribs || attribs >> pair Binding.empty) --| Parse.$$$ s)
Attrib.empty_binding;
-val spec = opt_thm_name ":" -- P.prop;
-val specs = opt_thm_name ":" -- Scan.repeat1 P.prop;
+val spec = opt_thm_name ":" -- Parse.prop;
+val specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop;
val alt_specs =
- P.enum1 "|" (spec --| Scan.option (Scan.ahead (P.name || P.$$$ "[") -- P.!!! (P.$$$ "|")));
+ Parse.enum1 "|"
+ (spec --| Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
-val where_alt_specs = P.where_ |-- P.!!! alt_specs;
+val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs;
val xthm =
- P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.named "") ||
- (P.alt_string >> Facts.Fact ||
- P.position P.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
+ Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") ||
+ (Parse.alt_string >> Facts.Fact ||
+ Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
val xthms1 = Scan.repeat1 xthm;
-val name_facts = P.and_list1 (opt_thm_name "=" -- xthms1);
+val name_facts = Parse.and_list1 (opt_thm_name "=" -- xthms1);
(* basic constant specifications *)
val constdecl =
- P.binding --
- (P.where_ >> K (NONE, NoSyn) ||
- P.$$$ "::" |-- P.!!! ((P.typ >> SOME) -- P.opt_mixfix' --| P.where_) ||
- Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
- >> P.triple2;
+ Parse.binding --
+ (Parse.where_ >> K (NONE, NoSyn) ||
+ Parse.$$$ "::" |-- Parse.!!! ((Parse.typ >> SOME) -- Parse.opt_mixfix' --| Parse.where_) ||
+ Scan.ahead (Parse.$$$ "(") |-- Parse.!!! (Parse.mixfix' --| Parse.where_ >> pair NONE))
+ >> Parse.triple2;
-val constdef = Scan.option constdecl -- (opt_thm_name ":" -- P.prop);
+val constdef = Scan.option constdecl -- (opt_thm_name ":" -- Parse.prop);
(* locale and context elements *)
-val locale_mixfix = P.$$$ "(" -- P.$$$ "structure" -- P.!!! (P.$$$ ")") >> K Structure || P.mixfix;
+val locale_mixfix =
+ Parse.$$$ "(" -- Parse.$$$ "structure" -- Parse.!!! (Parse.$$$ ")") >> K Structure ||
+ Parse.mixfix;
val locale_fixes =
- P.and_list1 (P.binding -- Scan.option (P.$$$ "::" |-- P.typ) -- locale_mixfix
- >> (single o P.triple1) ||
- P.params >> map Syntax.no_syn) >> flat;
+ Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- locale_mixfix
+ >> (single o Parse.triple1) ||
+ Parse.params >> map Syntax.no_syn) >> flat;
val locale_insts =
- Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) []
- -- Scan.optional (P.where_ |-- P.and_list1 (opt_thm_name ":" -- P.prop)) [];
+ Scan.optional
+ (Parse.$$$ "[" |-- Parse.!!! (Scan.repeat1 (Parse.maybe Parse.term) --| Parse.$$$ "]")) [] --
+ Scan.optional (Parse.where_ |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) [];
local
val loc_element =
- P.$$$ "fixes" |-- P.!!! locale_fixes >> Element.Fixes ||
- P.$$$ "constrains" |-- P.!!! (P.and_list1 (P.name -- (P.$$$ "::" |-- P.typ)))
+ Parse.$$$ "fixes" |-- Parse.!!! locale_fixes >> Element.Fixes ||
+ Parse.$$$ "constrains" |--
+ Parse.!!! (Parse.and_list1 (Parse.name -- (Parse.$$$ "::" |-- Parse.typ)))
>> Element.Constrains ||
- P.$$$ "assumes" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp))
+ Parse.$$$ "assumes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp))
>> Element.Assumes ||
- P.$$$ "defines" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- P.propp))
+ Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp))
>> Element.Defines ||
- P.$$$ "notes" |-- P.!!! (P.and_list1 (opt_thm_name "=" -- xthms1))
+ Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- xthms1))
>> (curry Element.Notes "");
fun plus1_unless test scan =
- scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
+ scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
fun prefix mandatory =
- P.name -- (P.$$$ "!" >> K true || P.$$$ "?" >> K false || Scan.succeed mandatory) --| P.$$$ ":";
+ Parse.name --
+ (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
+ Parse.$$$ ":";
-val instance = P.where_ |--
- P.and_list1 (P.name -- (P.$$$ "=" |-- P.term)) >> Expression.Named ||
- Scan.repeat1 (P.maybe P.term) >> Expression.Positional;
+val instance = Parse.where_ |--
+ Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named ||
+ Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional;
in
-val locale_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
- P.$$$ "defines" || P.$$$ "notes";
+val locale_keyword =
+ Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
+ Parse.$$$ "defines" || Parse.$$$ "notes";
-val class_expr = plus1_unless locale_keyword P.xname;
+val class_expr = plus1_unless locale_keyword Parse.xname;
fun locale_expression mandatory =
let
- val expr2 = P.xname;
+ val expr2 = Parse.xname;
val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
val expr0 = plus1_unless locale_keyword expr1;
- in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end;
+ in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
-val context_element = P.group "context element" loc_element;
+val context_element = Parse.group "context element" loc_element;
end;
(* statements *)
-val statement = P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp);
+val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
val obtain_case =
- P.parbinding -- (Scan.optional (P.simple_fixes --| P.where_) [] --
- (P.and_list1 (Scan.repeat1 P.prop) >> flat));
+ Parse.parbinding -- (Scan.optional (Parse.simple_fixes --| Parse.where_) [] --
+ (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
val general_statement =
statement >> (fn x => ([], Element.Shows x)) ||
Scan.repeat context_element --
- (P.$$$ "obtains" |-- P.!!! (P.enum1 "|" obtain_case) >> Element.Obtains ||
- P.$$$ "shows" |-- P.!!! statement >> Element.Shows);
+ (Parse.$$$ "obtains" |-- Parse.!!! (Parse.enum1 "|" obtain_case) >> Element.Obtains ||
+ Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows);
-val statement_keyword = P.$$$ "obtains" || P.$$$ "shows";
+val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
end;
--- a/src/Pure/Isar/toplevel.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Sat May 15 23:16:32 2010 +0200
@@ -660,8 +660,8 @@
let val st' = command tr st in
if immediate orelse
null proof_trs orelse
- OuterKeyword.is_schematic_goal (name_of tr) orelse
- exists (OuterKeyword.is_qed_global o name_of) proof_trs orelse
+ Keyword.is_schematic_goal (name_of tr) orelse
+ exists (Keyword.is_qed_global o name_of) proof_trs orelse
not (can proof_of st') orelse
Proof.is_relevant (proof_of st')
then
--- a/src/Pure/Isar/value_parse.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/value_parse.ML Sat May 15 23:16:32 2010 +0200
@@ -19,27 +19,24 @@
structure ValueParse: VALUE_PARSE =
struct
-structure P = OuterParse;
-
-
(* syntax utilities *)
-fun comma p = P.$$$ "," |-- P.!!! p;
-fun equal p = P.$$$ "=" |-- P.!!! p;
-fun parens p = P.$$$ "(" |-- P.!!! (p --| P.$$$ ")");
+fun comma p = Parse.$$$ "," |-- Parse.!!! p;
+fun equal p = Parse.$$$ "=" |-- Parse.!!! p;
+fun parens p = Parse.$$$ "(" |-- Parse.!!! (p --| Parse.$$$ ")");
(* tuples *)
val unit = parens (Scan.succeed ());
fun pair p1 p2 = parens (p1 -- comma p2);
-fun triple p1 p2 p3 = parens (p1 -- comma p2 -- comma p3) >> P.triple1;
+fun triple p1 p2 p3 = parens (p1 -- comma p2 -- comma p3) >> Parse.triple1;
(* lists *)
-fun list p = parens (P.enum "," p);
-val properties = list (P.string -- equal P.string);
+fun list p = parens (Parse.enum "," p);
+val properties = list (Parse.string -- equal Parse.string);
end;
--- a/src/Pure/ML/ml_antiquote.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Sat May 15 23:16:32 2010 +0200
@@ -57,12 +57,11 @@
(** misc antiquotations **)
-structure P = OuterParse;
-
val _ = inline "make_string" (Scan.succeed ml_make_string);
val _ = value "binding"
- (Scan.lift (P.position Args.name) >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
+ (Scan.lift (Parse.position Args.name)
+ >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
val _ = value "theory"
(Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name)
@@ -80,11 +79,12 @@
val _ = inline "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
val _ = macro "let" (Args.context --
- Scan.lift (P.and_list1 (P.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
+ Scan.lift
+ (Parse.and_list1 (Parse.and_list1 Args.name_source -- (Args.$$$ "=" |-- Args.name_source)))
>> (fn (ctxt, args) => #2 (ProofContext.match_bind true args ctxt)));
val _ = macro "note" (Args.context :|-- (fn ctxt =>
- P.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
+ Parse.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
((a, map (Attrib.attribute (ProofContext.theory_of ctxt)) srcs), [(ths, [])])))
>> (fn args => #2 (ProofContext.note_thmss "" args ctxt))));
@@ -118,7 +118,7 @@
(* type constructors *)
-fun type_name kind check = Args.context -- Scan.lift (OuterParse.position Args.name_source)
+fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_source)
>> (fn (ctxt, (s, pos)) =>
let
val Type (c, _) = ProofContext.read_type_name_proper ctxt false s;
@@ -137,7 +137,7 @@
(* constants *)
-fun const_name check = Args.context -- Scan.lift (OuterParse.position Args.name_source)
+fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_source)
>> (fn (ctxt, (s, pos)) =>
let
val Const (c, _) = ProofContext.read_const_proper ctxt false s;
@@ -151,13 +151,13 @@
val _ = inline "syntax_const"
- (Args.context -- Scan.lift (OuterParse.position Args.name) >> (fn (ctxt, (c, pos)) =>
+ (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
if Syntax.is_const (ProofContext.syn_of ctxt) c then ML_Syntax.print_string c
else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos)));
val _ = inline "const"
(Args.context -- Scan.lift Args.name_source -- Scan.optional
- (Scan.lift (Args.$$$ "(") |-- OuterParse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
+ (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
>> (fn ((ctxt, raw_c), Ts) =>
let
val Const (c, _) = ProofContext.read_const_proper ctxt true raw_c;
--- a/src/Pure/ML/ml_context.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/ML/ml_context.ML Sat May 15 23:16:32 2010 +0200
@@ -112,11 +112,10 @@
local
-structure P = OuterParse;
structure T = OuterLex;
val antiq =
- P.!!! (P.position P.xname -- Args.parse --| Scan.ahead P.eof)
+ Parse.!!! (Parse.position Parse.xname -- Args.parse --| Scan.ahead Parse.eof)
>> (fn ((x, pos), y) => Args.src ((x, y), pos));
val begin_env = ML_Lex.tokenize "structure Isabelle =\nstruct\n";
@@ -138,7 +137,7 @@
NONE => error ("No context -- cannot expand ML antiquotations" ^ Position.str_of pos)
| SOME ctxt => Context.proof_of ctxt);
- val lex = #1 (OuterKeyword.get_lexicons ());
+ val lex = #1 (Keyword.get_lexicons ());
fun no_decl _ = ([], []);
fun expand (Antiquote.Text tok) state = (K ([], [tok]), state)
--- a/src/Pure/ML/ml_thms.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/ML/ml_thms.ML Sat May 15 23:16:32 2010 +0200
@@ -54,7 +54,7 @@
val _ = ML_Context.add_antiq "lemma"
(fn _ => Args.context -- Args.mode "open" --
- Scan.lift (OuterParse.and_list1 (Scan.repeat1 goal) --
+ Scan.lift (Parse.and_list1 (Scan.repeat1 goal) --
(by |-- Method.parse -- Scan.option Method.parse)) >>
(fn ((ctxt, is_open), (raw_propss, methods)) => fn background =>
let
--- a/src/Pure/Proof/extraction.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Proof/extraction.ML Sat May 15 23:16:32 2010 +0200
@@ -750,31 +750,29 @@
(**** interface ****)
-structure P = OuterParse and K = OuterKeyword;
-
-val parse_vars = Scan.optional (P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") [];
+val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
val _ =
OuterSyntax.command "realizers"
"specify realizers for primitive axioms / theorems, together with correctness proof"
- K.thy_decl
- (Scan.repeat1 (P.xname -- parse_vars --| P.$$$ ":" -- P.string -- P.string) >>
+ Keyword.thy_decl
+ (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
(fn xs => Toplevel.theory (fn thy => add_realizers
(map (fn (((a, vs), s1), s2) => (PureThy.get_thm thy a, (vs, s1, s2))) xs) thy)));
val _ =
OuterSyntax.command "realizability"
- "add equations characterizing realizability" K.thy_decl
- (Scan.repeat1 P.string >> (Toplevel.theory o add_realizes_eqns));
+ "add equations characterizing realizability" Keyword.thy_decl
+ (Scan.repeat1 Parse.string >> (Toplevel.theory o add_realizes_eqns));
val _ =
OuterSyntax.command "extract_type"
- "add equations characterizing type of extracted program" K.thy_decl
- (Scan.repeat1 P.string >> (Toplevel.theory o add_typeof_eqns));
+ "add equations characterizing type of extracted program" Keyword.thy_decl
+ (Scan.repeat1 Parse.string >> (Toplevel.theory o add_typeof_eqns));
val _ =
- OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl
- (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
+ OuterSyntax.command "extract" "extract terms from proofs" Keyword.thy_decl
+ (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
extract (map (apfst (PureThy.get_thm thy)) xs) thy)));
val etype_of = etype_of o add_syntax;
--- a/src/Pure/ProofGeneral/pgip_parser.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML Sat May 15 23:16:32 2010 +0200
@@ -12,7 +12,6 @@
structure PgipParser: PGIP_PARSER =
struct
-structure K = OuterKeyword;
structure D = PgipMarkup;
structure I = PgipIsabelle;
@@ -51,42 +50,42 @@
fun closegoal text = [D.Closegoal {text = text}, D.Closeblock {}];
-fun command k f = Symtab.update_new (OuterKeyword.kind_of k, f);
+fun command k f = Symtab.update_new (Keyword.kind_of k, f);
val command_keywords = Symtab.empty
- |> command K.control badcmd
- |> command K.diag (fn text => [D.Spuriouscmd {text = text}])
- |> command K.thy_begin thy_begin
- |> command K.thy_switch badcmd
- |> command K.thy_end (fn text => [D.Closeblock {}, D.Closetheory {text = text}])
- |> command K.thy_heading thy_heading
- |> command K.thy_decl thy_decl
- |> command K.thy_script thy_decl
- |> command K.thy_goal goal
- |> command K.thy_schematic_goal goal
- |> command K.qed closegoal
- |> command K.qed_block closegoal
- |> command K.qed_global (fn text => [D.Giveupgoal {text = text}])
- |> command K.prf_heading (fn text => [D.Doccomment {text = text}])
- |> command K.prf_goal goal
- |> command K.prf_block prf_block
- |> command K.prf_open prf_open
- |> command K.prf_close (fn text => [D.Proofstep {text = text}, D.Closeblock {}])
- |> command K.prf_chain proofstep
- |> command K.prf_decl proofstep
- |> command K.prf_asm proofstep
- |> command K.prf_asm_goal goal
- |> command K.prf_script proofstep;
+ |> command Keyword.control badcmd
+ |> command Keyword.diag (fn text => [D.Spuriouscmd {text = text}])
+ |> command Keyword.thy_begin thy_begin
+ |> command Keyword.thy_switch badcmd
+ |> command Keyword.thy_end (fn text => [D.Closeblock {}, D.Closetheory {text = text}])
+ |> command Keyword.thy_heading thy_heading
+ |> command Keyword.thy_decl thy_decl
+ |> command Keyword.thy_script thy_decl
+ |> command Keyword.thy_goal goal
+ |> command Keyword.thy_schematic_goal goal
+ |> command Keyword.qed closegoal
+ |> command Keyword.qed_block closegoal
+ |> command Keyword.qed_global (fn text => [D.Giveupgoal {text = text}])
+ |> command Keyword.prf_heading (fn text => [D.Doccomment {text = text}])
+ |> command Keyword.prf_goal goal
+ |> command Keyword.prf_block prf_block
+ |> command Keyword.prf_open prf_open
+ |> command Keyword.prf_close (fn text => [D.Proofstep {text = text}, D.Closeblock {}])
+ |> command Keyword.prf_chain proofstep
+ |> command Keyword.prf_decl proofstep
+ |> command Keyword.prf_asm proofstep
+ |> command Keyword.prf_asm_goal goal
+ |> command Keyword.prf_script proofstep;
-val _ = subset (op =) (OuterKeyword.kinds, Symtab.keys command_keywords)
+val _ = subset (op =) (Keyword.kinds, Symtab.keys command_keywords)
orelse sys_error "Incomplete coverage of command keywords";
fun parse_command "sorry" text = [D.Postponegoal {text = text}, D.Closeblock {}]
| parse_command name text =
- (case OuterKeyword.command_keyword name of
+ (case Keyword.command_keyword name of
NONE => [D.Unparseable {text = text}]
| SOME k =>
- (case Symtab.lookup command_keywords (OuterKeyword.kind_of k) of
+ (case Symtab.lookup command_keywords (Keyword.kind_of k) of
NONE => [D.Unparseable {text = text}]
| SOME f => f text));
@@ -104,6 +103,6 @@
fun pgip_parser pos str =
- maps parse_span (ThySyntax.parse_spans (OuterKeyword.get_lexicons ()) pos str);
+ maps parse_span (ThySyntax.parse_spans (Keyword.get_lexicons ()) pos str);
end;
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Sat May 15 23:16:32 2010 +0200
@@ -188,48 +188,44 @@
(* additional outer syntax for Isar *)
-local structure P = OuterParse and K = OuterKeyword in
-
fun prP () =
- OuterSyntax.improper_command "ProofGeneral.pr" "print state (internal)" K.diag
+ OuterSyntax.improper_command "ProofGeneral.pr" "print state (internal)" Keyword.diag
(Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals ()
else (Toplevel.quiet := false; Toplevel.print_state true state))));
fun undoP () = (*undo without output -- historical*)
- OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
+ OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" Keyword.control
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)));
fun restartP () =
- OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
- (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
+ OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" Keyword.control
+ (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
fun kill_proofP () =
- OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
+ OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" Keyword.control
(Scan.succeed (Toplevel.no_timing o
Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
fun inform_file_processedP () =
- OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
- (P.name >> (fn file =>
+ OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" Keyword.control
+ (Parse.name >> (fn file =>
Toplevel.no_timing o Toplevel.imperative (fn () => inform_file_processed file)));
fun inform_file_retractedP () =
- OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
- (P.name >> (Toplevel.no_timing oo
+ OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" Keyword.control
+ (Parse.name >> (Toplevel.no_timing oo
(fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
fun process_pgipP () =
- OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
- (P.text >> (Toplevel.no_timing oo
+ OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
+ (Parse.text >> (Toplevel.no_timing oo
(fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
fun init_outer_syntax () = List.app (fn f => f ())
[prP, undoP, restartP, kill_proofP, inform_file_processedP,
inform_file_retractedP, process_pgipP];
-end;
-
(* init *)
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sat May 15 23:16:32 2010 +0200
@@ -312,8 +312,8 @@
(** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
fun lexicalstructure_keywords () =
- let val keywords = OuterKeyword.dest_keywords ()
- val commands = OuterKeyword.dest_commands ()
+ let val keywords = Keyword.dest_keywords ()
+ val commands = Keyword.dest_commands ()
fun keyword_elt kind keyword =
XML.Elem("keyword", [("word", keyword), ("category", kind)], [])
in
@@ -1013,8 +1013,8 @@
(* Extra command for embedding prover-control inside document (obscure/debug usage). *)
fun init_outer_syntax () =
- OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" OuterKeyword.control
- (OuterParse.text >> (Toplevel.no_timing oo
+ OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
+ (Parse.text >> (Toplevel.no_timing oo
(fn txt => Toplevel.imperative (fn () => process_pgip_plain txt))));
--- a/src/Pure/System/isabelle_process.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML Sat May 15 23:16:32 2010 +0200
@@ -89,9 +89,9 @@
fun init out =
(Unsynchronized.change print_mode
- (fold (update op =) [isabelle_processN, OuterKeyword.keyword_status_reportN, Pretty.symbolicN]);
+ (fold (update op =) [isabelle_processN, Keyword.keyword_status_reportN, Pretty.symbolicN]);
setup_channels out |> init_message;
- OuterKeyword.report ();
+ Keyword.report ();
Output.status (Markup.markup Markup.ready "");
Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
--- a/src/Pure/System/isar.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/System/isar.ML Sat May 15 23:16:32 2010 +0200
@@ -80,14 +80,14 @@
fun linear_undo n = edit_history n (K (find_and_undo (K true)));
fun undo n = edit_history n (fn st => fn hist =>
- find_and_undo (if Toplevel.is_proof st then K true else OuterKeyword.is_theory) hist);
+ find_and_undo (if Toplevel.is_proof st then K true else Keyword.is_theory) hist);
fun kill () = edit_history 1 (fn st => fn hist =>
find_and_undo
- (if Toplevel.is_proof st then OuterKeyword.is_theory else OuterKeyword.is_theory_begin) hist);
+ (if Toplevel.is_proof st then Keyword.is_theory else Keyword.is_theory_begin) hist);
fun kill_proof () = edit_history 1 (fn st => fn hist =>
- if Toplevel.is_proof st then find_and_undo OuterKeyword.is_theory hist
+ if Toplevel.is_proof st then find_and_undo Keyword.is_theory hist
else raise Toplevel.UNDEF);
end;
@@ -102,9 +102,9 @@
| SOME (st', NONE) =>
let
val name = Toplevel.name_of tr;
- val _ = if OuterKeyword.is_theory_begin name then init () else ();
+ val _ = if Keyword.is_theory_begin name then init () else ();
val _ =
- if OuterKeyword.is_regular name
+ if Keyword.is_regular name
then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else ();
in true end);
@@ -157,7 +157,6 @@
local
-structure P = OuterParse and K = OuterKeyword;
val op >> = Scan.>>;
in
@@ -165,33 +164,35 @@
(* global history *)
val _ =
- OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" K.control
+ OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" Keyword.control
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative init));
val _ =
- OuterSyntax.improper_command "linear_undo" "undo commands" K.control
- (Scan.optional P.nat 1 >>
+ OuterSyntax.improper_command "linear_undo" "undo commands" Keyword.control
+ (Scan.optional Parse.nat 1 >>
(fn n => Toplevel.no_timing o Toplevel.imperative (fn () => linear_undo n)));
val _ =
- OuterSyntax.improper_command "undo" "undo commands (skipping closed proofs)" K.control
- (Scan.optional P.nat 1 >>
+ OuterSyntax.improper_command "undo" "undo commands (skipping closed proofs)" Keyword.control
+ (Scan.optional Parse.nat 1 >>
(fn n => Toplevel.no_timing o Toplevel.imperative (fn () => undo n)));
val _ =
- OuterSyntax.improper_command "undos_proof" "undo commands (skipping closed proofs)" K.control
- (Scan.optional P.nat 1 >> (fn n => Toplevel.no_timing o
+ OuterSyntax.improper_command "undos_proof" "undo commands (skipping closed proofs)"
+ Keyword.control
+ (Scan.optional Parse.nat 1 >> (fn n => Toplevel.no_timing o
Toplevel.keep (fn state =>
if Toplevel.is_proof state then (undo n; print ()) else raise Toplevel.UNDEF)));
val _ =
- OuterSyntax.improper_command "cannot_undo" "partial undo -- Proof General legacy" K.control
- (P.name >>
+ OuterSyntax.improper_command "cannot_undo" "partial undo -- Proof General legacy"
+ Keyword.control
+ (Parse.name >>
(fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => undo 1)
| txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
val _ =
- OuterSyntax.improper_command "kill" "kill partial proof or theory development" K.control
+ OuterSyntax.improper_command "kill" "kill partial proof or theory development" Keyword.control
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
end;
--- a/src/Pure/System/session.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/System/session.ML Sat May 15 23:16:32 2010 +0200
@@ -48,7 +48,7 @@
(if Distribution.changelog <> "" then "\nSee also " ^ Distribution.changelog else "");
val _ =
- OuterSyntax.improper_command "welcome" "print welcome message" OuterKeyword.diag
+ OuterSyntax.improper_command "welcome" "print welcome message" Keyword.diag
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative (writeln o welcome)));
--- a/src/Pure/Thy/term_style.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Thy/term_style.ML Sat May 15 23:16:32 2010 +0200
@@ -43,7 +43,7 @@
(* style parsing *)
-fun parse_single ctxt = OuterParse.position (OuterParse.xname -- Args.parse)
+fun parse_single ctxt = Parse.position (Parse.xname -- Args.parse)
>> (fn x as ((name, _), _) => fst (Args.context_syntax "style"
(Scan.lift (the_style (ProofContext.theory_of ctxt) name))
(Args.src x) ctxt |>> (fn f => f ctxt)));
--- a/src/Pure/Thy/thy_header.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Thy/thy_header.ML Sat May 15 23:16:32 2010 +0200
@@ -15,7 +15,6 @@
struct
structure T = OuterLex;
-structure P = OuterParse;
(* keywords *)
@@ -32,23 +31,28 @@
(* header args *)
-val file_name = P.group "file name" P.name;
-val theory_name = P.group "theory name" P.name;
+val file_name = Parse.group "file name" Parse.name;
+val theory_name = Parse.group "theory name" Parse.name;
-val file = P.$$$ "(" |-- P.!!! (file_name --| P.$$$ ")") >> rpair false || file_name >> rpair true;
-val uses = Scan.optional (P.$$$ usesN |-- P.!!! (Scan.repeat1 file)) [];
+val file =
+ Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false ||
+ file_name >> rpair true;
+
+val uses = Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) [];
val args =
- theory_name -- (P.$$$ importsN |-- P.!!! (Scan.repeat1 theory_name -- uses --| P.$$$ beginN))
- >> P.triple2;
+ theory_name -- (Parse.$$$ importsN |--
+ Parse.!!! (Scan.repeat1 theory_name -- uses --| Parse.$$$ beginN))
+ >> Parse.triple2;
(* read header *)
val header =
- (P.$$$ headerN -- P.tags) |-- (P.!!! (P.doc_source -- Scan.repeat P.semicolon --
- (P.$$$ theoryN -- P.tags) |-- args)) ||
- (P.$$$ theoryN -- P.tags) |-- P.!!! args;
+ (Parse.$$$ headerN -- Parse.tags) |--
+ (Parse.!!! (Parse.doc_source -- Scan.repeat Parse.semicolon --
+ (Parse.$$$ theoryN -- Parse.tags) |-- args)) ||
+ (Parse.$$$ theoryN -- Parse.tags) |-- Parse.!!! args;
fun read pos src =
let val res =
@@ -56,7 +60,7 @@
|> 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 (P.!!! header))) NONE
+ |> Source.source T.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
|> Source.get_single;
in
(case res of SOME (x, _) => x
--- a/src/Pure/Thy/thy_output.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML Sat May 15 23:16:32 2010 +0200
@@ -37,7 +37,6 @@
struct
structure T = OuterLex;
-structure P = OuterParse;
(** global options **)
@@ -132,12 +131,16 @@
local
-val property = P.xname -- Scan.optional (P.$$$ "=" |-- P.!!! P.xname) "";
-val properties = Scan.optional (P.$$$ "[" |-- P.!!! (P.enum "," property --| P.$$$ "]")) [];
+val property =
+ Parse.xname -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.xname) "";
+
+val properties =
+ Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) [];
in
-val antiq = P.!!! (P.position P.xname -- properties -- Args.parse --| Scan.ahead P.eof)
+val antiq =
+ Parse.!!! (Parse.position Parse.xname -- properties -- Args.parse --| Scan.ahead Parse.eof)
>> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos)));
end;
@@ -249,7 +252,7 @@
val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
val (tag, tags) = tag_stack;
- val tag' = try hd (fold OuterKeyword.update_tags cmd_tags (the_list tag));
+ val tag' = try hd (fold Keyword.update_tags cmd_tags (the_list tag));
val active_tag' =
if is_some tag' then tag'
@@ -316,11 +319,11 @@
(if d = 0 then Scan.fail_with (K "Bad nesting of meta-comments") else opt_newline)
>> pair (d - 1));
-val tag = (improper -- P.$$$ "%" -- improper) |-- P.!!! (P.tag_name --| blank_end);
+val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (Parse.tag_name --| blank_end);
val locale =
- Scan.option ((P.$$$ "(" -- improper -- P.$$$ "in") |--
- P.!!! (improper |-- P.xname --| (improper -- P.$$$ ")")));
+ Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
+ Parse.!!! (improper |-- Parse.xname --| (improper -- Parse.$$$ ")")));
in
@@ -332,26 +335,27 @@
>> (fn d => (NONE, (NoToken, ("", d))));
fun markup mark mk flag = Scan.peek (fn d =>
- improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.content_of)) --
+ improper |--
+ Parse.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.content_of)) --
Scan.repeat tag --
- P.!!!! ((improper -- locale -- improper) |-- P.doc_source --| improper_end)
+ Parse.!!!! ((improper -- locale -- improper) |-- Parse.doc_source --| improper_end)
>> (fn (((tok, pos), tags), txt) =>
let val name = T.content_of tok
in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
val command = Scan.peek (fn d =>
- P.position (Scan.one (T.is_kind T.Command)) --
+ Parse.position (Scan.one (T.is_kind T.Command)) --
Scan.repeat tag
>> (fn ((tok, pos), tags) =>
let val name = T.content_of tok
in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
val cmt = Scan.peek (fn d =>
- P.$$$ "--" |-- P.!!!! (improper |-- P.doc_source)
+ Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.doc_source)
>> (fn txt => (NONE, (MarkupToken ("cmt", txt), ("", d)))));
val other = Scan.peek (fn d =>
- P.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
+ Parse.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
val token =
ignored ||
@@ -565,7 +569,7 @@
(* embedded lemma *)
-val _ = OuterKeyword.keyword "by";
+val _ = Keyword.keyword "by";
val _ = antiquotation "lemma"
(Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
--- a/src/Pure/Thy/thy_syntax.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.ML Sat May 15 23:16:32 2010 +0200
@@ -29,9 +29,7 @@
structure ThySyntax: THY_SYNTAX =
struct
-structure K = OuterKeyword;
structure T = OuterLex;
-structure P = OuterParse;
(** tokens **)
@@ -111,10 +109,11 @@
val is_whitespace = T.is_kind T.Space orf T.is_kind T.Comment;
-val body = Scan.unless (Scan.many is_whitespace -- Scan.ahead (P.command || P.eof)) P.not_eof;
+val body =
+ Scan.unless (Scan.many is_whitespace -- Scan.ahead (Parse.command || Parse.eof)) Parse.not_eof;
val span =
- Scan.ahead P.command -- P.not_eof -- Scan.repeat body
+ Scan.ahead Parse.command -- Parse.not_eof -- Scan.repeat body
>> (fn ((name, c), bs) => Span (Command name, c :: bs)) ||
Scan.many1 is_whitespace >> (fn toks => Span (Ignored, toks)) ||
Scan.repeat1 body >> (fn toks => Span (Malformed, toks));
@@ -175,13 +174,13 @@
val proof = Scan.pass 1 (Scan.repeat (Scan.depend (fn d =>
if d <= 0 then Scan.fail
else
- command_with K.is_qed_global >> pair ~1 ||
- command_with K.is_proof_goal >> pair (d + 1) ||
- (if d = 0 then Scan.fail else command_with K.is_qed >> pair (d - 1)) ||
- Scan.unless (command_with K.is_theory) (Scan.one not_eof) >> pair d)) -- Scan.state);
+ command_with Keyword.is_qed_global >> pair ~1 ||
+ command_with Keyword.is_proof_goal >> pair (d + 1) ||
+ (if d = 0 then Scan.fail else command_with Keyword.is_qed >> pair (d - 1)) ||
+ Scan.unless (command_with Keyword.is_theory) (Scan.one not_eof) >> pair d)) -- Scan.state);
val unit =
- command_with K.is_theory_goal -- proof >> (fn (a, (bs, d)) => (a, bs, d >= 0)) ||
+ command_with Keyword.is_theory_goal -- proof >> (fn (a, (bs, d)) => (a, bs, d >= 0)) ||
Scan.one not_eof >> (fn a => (a, [], true));
in
--- a/src/Pure/Tools/find_consts.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Tools/find_consts.ML Sat May 15 23:16:32 2010 +0200
@@ -148,23 +148,15 @@
Toplevel.unknown_theory o Toplevel.keep (fn state =>
find_consts (Proof.context_of (Toplevel.enter_proof_body state)) spec);
-local
-
-structure P = OuterParse and K = OuterKeyword;
-
val criterion =
- P.reserved "strict" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Strict ||
- P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Name ||
- P.xname >> Loose;
-
-in
+ Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Strict ||
+ Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
+ Parse.xname >> Loose;
val _ =
- OuterSyntax.improper_command "find_consts" "search constants by type pattern" K.diag
- (Scan.repeat ((Scan.option P.minus >> is_none) -- criterion)
+ OuterSyntax.improper_command "find_consts" "search constants by type pattern" Keyword.diag
+ (Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
>> (Toplevel.no_timing oo find_consts_cmd));
end;
-end;
-
--- a/src/Pure/Tools/find_theorems.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Tools/find_theorems.ML Sat May 15 23:16:32 2010 +0200
@@ -465,28 +465,27 @@
local
-structure P = OuterParse and K = OuterKeyword;
-
val criterion =
- P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Name ||
- P.reserved "intro" >> K Intro ||
- P.reserved "introiff" >> K IntroIff ||
- P.reserved "elim" >> K Elim ||
- P.reserved "dest" >> K Dest ||
- P.reserved "solves" >> K Solves ||
- P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> Simp ||
- P.term >> Pattern;
+ Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
+ Parse.reserved "intro" >> K Intro ||
+ Parse.reserved "introiff" >> K IntroIff ||
+ Parse.reserved "elim" >> K Elim ||
+ Parse.reserved "dest" >> K Dest ||
+ Parse.reserved "solves" >> K Solves ||
+ Parse.reserved "simp" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.term) >> Simp ||
+ Parse.term >> Pattern;
val options =
Scan.optional
- (P.$$$ "(" |--
- P.!!! (Scan.option P.nat -- Scan.optional (P.reserved "with_dups" >> K false) true
- --| P.$$$ ")")) (NONE, true);
+ (Parse.$$$ "(" |--
+ Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true
+ --| Parse.$$$ ")")) (NONE, true);
in
val _ =
- OuterSyntax.improper_command "find_theorems" "print theorems meeting specified criteria" K.diag
- (options -- Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
+ OuterSyntax.improper_command "find_theorems" "print theorems meeting specified criteria"
+ Keyword.diag
+ (options -- Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion))
>> (Toplevel.no_timing oo find_theorems_cmd));
end;
--- a/src/Pure/codegen.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/codegen.ML Sat May 15 23:16:32 2010 +0200
@@ -959,44 +959,42 @@
| _ => error ("Malformed annotation: " ^ quote s));
-structure P = OuterParse and K = OuterKeyword;
-
-val _ = List.app OuterKeyword.keyword ["attach", "file", "contains"];
+val _ = List.app Keyword.keyword ["attach", "file", "contains"];
fun strip_whitespace s = implode (fst (take_suffix (fn c => c = "\n" orelse c = " ")
(snd (take_prefix (fn c => c = "\n" orelse c = " ") (explode s))))) ^ "\n";
-val parse_attach = Scan.repeat (P.$$$ "attach" |--
- Scan.optional (P.$$$ "(" |-- P.xname --| P.$$$ ")") "" --
- (P.verbatim >> strip_whitespace));
+val parse_attach = Scan.repeat (Parse.$$$ "attach" |--
+ Scan.optional (Parse.$$$ "(" |-- Parse.xname --| Parse.$$$ ")") "" --
+ (Parse.verbatim >> strip_whitespace));
val _ =
OuterSyntax.command "types_code"
- "associate types with target language types" K.thy_decl
- (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
+ "associate types with target language types" Keyword.thy_decl
+ (Scan.repeat1 (Parse.xname --| Parse.$$$ "(" -- Parse.string --| Parse.$$$ ")" -- parse_attach) >>
(fn xs => Toplevel.theory (fn thy => fold (assoc_type o
(fn ((name, mfx), aux) => (name, (parse_mixfix
(Syntax.read_typ_global thy) mfx, aux)))) xs thy)));
val _ =
OuterSyntax.command "consts_code"
- "associate constants with target language code" K.thy_decl
+ "associate constants with target language code" Keyword.thy_decl
(Scan.repeat1
- (P.term --|
- P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
+ (Parse.term --|
+ Parse.$$$ "(" -- Parse.string --| Parse.$$$ ")" -- parse_attach) >>
(fn xs => Toplevel.theory (fn thy => fold (assoc_const o
(fn ((const, mfx), aux) =>
(const, (parse_mixfix (Syntax.read_term_global thy) mfx, aux)))) xs thy)));
fun parse_code lib =
- Scan.optional (P.$$$ "(" |-- P.enum "," P.xname --| P.$$$ ")") (!mode) --
- (if lib then Scan.optional P.name "" else P.name) --
- Scan.option (P.$$$ "file" |-- P.name) --
+ Scan.optional (Parse.$$$ "(" |-- Parse.enum "," Parse.xname --| Parse.$$$ ")") (!mode) --
+ (if lib then Scan.optional Parse.name "" else Parse.name) --
+ Scan.option (Parse.$$$ "file" |-- Parse.name) --
(if lib then Scan.succeed []
- else Scan.optional (P.$$$ "imports" |-- Scan.repeat1 P.name) []) --|
- P.$$$ "contains" --
- ( Scan.repeat1 (P.name --| P.$$$ "=" -- P.term)
- || Scan.repeat1 (P.term >> pair "")) >>
+ else Scan.optional (Parse.$$$ "imports" |-- Scan.repeat1 Parse.name) []) --|
+ Parse.$$$ "contains" --
+ ( Scan.repeat1 (Parse.name --| Parse.$$$ "=" -- Parse.term)
+ || Scan.repeat1 (Parse.term >> pair "")) >>
(fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
let
val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
@@ -1021,12 +1019,12 @@
val _ =
OuterSyntax.command "code_library"
- "generates code for terms (one structure for each theory)" K.thy_decl
+ "generates code for terms (one structure for each theory)" Keyword.thy_decl
(parse_code true);
val _ =
OuterSyntax.command "code_module"
- "generates code for terms (single structure, incremental)" K.thy_decl
+ "generates code for terms (single structure, incremental)" Keyword.thy_decl
(parse_code false);
end;