# HG changeset patch
# User wenzelm
# Date 1273955065 -7200
# Node ID 080e85d46108b4a1f2546586fe5f2e70d3336262
# Parent  d2cdad45fd1489addb4c6a6e540f560861aa46f1
renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;

diff -r d2cdad45fd14 -r 080e85d46108 NEWS
--- 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 ***
 
diff -r d2cdad45fd14 -r 080e85d46108 src/Pure/IsaMakefile
--- 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		\
diff -r d2cdad45fd14 -r 080e85d46108 src/Pure/Isar/keyword.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;
+
+
diff -r d2cdad45fd14 -r 080e85d46108 src/Pure/Isar/outer_keyword.ML
--- 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;
diff -r d2cdad45fd14 -r 080e85d46108 src/Pure/Isar/outer_parse.ML
--- 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;
-
diff -r d2cdad45fd14 -r 080e85d46108 src/Pure/Isar/parse.ML
--- /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;
+
diff -r d2cdad45fd14 -r 080e85d46108 src/Pure/ROOT.ML
--- 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";