renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
--- a/NEWS Sat May 15 22:15:57 2010 +0200
+++ b/NEWS Sat May 15 22:24:25 2010 +0200
@@ -502,6 +502,12 @@
context actually works, but under normal circumstances one needs to
pass the proper local context through the code!
+* Renamed some important ML structures, while keeping the old names as
+legacy aliases for some time:
+
+ OuterKeyword ~> Keyword
+ OuterParse ~> Parse
+
*** System ***
--- a/src/Pure/IsaMakefile Sat May 15 22:15:57 2010 +0200
+++ b/src/Pure/IsaMakefile Sat May 15 22:24:25 2010 +0200
@@ -65,27 +65,26 @@
Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML \
Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML \
Isar/expression.ML Isar/isar_cmd.ML Isar/isar_document.ML \
- Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML \
- Isar/local_theory.ML Isar/locale.ML Isar/method.ML \
- Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \
- Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \
- Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML \
- Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML \
- Isar/rule_insts.ML Isar/runtime.ML Isar/skip_proof.ML \
- Isar/spec_parse.ML Isar/spec_rules.ML Isar/specification.ML \
- Isar/theory_target.ML Isar/toplevel.ML Isar/typedecl.ML \
- Isar/value_parse.ML ML/ml_antiquote.ML ML/ml_compiler.ML \
- ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML \
- ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML \
- ML-Systems/install_pp_polyml.ML ML-Systems/install_pp_polyml-5.3.ML \
- ML-Systems/use_context.ML Proof/extraction.ML \
- Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \
- Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/pgip.ML \
- ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML \
- ProofGeneral/pgip_markup.ML ProofGeneral/pgip_output.ML \
- ProofGeneral/pgip_parser.ML ProofGeneral/pgip_tests.ML \
- ProofGeneral/pgip_types.ML ProofGeneral/preferences.ML \
- ProofGeneral/proof_general_emacs.ML \
+ Isar/isar_syn.ML Isar/keyword.ML Isar/local_defs.ML \
+ Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML \
+ Isar/method.ML Isar/object_logic.ML Isar/obtain.ML Isar/outer_lex.ML \
+ Isar/outer_syntax.ML Isar/overloading.ML Isar/parse.ML Isar/proof.ML \
+ Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \
+ Isar/rule_cases.ML Isar/rule_insts.ML Isar/runtime.ML \
+ Isar/skip_proof.ML Isar/spec_parse.ML Isar/spec_rules.ML \
+ Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML \
+ Isar/typedecl.ML Isar/value_parse.ML ML/ml_antiquote.ML \
+ ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML \
+ ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML \
+ ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \
+ ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML \
+ Proof/extraction.ML Proof/proof_rewrite_rules.ML \
+ Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \
+ ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML \
+ ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML \
+ ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML \
+ ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML \
+ ProofGeneral/preferences.ML ProofGeneral/proof_general_emacs.ML \
ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML \
Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \
Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/keyword.ML Sat May 15 22:24:25 2010 +0200
@@ -0,0 +1,216 @@
+(* Title: Pure/Isar/keyword.ML
+ Author: Makarius
+
+Isar command keyword classification and global keyword tables.
+*)
+
+signature KEYWORD =
+sig
+ type T
+ val kind_of: T -> string
+ val control: T
+ val diag: T
+ val thy_begin: T
+ val thy_switch: T
+ val thy_end: T
+ val thy_heading: T
+ val thy_decl: T
+ val thy_script: T
+ val thy_goal: T
+ val thy_schematic_goal: T
+ val qed: T
+ val qed_block: T
+ val qed_global: T
+ val prf_heading: T
+ val prf_goal: T
+ val prf_block: T
+ val prf_open: T
+ val prf_close: T
+ val prf_chain: T
+ val prf_decl: T
+ val prf_asm: T
+ val prf_asm_goal: T
+ val prf_script: T
+ val kinds: string list
+ val update_tags: string -> string list -> string list
+ val tag: string -> T -> T
+ val tags_of: T -> string list
+ val tag_theory: T -> T
+ val tag_proof: T -> T
+ val tag_ml: T -> T
+ val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
+ val is_keyword: string -> bool
+ val dest_keywords: unit -> string list
+ val dest_commands: unit -> string list
+ val command_keyword: string -> T option
+ val command_tags: string -> string list
+ val keyword_status_reportN: string
+ val report: unit -> unit
+ val keyword: string -> unit
+ val command: string -> T -> unit
+ val is_diag: string -> bool
+ val is_control: string -> bool
+ val is_regular: string -> bool
+ val is_theory_begin: string -> bool
+ val is_theory: string -> bool
+ val is_proof: string -> bool
+ val is_theory_goal: string -> bool
+ val is_proof_goal: string -> bool
+ val is_schematic_goal: string -> bool
+ val is_qed: string -> bool
+ val is_qed_global: string -> bool
+end;
+
+structure Keyword: KEYWORD =
+struct
+
+(** keyword classification **)
+
+datatype T = Keyword of string * string list;
+
+fun kind s = Keyword (s, []);
+fun kind_of (Keyword (s, _)) = s;
+
+
+(* kinds *)
+
+val control = kind "control";
+val diag = kind "diag";
+val thy_begin = kind "theory-begin";
+val thy_switch = kind "theory-switch";
+val thy_end = kind "theory-end";
+val thy_heading = kind "theory-heading";
+val thy_decl = kind "theory-decl";
+val thy_script = kind "theory-script";
+val thy_goal = kind "theory-goal";
+val thy_schematic_goal = kind "theory-schematic-goal";
+val qed = kind "qed";
+val qed_block = kind "qed-block";
+val qed_global = kind "qed-global";
+val prf_heading = kind "proof-heading";
+val prf_goal = kind "proof-goal";
+val prf_block = kind "proof-block";
+val prf_open = kind "proof-open";
+val prf_close = kind "proof-close";
+val prf_chain = kind "proof-chain";
+val prf_decl = kind "proof-decl";
+val prf_asm = kind "proof-asm";
+val prf_asm_goal = kind "proof-asm-goal";
+val prf_script = kind "proof-script";
+
+val kinds =
+ [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal,
+ thy_schematic_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open,
+ prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]
+ |> map kind_of;
+
+
+(* tags *)
+
+fun update_tags t ts = t :: remove (op = : string * string -> bool) t ts;
+
+fun tag t (Keyword (s, ts)) = Keyword (s, update_tags t ts);
+fun tags_of (Keyword (_, ts)) = ts;
+
+val tag_theory = tag "theory";
+val tag_proof = tag "proof";
+val tag_ml = tag "ML";
+
+
+
+(** global keyword tables **)
+
+local
+
+val global_commands = Unsynchronized.ref (Symtab.empty: T Symtab.table);
+val global_lexicons = Unsynchronized.ref (Scan.empty_lexicon, Scan.empty_lexicon);
+
+in
+
+fun get_commands () = ! global_commands;
+fun get_lexicons () = ! global_lexicons;
+
+fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);
+fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);
+
+end;
+
+
+(* lookup *)
+
+fun is_keyword s = Scan.is_literal (#1 (get_lexicons ())) (Symbol.explode s);
+fun dest_keywords () = sort_strings (Scan.dest_lexicon (#1 (get_lexicons ())));
+
+fun dest_commands () = sort_strings (Symtab.keys (get_commands ()));
+fun command_keyword name = Symtab.lookup (get_commands ()) name;
+fun command_tags name = these (Option.map tags_of (command_keyword name));
+
+
+(* reports *)
+
+val keyword_status_reportN = "keyword_status_report";
+
+fun report_message s =
+ (if print_mode_active keyword_status_reportN then Output.status else writeln) s;
+
+fun report_keyword name =
+ report_message (Markup.markup (Markup.keyword_decl name)
+ ("Outer syntax keyword: " ^ quote name));
+
+fun report_command (name, kind) =
+ report_message (Markup.markup (Markup.command_decl name (kind_of kind))
+ ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
+
+fun report () =
+ let val (keywords, commands) = CRITICAL (fn () =>
+ (dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
+ in
+ List.app report_keyword keywords;
+ List.app report_command commands
+ end;
+
+
+(* augment tables *)
+
+fun keyword name =
+ (change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
+ report_keyword name);
+
+fun command name kind =
+ (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
+ change_commands (Symtab.update (name, kind));
+ report_command (name, kind));
+
+
+(* command categories *)
+
+fun command_category ks name =
+ (case command_keyword name of
+ NONE => false
+ | SOME k => member (op = o pairself kind_of) ks k);
+
+val is_diag = command_category [diag];
+val is_control = command_category [control];
+fun is_regular name = not (is_diag name orelse is_control name);
+
+val is_theory_begin = command_category [thy_begin];
+
+val is_theory = command_category
+ [thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal, thy_schematic_goal];
+
+val is_proof = command_category
+ [qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
+ prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
+
+val is_theory_goal = command_category [thy_goal, thy_schematic_goal];
+val is_proof_goal = command_category [prf_goal, prf_asm_goal];
+val is_schematic_goal = command_category [thy_schematic_goal];
+val is_qed = command_category [qed, qed_block];
+val is_qed_global = command_category [qed_global];
+
+end;
+
+(*legacy alias*)
+structure OuterKeyword = Keyword;
+
+
--- a/src/Pure/Isar/outer_keyword.ML Sat May 15 22:15:57 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,211 +0,0 @@
-(* Title: Pure/Isar/outer_keyword.ML
- Author: Makarius
-
-Isar command keyword classification and global keyword tables.
-*)
-
-signature OUTER_KEYWORD =
-sig
- type T
- val kind_of: T -> string
- val control: T
- val diag: T
- val thy_begin: T
- val thy_switch: T
- val thy_end: T
- val thy_heading: T
- val thy_decl: T
- val thy_script: T
- val thy_goal: T
- val thy_schematic_goal: T
- val qed: T
- val qed_block: T
- val qed_global: T
- val prf_heading: T
- val prf_goal: T
- val prf_block: T
- val prf_open: T
- val prf_close: T
- val prf_chain: T
- val prf_decl: T
- val prf_asm: T
- val prf_asm_goal: T
- val prf_script: T
- val kinds: string list
- val update_tags: string -> string list -> string list
- val tag: string -> T -> T
- val tags_of: T -> string list
- val tag_theory: T -> T
- val tag_proof: T -> T
- val tag_ml: T -> T
- val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
- val is_keyword: string -> bool
- val dest_keywords: unit -> string list
- val dest_commands: unit -> string list
- val command_keyword: string -> T option
- val command_tags: string -> string list
- val keyword_status_reportN: string
- val report: unit -> unit
- val keyword: string -> unit
- val command: string -> T -> unit
- val is_diag: string -> bool
- val is_control: string -> bool
- val is_regular: string -> bool
- val is_theory_begin: string -> bool
- val is_theory: string -> bool
- val is_proof: string -> bool
- val is_theory_goal: string -> bool
- val is_proof_goal: string -> bool
- val is_schematic_goal: string -> bool
- val is_qed: string -> bool
- val is_qed_global: string -> bool
-end;
-
-structure OuterKeyword: OUTER_KEYWORD =
-struct
-
-(** keyword classification **)
-
-datatype T = Keyword of string * string list;
-
-fun kind s = Keyword (s, []);
-fun kind_of (Keyword (s, _)) = s;
-
-
-(* kinds *)
-
-val control = kind "control";
-val diag = kind "diag";
-val thy_begin = kind "theory-begin";
-val thy_switch = kind "theory-switch";
-val thy_end = kind "theory-end";
-val thy_heading = kind "theory-heading";
-val thy_decl = kind "theory-decl";
-val thy_script = kind "theory-script";
-val thy_goal = kind "theory-goal";
-val thy_schematic_goal = kind "theory-schematic-goal";
-val qed = kind "qed";
-val qed_block = kind "qed-block";
-val qed_global = kind "qed-global";
-val prf_heading = kind "proof-heading";
-val prf_goal = kind "proof-goal";
-val prf_block = kind "proof-block";
-val prf_open = kind "proof-open";
-val prf_close = kind "proof-close";
-val prf_chain = kind "proof-chain";
-val prf_decl = kind "proof-decl";
-val prf_asm = kind "proof-asm";
-val prf_asm_goal = kind "proof-asm-goal";
-val prf_script = kind "proof-script";
-
-val kinds =
- [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal,
- thy_schematic_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open,
- prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]
- |> map kind_of;
-
-
-(* tags *)
-
-fun update_tags t ts = t :: remove (op = : string * string -> bool) t ts;
-
-fun tag t (Keyword (s, ts)) = Keyword (s, update_tags t ts);
-fun tags_of (Keyword (_, ts)) = ts;
-
-val tag_theory = tag "theory";
-val tag_proof = tag "proof";
-val tag_ml = tag "ML";
-
-
-
-(** global keyword tables **)
-
-local
-
-val global_commands = Unsynchronized.ref (Symtab.empty: T Symtab.table);
-val global_lexicons = Unsynchronized.ref (Scan.empty_lexicon, Scan.empty_lexicon);
-
-in
-
-fun get_commands () = ! global_commands;
-fun get_lexicons () = ! global_lexicons;
-
-fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);
-fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);
-
-end;
-
-
-(* lookup *)
-
-fun is_keyword s = Scan.is_literal (#1 (get_lexicons ())) (Symbol.explode s);
-fun dest_keywords () = sort_strings (Scan.dest_lexicon (#1 (get_lexicons ())));
-
-fun dest_commands () = sort_strings (Symtab.keys (get_commands ()));
-fun command_keyword name = Symtab.lookup (get_commands ()) name;
-fun command_tags name = these (Option.map tags_of (command_keyword name));
-
-
-(* reports *)
-
-val keyword_status_reportN = "keyword_status_report";
-
-fun report_message s =
- (if print_mode_active keyword_status_reportN then Output.status else writeln) s;
-
-fun report_keyword name =
- report_message (Markup.markup (Markup.keyword_decl name)
- ("Outer syntax keyword: " ^ quote name));
-
-fun report_command (name, kind) =
- report_message (Markup.markup (Markup.command_decl name (kind_of kind))
- ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
-
-fun report () =
- let val (keywords, commands) = CRITICAL (fn () =>
- (dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
- in
- List.app report_keyword keywords;
- List.app report_command commands
- end;
-
-
-(* augment tables *)
-
-fun keyword name =
- (change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
- report_keyword name);
-
-fun command name kind =
- (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
- change_commands (Symtab.update (name, kind));
- report_command (name, kind));
-
-
-(* command categories *)
-
-fun command_category ks name =
- (case command_keyword name of
- NONE => false
- | SOME k => member (op = o pairself kind_of) ks k);
-
-val is_diag = command_category [diag];
-val is_control = command_category [control];
-fun is_regular name = not (is_diag name orelse is_control name);
-
-val is_theory_begin = command_category [thy_begin];
-
-val is_theory = command_category
- [thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal, thy_schematic_goal];
-
-val is_proof = command_category
- [qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
- prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
-
-val is_theory_goal = command_category [thy_goal, thy_schematic_goal];
-val is_proof_goal = command_category [prf_goal, prf_asm_goal];
-val is_schematic_goal = command_category [thy_schematic_goal];
-val is_qed = command_category [qed, qed_block];
-val is_qed_global = command_category [qed_global];
-
-end;
--- a/src/Pure/Isar/outer_parse.ML Sat May 15 22:15:57 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,343 +0,0 @@
-(* Title: Pure/Isar/outer_parse.ML
- Author: Markus Wenzel, TU Muenchen
-
-Generic parsers for Isabelle/Isar outer syntax.
-*)
-
-signature OUTER_PARSE =
-sig
- type token = OuterLex.token
- type 'a parser = token list -> 'a * token list
- type 'a context_parser = Context.generic * token list -> 'a * (Context.generic * token list)
- val group: string -> (token list -> 'a) -> token list -> 'a
- val !!! : (token list -> 'a) -> token list -> 'a
- val !!!! : (token list -> 'a) -> token list -> 'a
- val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
- val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
- val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
- val not_eof: token parser
- val position: (token list -> 'a * 'b) -> token list -> ('a * Position.T) * 'b
- val command: string parser
- val keyword: string parser
- val short_ident: string parser
- val long_ident: string parser
- val sym_ident: string parser
- val minus: string parser
- val term_var: string parser
- val type_ident: string parser
- val type_var: string parser
- val number: string parser
- val string: string parser
- val alt_string: string parser
- val verbatim: string parser
- val sync: string parser
- val eof: string parser
- val keyword_with: (string -> bool) -> string parser
- val keyword_ident_or_symbolic: string parser
- val $$$ : string -> string parser
- val reserved: string -> string parser
- val semicolon: string parser
- val underscore: string parser
- val maybe: 'a parser -> 'a option parser
- val tag_name: string parser
- val tags: string list parser
- val opt_unit: unit parser
- val opt_keyword: string -> bool parser
- val begin: string parser
- val opt_begin: bool parser
- val nat: int parser
- val int: int parser
- val enum: string -> 'a parser -> 'a list parser
- val enum1: string -> 'a parser -> 'a list parser
- val and_list: 'a parser -> 'a list parser
- val and_list1: 'a parser -> 'a list parser
- val enum': string -> 'a context_parser -> 'a list context_parser
- val enum1': string -> 'a context_parser -> 'a list context_parser
- val and_list': 'a context_parser -> 'a list context_parser
- val and_list1': 'a context_parser -> 'a list context_parser
- val list: 'a parser -> 'a list parser
- val list1: 'a parser -> 'a list parser
- val name: bstring parser
- val binding: binding parser
- val xname: xstring parser
- val text: string parser
- val path: Path.T parser
- val parname: string parser
- val parbinding: binding parser
- val sort: string parser
- val arity: (string * string list * string) parser
- val multi_arity: (string list * string list * string) parser
- val type_args: string list parser
- val type_args_constrained: (string * string option) list parser
- val typ_group: string parser
- val typ: string parser
- val mixfix: mixfix parser
- val mixfix': mixfix parser
- val opt_mixfix: mixfix parser
- val opt_mixfix': mixfix parser
- val where_: string parser
- val const: (string * string * mixfix) parser
- val const_binding: (binding * string * mixfix) parser
- val params: (binding * string option) list parser
- val simple_fixes: (binding * string option) list parser
- val fixes: (binding * string option * mixfix) list parser
- val for_fixes: (binding * string option * mixfix) list parser
- val for_simple_fixes: (binding * string option) list parser
- val ML_source: (Symbol_Pos.text * Position.T) parser
- val doc_source: (Symbol_Pos.text * Position.T) parser
- val term_group: string parser
- val prop_group: string parser
- val term: string parser
- val prop: string parser
- val propp: (string * string list) parser
- val termp: (string * string list) parser
- val target: xstring parser
- val opt_target: xstring option parser
-end;
-
-structure OuterParse: OUTER_PARSE =
-struct
-
-structure T = OuterLex;
-type token = T.token;
-
-type 'a parser = token list -> 'a * token list;
-type 'a context_parser = Context.generic * token list -> 'a * (Context.generic * token list);
-
-
-(** error handling **)
-
-(* group atomic parsers (no cuts!) *)
-
-fun fail_with s = Scan.fail_with
- (fn [] => s ^ " expected (past end-of-file!)"
- | (tok :: _) =>
- (case T.text_of tok of
- (txt, "") => s ^ " expected,\nbut " ^ txt ^ T.pos_of tok ^ " was found"
- | (txt1, txt2) => s ^ " expected,\nbut " ^ txt1 ^ T.pos_of tok ^ " was found:\n" ^ txt2));
-
-fun group s scan = scan || fail_with s;
-
-
-(* cut *)
-
-fun cut kind scan =
- let
- fun get_pos [] = " (past end-of-file!)"
- | get_pos (tok :: _) = T.pos_of tok;
-
- fun err (toks, NONE) = kind ^ get_pos toks
- | err (toks, SOME msg) =
- if String.isPrefix kind msg then msg
- else kind ^ get_pos toks ^ ": " ^ msg;
- in Scan.!! err scan end;
-
-fun !!! scan = cut "Outer syntax error" scan;
-fun !!!! scan = cut "Corrupted outer syntax in presentation" scan;
-
-
-
-(** basic parsers **)
-
-(* utils *)
-
-fun triple1 ((x, y), z) = (x, y, z);
-fun triple2 (x, (y, z)) = (x, y, z);
-fun triple_swap ((x, y), z) = ((x, z), y);
-
-
-(* tokens *)
-
-fun RESET_VALUE atom = (*required for all primitive parsers*)
- Scan.ahead (Scan.one (K true)) -- atom >> (fn (arg, x) => (T.assign NONE arg; x));
-
-
-val not_eof = RESET_VALUE (Scan.one T.not_eof);
-
-fun position scan = (Scan.ahead not_eof >> T.position_of) -- scan >> Library.swap;
-fun source_position atom = Scan.ahead atom |-- not_eof >> T.source_position_of;
-fun inner_syntax atom = Scan.ahead atom |-- not_eof >> T.source_of;
-
-fun kind k =
- group (T.str_of_kind k) (RESET_VALUE (Scan.one (T.is_kind k) >> T.content_of));
-
-val command = kind T.Command;
-val keyword = kind T.Keyword;
-val short_ident = kind T.Ident;
-val long_ident = kind T.LongIdent;
-val sym_ident = kind T.SymIdent;
-val term_var = kind T.Var;
-val type_ident = kind T.TypeIdent;
-val type_var = kind T.TypeVar;
-val number = kind T.Nat;
-val string = kind T.String;
-val alt_string = kind T.AltString;
-val verbatim = kind T.Verbatim;
-val sync = kind T.Sync;
-val eof = kind T.EOF;
-
-fun keyword_with pred = RESET_VALUE (Scan.one (T.keyword_with pred) >> T.content_of);
-val keyword_ident_or_symbolic = keyword_with T.ident_or_symbolic;
-
-fun $$$ x =
- group (T.str_of_kind T.Keyword ^ " " ^ quote x) (keyword_with (fn y => x = y));
-
-fun reserved x =
- group ("reserved identifier " ^ quote x)
- (RESET_VALUE (Scan.one (T.ident_with (fn y => x = y)) >> T.content_of));
-
-val semicolon = $$$ ";";
-
-val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;
-val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1;
-fun maybe scan = underscore >> K NONE || scan >> SOME;
-
-val nat = number >> (#1 o Library.read_int o Symbol.explode);
-val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
-
-val tag_name = group "tag name" (short_ident || string);
-val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
-
-val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
-fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;
-
-val begin = $$$ "begin";
-val opt_begin = Scan.optional (begin >> K true) false;
-
-
-(* enumerations *)
-
-fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
-fun enum sep scan = enum1 sep scan || Scan.succeed [];
-
-fun enum1' sep scan = scan ::: Scan.repeat (Scan.lift ($$$ sep) |-- scan);
-fun enum' sep scan = enum1' sep scan || Scan.succeed [];
-
-fun and_list1 scan = enum1 "and" scan;
-fun and_list scan = enum "and" scan;
-
-fun and_list1' scan = enum1' "and" scan;
-fun and_list' scan = enum' "and" scan;
-
-fun list1 scan = enum1 "," scan;
-fun list scan = enum "," scan;
-
-
-(* names and text *)
-
-val name = group "name declaration" (short_ident || sym_ident || string || number);
-val binding = position name >> Binding.make;
-val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
-val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
-val path = group "file name/path specification" name >> Path.explode;
-
-val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
-val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Binding.empty;
-
-
-(* sorts and arities *)
-
-val sort = group "sort" (inner_syntax xname);
-
-val arity = xname -- ($$$ "::" |-- !!!
- (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
-
-val multi_arity = and_list1 xname -- ($$$ "::" |-- !!!
- (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
-
-
-(* types *)
-
-val typ_group = group "type"
- (short_ident || long_ident || sym_ident || type_ident || type_var || string || number);
-
-val typ = inner_syntax typ_group;
-
-fun type_arguments arg =
- arg >> single ||
- $$$ "(" |-- !!! (list1 arg --| $$$ ")") ||
- Scan.succeed [];
-
-val type_args = type_arguments type_ident;
-val type_args_constrained = type_arguments (type_ident -- Scan.option ($$$ "::" |-- !!! sort));
-
-
-(* mixfix annotations *)
-
-val mfix = string --
- !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] --
- Scan.optional nat Syntax.max_pri) >> (Mixfix o triple2);
-
-val infx = $$$ "infix" |-- !!! (string -- nat >> Infix);
-val infxl = $$$ "infixl" |-- !!! (string -- nat >> Infixl);
-val infxr = $$$ "infixr" |-- !!! (string -- nat >> Infixr);
-
-val binder = $$$ "binder" |--
- !!! (string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n))))
- >> (Binder o triple2);
-
-fun annotation guard fix = $$$ "(" |-- guard (fix --| $$$ ")");
-fun opt_annotation guard fix = Scan.optional (annotation guard fix) NoSyn;
-
-val mixfix = annotation !!! (mfix || binder || infxl || infxr || infx);
-val mixfix' = annotation I (mfix || binder || infxl || infxr || infx);
-val opt_mixfix = opt_annotation !!! (mfix || binder || infxl || infxr || infx);
-val opt_mixfix' = opt_annotation I (mfix || binder || infxl || infxr || infx);
-
-
-(* fixes *)
-
-val where_ = $$$ "where";
-
-val const = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
-val const_binding = binding -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
-
-val params = Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)
- >> (fn (xs, T) => map (rpair T) xs);
-
-val simple_fixes = and_list1 params >> flat;
-
-val fixes =
- and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) ||
- params >> map Syntax.no_syn) >> flat;
-
-val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) [];
-val for_simple_fixes = Scan.optional ($$$ "for" |-- !!! simple_fixes) [];
-
-
-(* embedded source text *)
-
-val ML_source = source_position (group "ML source" text);
-val doc_source = source_position (group "document source" text);
-
-
-(* terms *)
-
-val trm = short_ident || long_ident || sym_ident || term_var || number || string;
-
-val term_group = group "term" trm;
-val prop_group = group "proposition" trm;
-
-val term = inner_syntax term_group;
-val prop = inner_syntax prop_group;
-
-
-(* patterns *)
-
-val is_terms = Scan.repeat1 ($$$ "is" |-- term);
-val is_props = Scan.repeat1 ($$$ "is" |-- prop);
-
-val propp = prop -- Scan.optional ($$$ "(" |-- !!! (is_props --| $$$ ")")) [];
-val termp = term -- Scan.optional ($$$ "(" |-- !!! (is_terms --| $$$ ")")) [];
-
-
-(* targets *)
-
-val target = ($$$ "(" -- $$$ "in") |-- !!! (xname --| $$$ ")");
-val opt_target = Scan.option target;
-
-end;
-
-type 'a parser = 'a OuterParse.parser;
-type 'a context_parser = 'a OuterParse.context_parser;
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/parse.ML Sat May 15 22:24:25 2010 +0200
@@ -0,0 +1,346 @@
+(* Title: Pure/Isar/parse.ML
+ Author: Markus Wenzel, TU Muenchen
+
+Generic parsers for Isabelle/Isar outer syntax.
+*)
+
+signature PARSE =
+sig
+ type token = OuterLex.token
+ type 'a parser = token list -> 'a * token list
+ type 'a context_parser = Context.generic * token list -> 'a * (Context.generic * token list)
+ val group: string -> (token list -> 'a) -> token list -> 'a
+ val !!! : (token list -> 'a) -> token list -> 'a
+ val !!!! : (token list -> 'a) -> token list -> 'a
+ val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
+ val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
+ val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
+ val not_eof: token parser
+ val position: (token list -> 'a * 'b) -> token list -> ('a * Position.T) * 'b
+ val command: string parser
+ val keyword: string parser
+ val short_ident: string parser
+ val long_ident: string parser
+ val sym_ident: string parser
+ val minus: string parser
+ val term_var: string parser
+ val type_ident: string parser
+ val type_var: string parser
+ val number: string parser
+ val string: string parser
+ val alt_string: string parser
+ val verbatim: string parser
+ val sync: string parser
+ val eof: string parser
+ val keyword_with: (string -> bool) -> string parser
+ val keyword_ident_or_symbolic: string parser
+ val $$$ : string -> string parser
+ val reserved: string -> string parser
+ val semicolon: string parser
+ val underscore: string parser
+ val maybe: 'a parser -> 'a option parser
+ val tag_name: string parser
+ val tags: string list parser
+ val opt_unit: unit parser
+ val opt_keyword: string -> bool parser
+ val begin: string parser
+ val opt_begin: bool parser
+ val nat: int parser
+ val int: int parser
+ val enum: string -> 'a parser -> 'a list parser
+ val enum1: string -> 'a parser -> 'a list parser
+ val and_list: 'a parser -> 'a list parser
+ val and_list1: 'a parser -> 'a list parser
+ val enum': string -> 'a context_parser -> 'a list context_parser
+ val enum1': string -> 'a context_parser -> 'a list context_parser
+ val and_list': 'a context_parser -> 'a list context_parser
+ val and_list1': 'a context_parser -> 'a list context_parser
+ val list: 'a parser -> 'a list parser
+ val list1: 'a parser -> 'a list parser
+ val name: bstring parser
+ val binding: binding parser
+ val xname: xstring parser
+ val text: string parser
+ val path: Path.T parser
+ val parname: string parser
+ val parbinding: binding parser
+ val sort: string parser
+ val arity: (string * string list * string) parser
+ val multi_arity: (string list * string list * string) parser
+ val type_args: string list parser
+ val type_args_constrained: (string * string option) list parser
+ val typ_group: string parser
+ val typ: string parser
+ val mixfix: mixfix parser
+ val mixfix': mixfix parser
+ val opt_mixfix: mixfix parser
+ val opt_mixfix': mixfix parser
+ val where_: string parser
+ val const: (string * string * mixfix) parser
+ val const_binding: (binding * string * mixfix) parser
+ val params: (binding * string option) list parser
+ val simple_fixes: (binding * string option) list parser
+ val fixes: (binding * string option * mixfix) list parser
+ val for_fixes: (binding * string option * mixfix) list parser
+ val for_simple_fixes: (binding * string option) list parser
+ val ML_source: (Symbol_Pos.text * Position.T) parser
+ val doc_source: (Symbol_Pos.text * Position.T) parser
+ val term_group: string parser
+ val prop_group: string parser
+ val term: string parser
+ val prop: string parser
+ val propp: (string * string list) parser
+ val termp: (string * string list) parser
+ val target: xstring parser
+ val opt_target: xstring option parser
+end;
+
+structure Parse: PARSE =
+struct
+
+structure T = OuterLex;
+type token = T.token;
+
+type 'a parser = token list -> 'a * token list;
+type 'a context_parser = Context.generic * token list -> 'a * (Context.generic * token list);
+
+
+(** error handling **)
+
+(* group atomic parsers (no cuts!) *)
+
+fun fail_with s = Scan.fail_with
+ (fn [] => s ^ " expected (past end-of-file!)"
+ | (tok :: _) =>
+ (case T.text_of tok of
+ (txt, "") => s ^ " expected,\nbut " ^ txt ^ T.pos_of tok ^ " was found"
+ | (txt1, txt2) => s ^ " expected,\nbut " ^ txt1 ^ T.pos_of tok ^ " was found:\n" ^ txt2));
+
+fun group s scan = scan || fail_with s;
+
+
+(* cut *)
+
+fun cut kind scan =
+ let
+ fun get_pos [] = " (past end-of-file!)"
+ | get_pos (tok :: _) = T.pos_of tok;
+
+ fun err (toks, NONE) = kind ^ get_pos toks
+ | err (toks, SOME msg) =
+ if String.isPrefix kind msg then msg
+ else kind ^ get_pos toks ^ ": " ^ msg;
+ in Scan.!! err scan end;
+
+fun !!! scan = cut "Outer syntax error" scan;
+fun !!!! scan = cut "Corrupted outer syntax in presentation" scan;
+
+
+
+(** basic parsers **)
+
+(* utils *)
+
+fun triple1 ((x, y), z) = (x, y, z);
+fun triple2 (x, (y, z)) = (x, y, z);
+fun triple_swap ((x, y), z) = ((x, z), y);
+
+
+(* tokens *)
+
+fun RESET_VALUE atom = (*required for all primitive parsers*)
+ Scan.ahead (Scan.one (K true)) -- atom >> (fn (arg, x) => (T.assign NONE arg; x));
+
+
+val not_eof = RESET_VALUE (Scan.one T.not_eof);
+
+fun position scan = (Scan.ahead not_eof >> T.position_of) -- scan >> Library.swap;
+fun source_position atom = Scan.ahead atom |-- not_eof >> T.source_position_of;
+fun inner_syntax atom = Scan.ahead atom |-- not_eof >> T.source_of;
+
+fun kind k =
+ group (T.str_of_kind k) (RESET_VALUE (Scan.one (T.is_kind k) >> T.content_of));
+
+val command = kind T.Command;
+val keyword = kind T.Keyword;
+val short_ident = kind T.Ident;
+val long_ident = kind T.LongIdent;
+val sym_ident = kind T.SymIdent;
+val term_var = kind T.Var;
+val type_ident = kind T.TypeIdent;
+val type_var = kind T.TypeVar;
+val number = kind T.Nat;
+val string = kind T.String;
+val alt_string = kind T.AltString;
+val verbatim = kind T.Verbatim;
+val sync = kind T.Sync;
+val eof = kind T.EOF;
+
+fun keyword_with pred = RESET_VALUE (Scan.one (T.keyword_with pred) >> T.content_of);
+val keyword_ident_or_symbolic = keyword_with T.ident_or_symbolic;
+
+fun $$$ x =
+ group (T.str_of_kind T.Keyword ^ " " ^ quote x) (keyword_with (fn y => x = y));
+
+fun reserved x =
+ group ("reserved identifier " ^ quote x)
+ (RESET_VALUE (Scan.one (T.ident_with (fn y => x = y)) >> T.content_of));
+
+val semicolon = $$$ ";";
+
+val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;
+val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1;
+fun maybe scan = underscore >> K NONE || scan >> SOME;
+
+val nat = number >> (#1 o Library.read_int o Symbol.explode);
+val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
+
+val tag_name = group "tag name" (short_ident || string);
+val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
+
+val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
+fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;
+
+val begin = $$$ "begin";
+val opt_begin = Scan.optional (begin >> K true) false;
+
+
+(* enumerations *)
+
+fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
+fun enum sep scan = enum1 sep scan || Scan.succeed [];
+
+fun enum1' sep scan = scan ::: Scan.repeat (Scan.lift ($$$ sep) |-- scan);
+fun enum' sep scan = enum1' sep scan || Scan.succeed [];
+
+fun and_list1 scan = enum1 "and" scan;
+fun and_list scan = enum "and" scan;
+
+fun and_list1' scan = enum1' "and" scan;
+fun and_list' scan = enum' "and" scan;
+
+fun list1 scan = enum1 "," scan;
+fun list scan = enum "," scan;
+
+
+(* names and text *)
+
+val name = group "name declaration" (short_ident || sym_ident || string || number);
+val binding = position name >> Binding.make;
+val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
+val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
+val path = group "file name/path specification" name >> Path.explode;
+
+val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
+val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Binding.empty;
+
+
+(* sorts and arities *)
+
+val sort = group "sort" (inner_syntax xname);
+
+val arity = xname -- ($$$ "::" |-- !!!
+ (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
+
+val multi_arity = and_list1 xname -- ($$$ "::" |-- !!!
+ (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
+
+
+(* types *)
+
+val typ_group = group "type"
+ (short_ident || long_ident || sym_ident || type_ident || type_var || string || number);
+
+val typ = inner_syntax typ_group;
+
+fun type_arguments arg =
+ arg >> single ||
+ $$$ "(" |-- !!! (list1 arg --| $$$ ")") ||
+ Scan.succeed [];
+
+val type_args = type_arguments type_ident;
+val type_args_constrained = type_arguments (type_ident -- Scan.option ($$$ "::" |-- !!! sort));
+
+
+(* mixfix annotations *)
+
+val mfix = string --
+ !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] --
+ Scan.optional nat Syntax.max_pri) >> (Mixfix o triple2);
+
+val infx = $$$ "infix" |-- !!! (string -- nat >> Infix);
+val infxl = $$$ "infixl" |-- !!! (string -- nat >> Infixl);
+val infxr = $$$ "infixr" |-- !!! (string -- nat >> Infixr);
+
+val binder = $$$ "binder" |--
+ !!! (string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n))))
+ >> (Binder o triple2);
+
+fun annotation guard fix = $$$ "(" |-- guard (fix --| $$$ ")");
+fun opt_annotation guard fix = Scan.optional (annotation guard fix) NoSyn;
+
+val mixfix = annotation !!! (mfix || binder || infxl || infxr || infx);
+val mixfix' = annotation I (mfix || binder || infxl || infxr || infx);
+val opt_mixfix = opt_annotation !!! (mfix || binder || infxl || infxr || infx);
+val opt_mixfix' = opt_annotation I (mfix || binder || infxl || infxr || infx);
+
+
+(* fixes *)
+
+val where_ = $$$ "where";
+
+val const = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
+val const_binding = binding -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
+
+val params = Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)
+ >> (fn (xs, T) => map (rpair T) xs);
+
+val simple_fixes = and_list1 params >> flat;
+
+val fixes =
+ and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) ||
+ params >> map Syntax.no_syn) >> flat;
+
+val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) [];
+val for_simple_fixes = Scan.optional ($$$ "for" |-- !!! simple_fixes) [];
+
+
+(* embedded source text *)
+
+val ML_source = source_position (group "ML source" text);
+val doc_source = source_position (group "document source" text);
+
+
+(* terms *)
+
+val trm = short_ident || long_ident || sym_ident || term_var || number || string;
+
+val term_group = group "term" trm;
+val prop_group = group "proposition" trm;
+
+val term = inner_syntax term_group;
+val prop = inner_syntax prop_group;
+
+
+(* patterns *)
+
+val is_terms = Scan.repeat1 ($$$ "is" |-- term);
+val is_props = Scan.repeat1 ($$$ "is" |-- prop);
+
+val propp = prop -- Scan.optional ($$$ "(" |-- !!! (is_props --| $$$ ")")) [];
+val termp = term -- Scan.optional ($$$ "(" |-- !!! (is_terms --| $$$ ")")) [];
+
+
+(* targets *)
+
+val target = ($$$ "(" -- $$$ "in") |-- !!! (xname --| $$$ ")");
+val opt_target = Scan.option target;
+
+end;
+
+type 'a parser = 'a Parse.parser;
+type 'a context_parser = 'a Parse.context_parser;
+
+(*legacy alias*)
+structure OuterParse = Parse;
+
--- a/src/Pure/ROOT.ML Sat May 15 22:15:57 2010 +0200
+++ b/src/Pure/ROOT.ML Sat May 15 22:24:25 2010 +0200
@@ -168,8 +168,8 @@
(*outer syntax*)
use "Isar/outer_lex.ML";
-use "Isar/outer_keyword.ML";
-use "Isar/outer_parse.ML";
+use "Isar/keyword.ML";
+use "Isar/parse.ML";
use "Isar/value_parse.ML";
use "Isar/args.ML";