renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
authorwenzelm
Sat May 15 22:24:25 2010 +0200 (2010-05-15 ago)
changeset 36949080e85d46108
parent 36948 d2cdad45fd14
child 36950 75b8f26f2f07
renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
NEWS
src/Pure/IsaMakefile
src/Pure/Isar/keyword.ML
src/Pure/Isar/outer_keyword.ML
src/Pure/Isar/outer_parse.ML
src/Pure/Isar/parse.ML
src/Pure/ROOT.ML
     1.1 --- a/NEWS	Sat May 15 22:15:57 2010 +0200
     1.2 +++ b/NEWS	Sat May 15 22:24:25 2010 +0200
     1.3 @@ -502,6 +502,12 @@
     1.4  context actually works, but under normal circumstances one needs to
     1.5  pass the proper local context through the code!
     1.6  
     1.7 +* Renamed some important ML structures, while keeping the old names as
     1.8 +legacy aliases for some time:
     1.9 +
    1.10 +  OuterKeyword  ~>  Keyword
    1.11 +  OuterParse    ~>  Parse
    1.12 +
    1.13  
    1.14  *** System ***
    1.15  
     2.1 --- a/src/Pure/IsaMakefile	Sat May 15 22:15:57 2010 +0200
     2.2 +++ b/src/Pure/IsaMakefile	Sat May 15 22:24:25 2010 +0200
     2.3 @@ -65,27 +65,26 @@
     2.4    Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML	\
     2.5    Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML		\
     2.6    Isar/expression.ML Isar/isar_cmd.ML Isar/isar_document.ML		\
     2.7 -  Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML		\
     2.8 -  Isar/local_theory.ML Isar/locale.ML Isar/method.ML			\
     2.9 -  Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML		\
    2.10 -  Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML		\
    2.11 -  Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML		\
    2.12 -  Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML		\
    2.13 -  Isar/rule_insts.ML Isar/runtime.ML Isar/skip_proof.ML			\
    2.14 -  Isar/spec_parse.ML Isar/spec_rules.ML Isar/specification.ML		\
    2.15 -  Isar/theory_target.ML Isar/toplevel.ML Isar/typedecl.ML		\
    2.16 -  Isar/value_parse.ML ML/ml_antiquote.ML ML/ml_compiler.ML		\
    2.17 -  ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML		\
    2.18 -  ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML		\
    2.19 -  ML-Systems/install_pp_polyml.ML ML-Systems/install_pp_polyml-5.3.ML	\
    2.20 -  ML-Systems/use_context.ML Proof/extraction.ML				\
    2.21 -  Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML			\
    2.22 -  Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/pgip.ML	\
    2.23 -  ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML		\
    2.24 -  ProofGeneral/pgip_markup.ML ProofGeneral/pgip_output.ML		\
    2.25 -  ProofGeneral/pgip_parser.ML ProofGeneral/pgip_tests.ML		\
    2.26 -  ProofGeneral/pgip_types.ML ProofGeneral/preferences.ML		\
    2.27 -  ProofGeneral/proof_general_emacs.ML					\
    2.28 +  Isar/isar_syn.ML Isar/keyword.ML Isar/local_defs.ML			\
    2.29 +  Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML		\
    2.30 +  Isar/method.ML Isar/object_logic.ML Isar/obtain.ML Isar/outer_lex.ML	\
    2.31 +  Isar/outer_syntax.ML Isar/overloading.ML Isar/parse.ML Isar/proof.ML	\
    2.32 +  Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML	\
    2.33 +  Isar/rule_cases.ML Isar/rule_insts.ML Isar/runtime.ML			\
    2.34 +  Isar/skip_proof.ML Isar/spec_parse.ML Isar/spec_rules.ML		\
    2.35 +  Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML		\
    2.36 +  Isar/typedecl.ML Isar/value_parse.ML ML/ml_antiquote.ML		\
    2.37 +  ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML	\
    2.38 +  ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML		\
    2.39 +  ML/ml_thms.ML ML-Systems/install_pp_polyml.ML				\
    2.40 +  ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML		\
    2.41 +  Proof/extraction.ML Proof/proof_rewrite_rules.ML			\
    2.42 +  Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML	\
    2.43 +  ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML			\
    2.44 +  ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML		\
    2.45 +  ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML		\
    2.46 +  ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML			\
    2.47 +  ProofGeneral/preferences.ML ProofGeneral/proof_general_emacs.ML	\
    2.48    ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML	\
    2.49    Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML			\
    2.50    Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML		\
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Isar/keyword.ML	Sat May 15 22:24:25 2010 +0200
     3.3 @@ -0,0 +1,216 @@
     3.4 +(*  Title:      Pure/Isar/keyword.ML
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Isar command keyword classification and global keyword tables.
     3.8 +*)
     3.9 +
    3.10 +signature KEYWORD =
    3.11 +sig
    3.12 +  type T
    3.13 +  val kind_of: T -> string
    3.14 +  val control: T
    3.15 +  val diag: T
    3.16 +  val thy_begin: T
    3.17 +  val thy_switch: T
    3.18 +  val thy_end: T
    3.19 +  val thy_heading: T
    3.20 +  val thy_decl: T
    3.21 +  val thy_script: T
    3.22 +  val thy_goal: T
    3.23 +  val thy_schematic_goal: T
    3.24 +  val qed: T
    3.25 +  val qed_block: T
    3.26 +  val qed_global: T
    3.27 +  val prf_heading: T
    3.28 +  val prf_goal: T
    3.29 +  val prf_block: T
    3.30 +  val prf_open: T
    3.31 +  val prf_close: T
    3.32 +  val prf_chain: T
    3.33 +  val prf_decl: T
    3.34 +  val prf_asm: T
    3.35 +  val prf_asm_goal: T
    3.36 +  val prf_script: T
    3.37 +  val kinds: string list
    3.38 +  val update_tags: string -> string list -> string list
    3.39 +  val tag: string -> T -> T
    3.40 +  val tags_of: T -> string list
    3.41 +  val tag_theory: T -> T
    3.42 +  val tag_proof: T -> T
    3.43 +  val tag_ml: T -> T
    3.44 +  val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
    3.45 +  val is_keyword: string -> bool
    3.46 +  val dest_keywords: unit -> string list
    3.47 +  val dest_commands: unit -> string list
    3.48 +  val command_keyword: string -> T option
    3.49 +  val command_tags: string -> string list
    3.50 +  val keyword_status_reportN: string
    3.51 +  val report: unit -> unit
    3.52 +  val keyword: string -> unit
    3.53 +  val command: string -> T -> unit
    3.54 +  val is_diag: string -> bool
    3.55 +  val is_control: string -> bool
    3.56 +  val is_regular: string -> bool
    3.57 +  val is_theory_begin: string -> bool
    3.58 +  val is_theory: string -> bool
    3.59 +  val is_proof: string -> bool
    3.60 +  val is_theory_goal: string -> bool
    3.61 +  val is_proof_goal: string -> bool
    3.62 +  val is_schematic_goal: string -> bool
    3.63 +  val is_qed: string -> bool
    3.64 +  val is_qed_global: string -> bool
    3.65 +end;
    3.66 +
    3.67 +structure Keyword: KEYWORD =
    3.68 +struct
    3.69 +
    3.70 +(** keyword classification **)
    3.71 +
    3.72 +datatype T = Keyword of string * string list;
    3.73 +
    3.74 +fun kind s = Keyword (s, []);
    3.75 +fun kind_of (Keyword (s, _)) = s;
    3.76 +
    3.77 +
    3.78 +(* kinds *)
    3.79 +
    3.80 +val control = kind "control";
    3.81 +val diag = kind "diag";
    3.82 +val thy_begin = kind "theory-begin";
    3.83 +val thy_switch = kind "theory-switch";
    3.84 +val thy_end = kind "theory-end";
    3.85 +val thy_heading = kind "theory-heading";
    3.86 +val thy_decl = kind "theory-decl";
    3.87 +val thy_script = kind "theory-script";
    3.88 +val thy_goal = kind "theory-goal";
    3.89 +val thy_schematic_goal = kind "theory-schematic-goal";
    3.90 +val qed = kind "qed";
    3.91 +val qed_block = kind "qed-block";
    3.92 +val qed_global = kind "qed-global";
    3.93 +val prf_heading = kind "proof-heading";
    3.94 +val prf_goal = kind "proof-goal";
    3.95 +val prf_block = kind "proof-block";
    3.96 +val prf_open = kind "proof-open";
    3.97 +val prf_close = kind "proof-close";
    3.98 +val prf_chain = kind "proof-chain";
    3.99 +val prf_decl = kind "proof-decl";
   3.100 +val prf_asm = kind "proof-asm";
   3.101 +val prf_asm_goal = kind "proof-asm-goal";
   3.102 +val prf_script = kind "proof-script";
   3.103 +
   3.104 +val kinds =
   3.105 +  [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal,
   3.106 +    thy_schematic_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open,
   3.107 +    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]
   3.108 + |> map kind_of;
   3.109 +
   3.110 +
   3.111 +(* tags *)
   3.112 +
   3.113 +fun update_tags t ts = t :: remove (op = : string * string -> bool) t ts;
   3.114 +
   3.115 +fun tag t (Keyword (s, ts)) = Keyword (s, update_tags t ts);
   3.116 +fun tags_of (Keyword (_, ts)) = ts;
   3.117 +
   3.118 +val tag_theory = tag "theory";
   3.119 +val tag_proof = tag "proof";
   3.120 +val tag_ml = tag "ML";
   3.121 +
   3.122 +
   3.123 +
   3.124 +(** global keyword tables **)
   3.125 +
   3.126 +local
   3.127 +
   3.128 +val global_commands = Unsynchronized.ref (Symtab.empty: T Symtab.table);
   3.129 +val global_lexicons = Unsynchronized.ref (Scan.empty_lexicon, Scan.empty_lexicon);
   3.130 +
   3.131 +in
   3.132 +
   3.133 +fun get_commands () = ! global_commands;
   3.134 +fun get_lexicons () = ! global_lexicons;
   3.135 +
   3.136 +fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);
   3.137 +fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);
   3.138 +
   3.139 +end;
   3.140 +
   3.141 +
   3.142 +(* lookup *)
   3.143 +
   3.144 +fun is_keyword s = Scan.is_literal (#1 (get_lexicons ())) (Symbol.explode s);
   3.145 +fun dest_keywords () = sort_strings (Scan.dest_lexicon (#1 (get_lexicons ())));
   3.146 +
   3.147 +fun dest_commands () = sort_strings (Symtab.keys (get_commands ()));
   3.148 +fun command_keyword name = Symtab.lookup (get_commands ()) name;
   3.149 +fun command_tags name = these (Option.map tags_of (command_keyword name));
   3.150 +
   3.151 +
   3.152 +(* reports *)
   3.153 +
   3.154 +val keyword_status_reportN = "keyword_status_report";
   3.155 +
   3.156 +fun report_message s =
   3.157 +  (if print_mode_active keyword_status_reportN then Output.status else writeln) s;
   3.158 +
   3.159 +fun report_keyword name =
   3.160 +  report_message (Markup.markup (Markup.keyword_decl name)
   3.161 +    ("Outer syntax keyword: " ^ quote name));
   3.162 +
   3.163 +fun report_command (name, kind) =
   3.164 +  report_message (Markup.markup (Markup.command_decl name (kind_of kind))
   3.165 +    ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
   3.166 +
   3.167 +fun report () =
   3.168 +  let val (keywords, commands) = CRITICAL (fn () =>
   3.169 +    (dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
   3.170 +  in
   3.171 +    List.app report_keyword keywords;
   3.172 +    List.app report_command commands
   3.173 +  end;
   3.174 +
   3.175 +
   3.176 +(* augment tables *)
   3.177 +
   3.178 +fun keyword name =
   3.179 + (change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
   3.180 +  report_keyword name);
   3.181 +
   3.182 +fun command name kind =
   3.183 + (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
   3.184 +  change_commands (Symtab.update (name, kind));
   3.185 +  report_command (name, kind));
   3.186 +
   3.187 +
   3.188 +(* command categories *)
   3.189 +
   3.190 +fun command_category ks name =
   3.191 +  (case command_keyword name of
   3.192 +    NONE => false
   3.193 +  | SOME k => member (op = o pairself kind_of) ks k);
   3.194 +
   3.195 +val is_diag = command_category [diag];
   3.196 +val is_control = command_category [control];
   3.197 +fun is_regular name = not (is_diag name orelse is_control name);
   3.198 +
   3.199 +val is_theory_begin = command_category [thy_begin];
   3.200 +
   3.201 +val is_theory = command_category
   3.202 +  [thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal, thy_schematic_goal];
   3.203 +
   3.204 +val is_proof = command_category
   3.205 +  [qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
   3.206 +    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
   3.207 +
   3.208 +val is_theory_goal = command_category [thy_goal, thy_schematic_goal];
   3.209 +val is_proof_goal = command_category [prf_goal, prf_asm_goal];
   3.210 +val is_schematic_goal = command_category [thy_schematic_goal];
   3.211 +val is_qed = command_category [qed, qed_block];
   3.212 +val is_qed_global = command_category [qed_global];
   3.213 +
   3.214 +end;
   3.215 +
   3.216 +(*legacy alias*)
   3.217 +structure OuterKeyword = Keyword;
   3.218 +
   3.219 +
     4.1 --- a/src/Pure/Isar/outer_keyword.ML	Sat May 15 22:15:57 2010 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,211 +0,0 @@
     4.4 -(*  Title:      Pure/Isar/outer_keyword.ML
     4.5 -    Author:     Makarius
     4.6 -
     4.7 -Isar command keyword classification and global keyword tables.
     4.8 -*)
     4.9 -
    4.10 -signature OUTER_KEYWORD =
    4.11 -sig
    4.12 -  type T
    4.13 -  val kind_of: T -> string
    4.14 -  val control: T
    4.15 -  val diag: T
    4.16 -  val thy_begin: T
    4.17 -  val thy_switch: T
    4.18 -  val thy_end: T
    4.19 -  val thy_heading: T
    4.20 -  val thy_decl: T
    4.21 -  val thy_script: T
    4.22 -  val thy_goal: T
    4.23 -  val thy_schematic_goal: T
    4.24 -  val qed: T
    4.25 -  val qed_block: T
    4.26 -  val qed_global: T
    4.27 -  val prf_heading: T
    4.28 -  val prf_goal: T
    4.29 -  val prf_block: T
    4.30 -  val prf_open: T
    4.31 -  val prf_close: T
    4.32 -  val prf_chain: T
    4.33 -  val prf_decl: T
    4.34 -  val prf_asm: T
    4.35 -  val prf_asm_goal: T
    4.36 -  val prf_script: T
    4.37 -  val kinds: string list
    4.38 -  val update_tags: string -> string list -> string list
    4.39 -  val tag: string -> T -> T
    4.40 -  val tags_of: T -> string list
    4.41 -  val tag_theory: T -> T
    4.42 -  val tag_proof: T -> T
    4.43 -  val tag_ml: T -> T
    4.44 -  val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
    4.45 -  val is_keyword: string -> bool
    4.46 -  val dest_keywords: unit -> string list
    4.47 -  val dest_commands: unit -> string list
    4.48 -  val command_keyword: string -> T option
    4.49 -  val command_tags: string -> string list
    4.50 -  val keyword_status_reportN: string
    4.51 -  val report: unit -> unit
    4.52 -  val keyword: string -> unit
    4.53 -  val command: string -> T -> unit
    4.54 -  val is_diag: string -> bool
    4.55 -  val is_control: string -> bool
    4.56 -  val is_regular: string -> bool
    4.57 -  val is_theory_begin: string -> bool
    4.58 -  val is_theory: string -> bool
    4.59 -  val is_proof: string -> bool
    4.60 -  val is_theory_goal: string -> bool
    4.61 -  val is_proof_goal: string -> bool
    4.62 -  val is_schematic_goal: string -> bool
    4.63 -  val is_qed: string -> bool
    4.64 -  val is_qed_global: string -> bool
    4.65 -end;
    4.66 -
    4.67 -structure OuterKeyword: OUTER_KEYWORD =
    4.68 -struct
    4.69 -
    4.70 -(** keyword classification **)
    4.71 -
    4.72 -datatype T = Keyword of string * string list;
    4.73 -
    4.74 -fun kind s = Keyword (s, []);
    4.75 -fun kind_of (Keyword (s, _)) = s;
    4.76 -
    4.77 -
    4.78 -(* kinds *)
    4.79 -
    4.80 -val control = kind "control";
    4.81 -val diag = kind "diag";
    4.82 -val thy_begin = kind "theory-begin";
    4.83 -val thy_switch = kind "theory-switch";
    4.84 -val thy_end = kind "theory-end";
    4.85 -val thy_heading = kind "theory-heading";
    4.86 -val thy_decl = kind "theory-decl";
    4.87 -val thy_script = kind "theory-script";
    4.88 -val thy_goal = kind "theory-goal";
    4.89 -val thy_schematic_goal = kind "theory-schematic-goal";
    4.90 -val qed = kind "qed";
    4.91 -val qed_block = kind "qed-block";
    4.92 -val qed_global = kind "qed-global";
    4.93 -val prf_heading = kind "proof-heading";
    4.94 -val prf_goal = kind "proof-goal";
    4.95 -val prf_block = kind "proof-block";
    4.96 -val prf_open = kind "proof-open";
    4.97 -val prf_close = kind "proof-close";
    4.98 -val prf_chain = kind "proof-chain";
    4.99 -val prf_decl = kind "proof-decl";
   4.100 -val prf_asm = kind "proof-asm";
   4.101 -val prf_asm_goal = kind "proof-asm-goal";
   4.102 -val prf_script = kind "proof-script";
   4.103 -
   4.104 -val kinds =
   4.105 -  [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal,
   4.106 -    thy_schematic_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open,
   4.107 -    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]
   4.108 - |> map kind_of;
   4.109 -
   4.110 -
   4.111 -(* tags *)
   4.112 -
   4.113 -fun update_tags t ts = t :: remove (op = : string * string -> bool) t ts;
   4.114 -
   4.115 -fun tag t (Keyword (s, ts)) = Keyword (s, update_tags t ts);
   4.116 -fun tags_of (Keyword (_, ts)) = ts;
   4.117 -
   4.118 -val tag_theory = tag "theory";
   4.119 -val tag_proof = tag "proof";
   4.120 -val tag_ml = tag "ML";
   4.121 -
   4.122 -
   4.123 -
   4.124 -(** global keyword tables **)
   4.125 -
   4.126 -local
   4.127 -
   4.128 -val global_commands = Unsynchronized.ref (Symtab.empty: T Symtab.table);
   4.129 -val global_lexicons = Unsynchronized.ref (Scan.empty_lexicon, Scan.empty_lexicon);
   4.130 -
   4.131 -in
   4.132 -
   4.133 -fun get_commands () = ! global_commands;
   4.134 -fun get_lexicons () = ! global_lexicons;
   4.135 -
   4.136 -fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);
   4.137 -fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);
   4.138 -
   4.139 -end;
   4.140 -
   4.141 -
   4.142 -(* lookup *)
   4.143 -
   4.144 -fun is_keyword s = Scan.is_literal (#1 (get_lexicons ())) (Symbol.explode s);
   4.145 -fun dest_keywords () = sort_strings (Scan.dest_lexicon (#1 (get_lexicons ())));
   4.146 -
   4.147 -fun dest_commands () = sort_strings (Symtab.keys (get_commands ()));
   4.148 -fun command_keyword name = Symtab.lookup (get_commands ()) name;
   4.149 -fun command_tags name = these (Option.map tags_of (command_keyword name));
   4.150 -
   4.151 -
   4.152 -(* reports *)
   4.153 -
   4.154 -val keyword_status_reportN = "keyword_status_report";
   4.155 -
   4.156 -fun report_message s =
   4.157 -  (if print_mode_active keyword_status_reportN then Output.status else writeln) s;
   4.158 -
   4.159 -fun report_keyword name =
   4.160 -  report_message (Markup.markup (Markup.keyword_decl name)
   4.161 -    ("Outer syntax keyword: " ^ quote name));
   4.162 -
   4.163 -fun report_command (name, kind) =
   4.164 -  report_message (Markup.markup (Markup.command_decl name (kind_of kind))
   4.165 -    ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
   4.166 -
   4.167 -fun report () =
   4.168 -  let val (keywords, commands) = CRITICAL (fn () =>
   4.169 -    (dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
   4.170 -  in
   4.171 -    List.app report_keyword keywords;
   4.172 -    List.app report_command commands
   4.173 -  end;
   4.174 -
   4.175 -
   4.176 -(* augment tables *)
   4.177 -
   4.178 -fun keyword name =
   4.179 - (change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
   4.180 -  report_keyword name);
   4.181 -
   4.182 -fun command name kind =
   4.183 - (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
   4.184 -  change_commands (Symtab.update (name, kind));
   4.185 -  report_command (name, kind));
   4.186 -
   4.187 -
   4.188 -(* command categories *)
   4.189 -
   4.190 -fun command_category ks name =
   4.191 -  (case command_keyword name of
   4.192 -    NONE => false
   4.193 -  | SOME k => member (op = o pairself kind_of) ks k);
   4.194 -
   4.195 -val is_diag = command_category [diag];
   4.196 -val is_control = command_category [control];
   4.197 -fun is_regular name = not (is_diag name orelse is_control name);
   4.198 -
   4.199 -val is_theory_begin = command_category [thy_begin];
   4.200 -
   4.201 -val is_theory = command_category
   4.202 -  [thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal, thy_schematic_goal];
   4.203 -
   4.204 -val is_proof = command_category
   4.205 -  [qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
   4.206 -    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
   4.207 -
   4.208 -val is_theory_goal = command_category [thy_goal, thy_schematic_goal];
   4.209 -val is_proof_goal = command_category [prf_goal, prf_asm_goal];
   4.210 -val is_schematic_goal = command_category [thy_schematic_goal];
   4.211 -val is_qed = command_category [qed, qed_block];
   4.212 -val is_qed_global = command_category [qed_global];
   4.213 -
   4.214 -end;
     5.1 --- a/src/Pure/Isar/outer_parse.ML	Sat May 15 22:15:57 2010 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,343 +0,0 @@
     5.4 -(*  Title:      Pure/Isar/outer_parse.ML
     5.5 -    Author:     Markus Wenzel, TU Muenchen
     5.6 -
     5.7 -Generic parsers for Isabelle/Isar outer syntax.
     5.8 -*)
     5.9 -
    5.10 -signature OUTER_PARSE =
    5.11 -sig
    5.12 -  type token = OuterLex.token
    5.13 -  type 'a parser = token list -> 'a * token list
    5.14 -  type 'a context_parser = Context.generic * token list -> 'a * (Context.generic * token list)
    5.15 -  val group: string -> (token list -> 'a) -> token list -> 'a
    5.16 -  val !!! : (token list -> 'a) -> token list -> 'a
    5.17 -  val !!!! : (token list -> 'a) -> token list -> 'a
    5.18 -  val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
    5.19 -  val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
    5.20 -  val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
    5.21 -  val not_eof: token parser
    5.22 -  val position: (token list -> 'a * 'b) -> token list -> ('a * Position.T) * 'b
    5.23 -  val command: string parser
    5.24 -  val keyword: string parser
    5.25 -  val short_ident: string parser
    5.26 -  val long_ident: string parser
    5.27 -  val sym_ident: string parser
    5.28 -  val minus: string parser
    5.29 -  val term_var: string parser
    5.30 -  val type_ident: string parser
    5.31 -  val type_var: string parser
    5.32 -  val number: string parser
    5.33 -  val string: string parser
    5.34 -  val alt_string: string parser
    5.35 -  val verbatim: string parser
    5.36 -  val sync: string parser
    5.37 -  val eof: string parser
    5.38 -  val keyword_with: (string -> bool) -> string parser
    5.39 -  val keyword_ident_or_symbolic: string parser
    5.40 -  val $$$ : string -> string parser
    5.41 -  val reserved: string -> string parser
    5.42 -  val semicolon: string parser
    5.43 -  val underscore: string parser
    5.44 -  val maybe: 'a parser -> 'a option parser
    5.45 -  val tag_name: string parser
    5.46 -  val tags: string list parser
    5.47 -  val opt_unit: unit parser
    5.48 -  val opt_keyword: string -> bool parser
    5.49 -  val begin: string parser
    5.50 -  val opt_begin: bool parser
    5.51 -  val nat: int parser
    5.52 -  val int: int parser
    5.53 -  val enum: string -> 'a parser -> 'a list parser
    5.54 -  val enum1: string -> 'a parser -> 'a list parser
    5.55 -  val and_list: 'a parser -> 'a list parser
    5.56 -  val and_list1: 'a parser -> 'a list parser
    5.57 -  val enum': string -> 'a context_parser -> 'a list context_parser
    5.58 -  val enum1': string -> 'a context_parser -> 'a list context_parser
    5.59 -  val and_list': 'a context_parser -> 'a list context_parser
    5.60 -  val and_list1': 'a context_parser -> 'a list context_parser
    5.61 -  val list: 'a parser -> 'a list parser
    5.62 -  val list1: 'a parser -> 'a list parser
    5.63 -  val name: bstring parser
    5.64 -  val binding: binding parser
    5.65 -  val xname: xstring parser
    5.66 -  val text: string parser
    5.67 -  val path: Path.T parser
    5.68 -  val parname: string parser
    5.69 -  val parbinding: binding parser
    5.70 -  val sort: string parser
    5.71 -  val arity: (string * string list * string) parser
    5.72 -  val multi_arity: (string list * string list * string) parser
    5.73 -  val type_args: string list parser
    5.74 -  val type_args_constrained: (string * string option) list parser
    5.75 -  val typ_group: string parser
    5.76 -  val typ: string parser
    5.77 -  val mixfix: mixfix parser
    5.78 -  val mixfix': mixfix parser
    5.79 -  val opt_mixfix: mixfix parser
    5.80 -  val opt_mixfix': mixfix parser
    5.81 -  val where_: string parser
    5.82 -  val const: (string * string * mixfix) parser
    5.83 -  val const_binding: (binding * string * mixfix) parser
    5.84 -  val params: (binding * string option) list parser
    5.85 -  val simple_fixes: (binding * string option) list parser
    5.86 -  val fixes: (binding * string option * mixfix) list parser
    5.87 -  val for_fixes: (binding * string option * mixfix) list parser
    5.88 -  val for_simple_fixes: (binding * string option) list parser
    5.89 -  val ML_source: (Symbol_Pos.text * Position.T) parser
    5.90 -  val doc_source: (Symbol_Pos.text * Position.T) parser
    5.91 -  val term_group: string parser
    5.92 -  val prop_group: string parser
    5.93 -  val term: string parser
    5.94 -  val prop: string parser
    5.95 -  val propp: (string * string list) parser
    5.96 -  val termp: (string * string list) parser
    5.97 -  val target: xstring parser
    5.98 -  val opt_target: xstring option parser
    5.99 -end;
   5.100 -
   5.101 -structure OuterParse: OUTER_PARSE =
   5.102 -struct
   5.103 -
   5.104 -structure T = OuterLex;
   5.105 -type token = T.token;
   5.106 -
   5.107 -type 'a parser = token list -> 'a * token list;
   5.108 -type 'a context_parser = Context.generic * token list -> 'a * (Context.generic * token list);
   5.109 -
   5.110 -
   5.111 -(** error handling **)
   5.112 -
   5.113 -(* group atomic parsers (no cuts!) *)
   5.114 -
   5.115 -fun fail_with s = Scan.fail_with
   5.116 -  (fn [] => s ^ " expected (past end-of-file!)"
   5.117 -    | (tok :: _) =>
   5.118 -        (case T.text_of tok of
   5.119 -          (txt, "") => s ^ " expected,\nbut " ^ txt ^ T.pos_of tok ^ " was found"
   5.120 -        | (txt1, txt2) => s ^ " expected,\nbut " ^ txt1 ^ T.pos_of tok ^ " was found:\n" ^ txt2));
   5.121 -
   5.122 -fun group s scan = scan || fail_with s;
   5.123 -
   5.124 -
   5.125 -(* cut *)
   5.126 -
   5.127 -fun cut kind scan =
   5.128 -  let
   5.129 -    fun get_pos [] = " (past end-of-file!)"
   5.130 -      | get_pos (tok :: _) = T.pos_of tok;
   5.131 -
   5.132 -    fun err (toks, NONE) = kind ^ get_pos toks
   5.133 -      | err (toks, SOME msg) =
   5.134 -          if String.isPrefix kind msg then msg
   5.135 -          else kind ^ get_pos toks ^ ": " ^ msg;
   5.136 -  in Scan.!! err scan end;
   5.137 -
   5.138 -fun !!! scan = cut "Outer syntax error" scan;
   5.139 -fun !!!! scan = cut "Corrupted outer syntax in presentation" scan;
   5.140 -
   5.141 -
   5.142 -
   5.143 -(** basic parsers **)
   5.144 -
   5.145 -(* utils *)
   5.146 -
   5.147 -fun triple1 ((x, y), z) = (x, y, z);
   5.148 -fun triple2 (x, (y, z)) = (x, y, z);
   5.149 -fun triple_swap ((x, y), z) = ((x, z), y);
   5.150 -
   5.151 -
   5.152 -(* tokens *)
   5.153 -
   5.154 -fun RESET_VALUE atom = (*required for all primitive parsers*)
   5.155 -  Scan.ahead (Scan.one (K true)) -- atom >> (fn (arg, x) => (T.assign NONE arg; x));
   5.156 -
   5.157 -
   5.158 -val not_eof = RESET_VALUE (Scan.one T.not_eof);
   5.159 -
   5.160 -fun position scan = (Scan.ahead not_eof >> T.position_of) -- scan >> Library.swap;
   5.161 -fun source_position atom = Scan.ahead atom |-- not_eof >> T.source_position_of;
   5.162 -fun inner_syntax atom = Scan.ahead atom |-- not_eof >> T.source_of;
   5.163 -
   5.164 -fun kind k =
   5.165 -  group (T.str_of_kind k) (RESET_VALUE (Scan.one (T.is_kind k) >> T.content_of));
   5.166 -
   5.167 -val command = kind T.Command;
   5.168 -val keyword = kind T.Keyword;
   5.169 -val short_ident = kind T.Ident;
   5.170 -val long_ident = kind T.LongIdent;
   5.171 -val sym_ident = kind T.SymIdent;
   5.172 -val term_var = kind T.Var;
   5.173 -val type_ident = kind T.TypeIdent;
   5.174 -val type_var = kind T.TypeVar;
   5.175 -val number = kind T.Nat;
   5.176 -val string = kind T.String;
   5.177 -val alt_string = kind T.AltString;
   5.178 -val verbatim = kind T.Verbatim;
   5.179 -val sync = kind T.Sync;
   5.180 -val eof = kind T.EOF;
   5.181 -
   5.182 -fun keyword_with pred = RESET_VALUE (Scan.one (T.keyword_with pred) >> T.content_of);
   5.183 -val keyword_ident_or_symbolic = keyword_with T.ident_or_symbolic;
   5.184 -
   5.185 -fun $$$ x =
   5.186 -  group (T.str_of_kind T.Keyword ^ " " ^ quote x) (keyword_with (fn y => x = y));
   5.187 -
   5.188 -fun reserved x =
   5.189 -  group ("reserved identifier " ^ quote x)
   5.190 -    (RESET_VALUE (Scan.one (T.ident_with (fn y => x = y)) >> T.content_of));
   5.191 -
   5.192 -val semicolon = $$$ ";";
   5.193 -
   5.194 -val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;
   5.195 -val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1;
   5.196 -fun maybe scan = underscore >> K NONE || scan >> SOME;
   5.197 -
   5.198 -val nat = number >> (#1 o Library.read_int o Symbol.explode);
   5.199 -val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
   5.200 -
   5.201 -val tag_name = group "tag name" (short_ident || string);
   5.202 -val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
   5.203 -
   5.204 -val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
   5.205 -fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;
   5.206 -
   5.207 -val begin = $$$ "begin";
   5.208 -val opt_begin = Scan.optional (begin >> K true) false;
   5.209 -
   5.210 -
   5.211 -(* enumerations *)
   5.212 -
   5.213 -fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
   5.214 -fun enum sep scan = enum1 sep scan || Scan.succeed [];
   5.215 -
   5.216 -fun enum1' sep scan = scan ::: Scan.repeat (Scan.lift ($$$ sep) |-- scan);
   5.217 -fun enum' sep scan = enum1' sep scan || Scan.succeed [];
   5.218 -
   5.219 -fun and_list1 scan = enum1 "and" scan;
   5.220 -fun and_list scan = enum "and" scan;
   5.221 -
   5.222 -fun and_list1' scan = enum1' "and" scan;
   5.223 -fun and_list' scan = enum' "and" scan;
   5.224 -
   5.225 -fun list1 scan = enum1 "," scan;
   5.226 -fun list scan = enum "," scan;
   5.227 -
   5.228 -
   5.229 -(* names and text *)
   5.230 -
   5.231 -val name = group "name declaration" (short_ident || sym_ident || string || number);
   5.232 -val binding = position name >> Binding.make;
   5.233 -val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
   5.234 -val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
   5.235 -val path = group "file name/path specification" name >> Path.explode;
   5.236 -
   5.237 -val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
   5.238 -val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Binding.empty;
   5.239 -
   5.240 -
   5.241 -(* sorts and arities *)
   5.242 -
   5.243 -val sort = group "sort" (inner_syntax xname);
   5.244 -
   5.245 -val arity = xname -- ($$$ "::" |-- !!!
   5.246 -  (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
   5.247 -
   5.248 -val multi_arity = and_list1 xname -- ($$$ "::" |-- !!!
   5.249 -  (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
   5.250 -
   5.251 -
   5.252 -(* types *)
   5.253 -
   5.254 -val typ_group = group "type"
   5.255 -  (short_ident || long_ident || sym_ident || type_ident || type_var || string || number);
   5.256 -
   5.257 -val typ = inner_syntax typ_group;
   5.258 -
   5.259 -fun type_arguments arg =
   5.260 -  arg >> single ||
   5.261 -  $$$ "(" |-- !!! (list1 arg --| $$$ ")") ||
   5.262 -  Scan.succeed [];
   5.263 -
   5.264 -val type_args = type_arguments type_ident;
   5.265 -val type_args_constrained = type_arguments (type_ident -- Scan.option ($$$ "::" |-- !!! sort));
   5.266 -
   5.267 -
   5.268 -(* mixfix annotations *)
   5.269 -
   5.270 -val mfix = string --
   5.271 -  !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] --
   5.272 -    Scan.optional nat Syntax.max_pri) >> (Mixfix o triple2);
   5.273 -
   5.274 -val infx = $$$ "infix" |-- !!! (string -- nat >> Infix);
   5.275 -val infxl = $$$ "infixl" |-- !!! (string -- nat >> Infixl);
   5.276 -val infxr = $$$ "infixr" |-- !!! (string -- nat >> Infixr);
   5.277 -
   5.278 -val binder = $$$ "binder" |--
   5.279 -  !!! (string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n))))
   5.280 -  >> (Binder o triple2);
   5.281 -
   5.282 -fun annotation guard fix = $$$ "(" |-- guard (fix --| $$$ ")");
   5.283 -fun opt_annotation guard fix = Scan.optional (annotation guard fix) NoSyn;
   5.284 -
   5.285 -val mixfix = annotation !!! (mfix || binder || infxl || infxr || infx);
   5.286 -val mixfix' = annotation I (mfix || binder || infxl || infxr || infx);
   5.287 -val opt_mixfix = opt_annotation !!! (mfix || binder || infxl || infxr || infx);
   5.288 -val opt_mixfix' = opt_annotation I (mfix || binder || infxl || infxr || infx);
   5.289 -
   5.290 -
   5.291 -(* fixes *)
   5.292 -
   5.293 -val where_ = $$$ "where";
   5.294 -
   5.295 -val const = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
   5.296 -val const_binding = binding -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
   5.297 -
   5.298 -val params = Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)
   5.299 -  >> (fn (xs, T) => map (rpair T) xs);
   5.300 -
   5.301 -val simple_fixes = and_list1 params >> flat;
   5.302 -
   5.303 -val fixes =
   5.304 -  and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) ||
   5.305 -    params >> map Syntax.no_syn) >> flat;
   5.306 -
   5.307 -val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) [];
   5.308 -val for_simple_fixes = Scan.optional ($$$ "for" |-- !!! simple_fixes) [];
   5.309 -
   5.310 -
   5.311 -(* embedded source text *)
   5.312 -
   5.313 -val ML_source = source_position (group "ML source" text);
   5.314 -val doc_source = source_position (group "document source" text);
   5.315 -
   5.316 -
   5.317 -(* terms *)
   5.318 -
   5.319 -val trm = short_ident || long_ident || sym_ident || term_var || number || string;
   5.320 -
   5.321 -val term_group = group "term" trm;
   5.322 -val prop_group = group "proposition" trm;
   5.323 -
   5.324 -val term = inner_syntax term_group;
   5.325 -val prop = inner_syntax prop_group;
   5.326 -
   5.327 -
   5.328 -(* patterns *)
   5.329 -
   5.330 -val is_terms = Scan.repeat1 ($$$ "is" |-- term);
   5.331 -val is_props = Scan.repeat1 ($$$ "is" |-- prop);
   5.332 -
   5.333 -val propp = prop -- Scan.optional ($$$ "(" |-- !!! (is_props --| $$$ ")")) [];
   5.334 -val termp = term -- Scan.optional ($$$ "(" |-- !!! (is_terms --| $$$ ")")) [];
   5.335 -
   5.336 -
   5.337 -(* targets *)
   5.338 -
   5.339 -val target = ($$$ "(" -- $$$ "in") |-- !!! (xname --| $$$ ")");
   5.340 -val opt_target = Scan.option target;
   5.341 -
   5.342 -end;
   5.343 -
   5.344 -type 'a parser = 'a OuterParse.parser;
   5.345 -type 'a context_parser = 'a OuterParse.context_parser;
   5.346 -
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Pure/Isar/parse.ML	Sat May 15 22:24:25 2010 +0200
     6.3 @@ -0,0 +1,346 @@
     6.4 +(*  Title:      Pure/Isar/parse.ML
     6.5 +    Author:     Markus Wenzel, TU Muenchen
     6.6 +
     6.7 +Generic parsers for Isabelle/Isar outer syntax.
     6.8 +*)
     6.9 +
    6.10 +signature PARSE =
    6.11 +sig
    6.12 +  type token = OuterLex.token
    6.13 +  type 'a parser = token list -> 'a * token list
    6.14 +  type 'a context_parser = Context.generic * token list -> 'a * (Context.generic * token list)
    6.15 +  val group: string -> (token list -> 'a) -> token list -> 'a
    6.16 +  val !!! : (token list -> 'a) -> token list -> 'a
    6.17 +  val !!!! : (token list -> 'a) -> token list -> 'a
    6.18 +  val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
    6.19 +  val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
    6.20 +  val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
    6.21 +  val not_eof: token parser
    6.22 +  val position: (token list -> 'a * 'b) -> token list -> ('a * Position.T) * 'b
    6.23 +  val command: string parser
    6.24 +  val keyword: string parser
    6.25 +  val short_ident: string parser
    6.26 +  val long_ident: string parser
    6.27 +  val sym_ident: string parser
    6.28 +  val minus: string parser
    6.29 +  val term_var: string parser
    6.30 +  val type_ident: string parser
    6.31 +  val type_var: string parser
    6.32 +  val number: string parser
    6.33 +  val string: string parser
    6.34 +  val alt_string: string parser
    6.35 +  val verbatim: string parser
    6.36 +  val sync: string parser
    6.37 +  val eof: string parser
    6.38 +  val keyword_with: (string -> bool) -> string parser
    6.39 +  val keyword_ident_or_symbolic: string parser
    6.40 +  val $$$ : string -> string parser
    6.41 +  val reserved: string -> string parser
    6.42 +  val semicolon: string parser
    6.43 +  val underscore: string parser
    6.44 +  val maybe: 'a parser -> 'a option parser
    6.45 +  val tag_name: string parser
    6.46 +  val tags: string list parser
    6.47 +  val opt_unit: unit parser
    6.48 +  val opt_keyword: string -> bool parser
    6.49 +  val begin: string parser
    6.50 +  val opt_begin: bool parser
    6.51 +  val nat: int parser
    6.52 +  val int: int parser
    6.53 +  val enum: string -> 'a parser -> 'a list parser
    6.54 +  val enum1: string -> 'a parser -> 'a list parser
    6.55 +  val and_list: 'a parser -> 'a list parser
    6.56 +  val and_list1: 'a parser -> 'a list parser
    6.57 +  val enum': string -> 'a context_parser -> 'a list context_parser
    6.58 +  val enum1': string -> 'a context_parser -> 'a list context_parser
    6.59 +  val and_list': 'a context_parser -> 'a list context_parser
    6.60 +  val and_list1': 'a context_parser -> 'a list context_parser
    6.61 +  val list: 'a parser -> 'a list parser
    6.62 +  val list1: 'a parser -> 'a list parser
    6.63 +  val name: bstring parser
    6.64 +  val binding: binding parser
    6.65 +  val xname: xstring parser
    6.66 +  val text: string parser
    6.67 +  val path: Path.T parser
    6.68 +  val parname: string parser
    6.69 +  val parbinding: binding parser
    6.70 +  val sort: string parser
    6.71 +  val arity: (string * string list * string) parser
    6.72 +  val multi_arity: (string list * string list * string) parser
    6.73 +  val type_args: string list parser
    6.74 +  val type_args_constrained: (string * string option) list parser
    6.75 +  val typ_group: string parser
    6.76 +  val typ: string parser
    6.77 +  val mixfix: mixfix parser
    6.78 +  val mixfix': mixfix parser
    6.79 +  val opt_mixfix: mixfix parser
    6.80 +  val opt_mixfix': mixfix parser
    6.81 +  val where_: string parser
    6.82 +  val const: (string * string * mixfix) parser
    6.83 +  val const_binding: (binding * string * mixfix) parser
    6.84 +  val params: (binding * string option) list parser
    6.85 +  val simple_fixes: (binding * string option) list parser
    6.86 +  val fixes: (binding * string option * mixfix) list parser
    6.87 +  val for_fixes: (binding * string option * mixfix) list parser
    6.88 +  val for_simple_fixes: (binding * string option) list parser
    6.89 +  val ML_source: (Symbol_Pos.text * Position.T) parser
    6.90 +  val doc_source: (Symbol_Pos.text * Position.T) parser
    6.91 +  val term_group: string parser
    6.92 +  val prop_group: string parser
    6.93 +  val term: string parser
    6.94 +  val prop: string parser
    6.95 +  val propp: (string * string list) parser
    6.96 +  val termp: (string * string list) parser
    6.97 +  val target: xstring parser
    6.98 +  val opt_target: xstring option parser
    6.99 +end;
   6.100 +
   6.101 +structure Parse: PARSE =
   6.102 +struct
   6.103 +
   6.104 +structure T = OuterLex;
   6.105 +type token = T.token;
   6.106 +
   6.107 +type 'a parser = token list -> 'a * token list;
   6.108 +type 'a context_parser = Context.generic * token list -> 'a * (Context.generic * token list);
   6.109 +
   6.110 +
   6.111 +(** error handling **)
   6.112 +
   6.113 +(* group atomic parsers (no cuts!) *)
   6.114 +
   6.115 +fun fail_with s = Scan.fail_with
   6.116 +  (fn [] => s ^ " expected (past end-of-file!)"
   6.117 +    | (tok :: _) =>
   6.118 +        (case T.text_of tok of
   6.119 +          (txt, "") => s ^ " expected,\nbut " ^ txt ^ T.pos_of tok ^ " was found"
   6.120 +        | (txt1, txt2) => s ^ " expected,\nbut " ^ txt1 ^ T.pos_of tok ^ " was found:\n" ^ txt2));
   6.121 +
   6.122 +fun group s scan = scan || fail_with s;
   6.123 +
   6.124 +
   6.125 +(* cut *)
   6.126 +
   6.127 +fun cut kind scan =
   6.128 +  let
   6.129 +    fun get_pos [] = " (past end-of-file!)"
   6.130 +      | get_pos (tok :: _) = T.pos_of tok;
   6.131 +
   6.132 +    fun err (toks, NONE) = kind ^ get_pos toks
   6.133 +      | err (toks, SOME msg) =
   6.134 +          if String.isPrefix kind msg then msg
   6.135 +          else kind ^ get_pos toks ^ ": " ^ msg;
   6.136 +  in Scan.!! err scan end;
   6.137 +
   6.138 +fun !!! scan = cut "Outer syntax error" scan;
   6.139 +fun !!!! scan = cut "Corrupted outer syntax in presentation" scan;
   6.140 +
   6.141 +
   6.142 +
   6.143 +(** basic parsers **)
   6.144 +
   6.145 +(* utils *)
   6.146 +
   6.147 +fun triple1 ((x, y), z) = (x, y, z);
   6.148 +fun triple2 (x, (y, z)) = (x, y, z);
   6.149 +fun triple_swap ((x, y), z) = ((x, z), y);
   6.150 +
   6.151 +
   6.152 +(* tokens *)
   6.153 +
   6.154 +fun RESET_VALUE atom = (*required for all primitive parsers*)
   6.155 +  Scan.ahead (Scan.one (K true)) -- atom >> (fn (arg, x) => (T.assign NONE arg; x));
   6.156 +
   6.157 +
   6.158 +val not_eof = RESET_VALUE (Scan.one T.not_eof);
   6.159 +
   6.160 +fun position scan = (Scan.ahead not_eof >> T.position_of) -- scan >> Library.swap;
   6.161 +fun source_position atom = Scan.ahead atom |-- not_eof >> T.source_position_of;
   6.162 +fun inner_syntax atom = Scan.ahead atom |-- not_eof >> T.source_of;
   6.163 +
   6.164 +fun kind k =
   6.165 +  group (T.str_of_kind k) (RESET_VALUE (Scan.one (T.is_kind k) >> T.content_of));
   6.166 +
   6.167 +val command = kind T.Command;
   6.168 +val keyword = kind T.Keyword;
   6.169 +val short_ident = kind T.Ident;
   6.170 +val long_ident = kind T.LongIdent;
   6.171 +val sym_ident = kind T.SymIdent;
   6.172 +val term_var = kind T.Var;
   6.173 +val type_ident = kind T.TypeIdent;
   6.174 +val type_var = kind T.TypeVar;
   6.175 +val number = kind T.Nat;
   6.176 +val string = kind T.String;
   6.177 +val alt_string = kind T.AltString;
   6.178 +val verbatim = kind T.Verbatim;
   6.179 +val sync = kind T.Sync;
   6.180 +val eof = kind T.EOF;
   6.181 +
   6.182 +fun keyword_with pred = RESET_VALUE (Scan.one (T.keyword_with pred) >> T.content_of);
   6.183 +val keyword_ident_or_symbolic = keyword_with T.ident_or_symbolic;
   6.184 +
   6.185 +fun $$$ x =
   6.186 +  group (T.str_of_kind T.Keyword ^ " " ^ quote x) (keyword_with (fn y => x = y));
   6.187 +
   6.188 +fun reserved x =
   6.189 +  group ("reserved identifier " ^ quote x)
   6.190 +    (RESET_VALUE (Scan.one (T.ident_with (fn y => x = y)) >> T.content_of));
   6.191 +
   6.192 +val semicolon = $$$ ";";
   6.193 +
   6.194 +val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;
   6.195 +val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1;
   6.196 +fun maybe scan = underscore >> K NONE || scan >> SOME;
   6.197 +
   6.198 +val nat = number >> (#1 o Library.read_int o Symbol.explode);
   6.199 +val int = Scan.optional (minus >> K ~1) 1 -- nat >> op *;
   6.200 +
   6.201 +val tag_name = group "tag name" (short_ident || string);
   6.202 +val tags = Scan.repeat ($$$ "%" |-- !!! tag_name);
   6.203 +
   6.204 +val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
   6.205 +fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;
   6.206 +
   6.207 +val begin = $$$ "begin";
   6.208 +val opt_begin = Scan.optional (begin >> K true) false;
   6.209 +
   6.210 +
   6.211 +(* enumerations *)
   6.212 +
   6.213 +fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
   6.214 +fun enum sep scan = enum1 sep scan || Scan.succeed [];
   6.215 +
   6.216 +fun enum1' sep scan = scan ::: Scan.repeat (Scan.lift ($$$ sep) |-- scan);
   6.217 +fun enum' sep scan = enum1' sep scan || Scan.succeed [];
   6.218 +
   6.219 +fun and_list1 scan = enum1 "and" scan;
   6.220 +fun and_list scan = enum "and" scan;
   6.221 +
   6.222 +fun and_list1' scan = enum1' "and" scan;
   6.223 +fun and_list' scan = enum' "and" scan;
   6.224 +
   6.225 +fun list1 scan = enum1 "," scan;
   6.226 +fun list scan = enum "," scan;
   6.227 +
   6.228 +
   6.229 +(* names and text *)
   6.230 +
   6.231 +val name = group "name declaration" (short_ident || sym_ident || string || number);
   6.232 +val binding = position name >> Binding.make;
   6.233 +val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
   6.234 +val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
   6.235 +val path = group "file name/path specification" name >> Path.explode;
   6.236 +
   6.237 +val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
   6.238 +val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Binding.empty;
   6.239 +
   6.240 +
   6.241 +(* sorts and arities *)
   6.242 +
   6.243 +val sort = group "sort" (inner_syntax xname);
   6.244 +
   6.245 +val arity = xname -- ($$$ "::" |-- !!!
   6.246 +  (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
   6.247 +
   6.248 +val multi_arity = and_list1 xname -- ($$$ "::" |-- !!!
   6.249 +  (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
   6.250 +
   6.251 +
   6.252 +(* types *)
   6.253 +
   6.254 +val typ_group = group "type"
   6.255 +  (short_ident || long_ident || sym_ident || type_ident || type_var || string || number);
   6.256 +
   6.257 +val typ = inner_syntax typ_group;
   6.258 +
   6.259 +fun type_arguments arg =
   6.260 +  arg >> single ||
   6.261 +  $$$ "(" |-- !!! (list1 arg --| $$$ ")") ||
   6.262 +  Scan.succeed [];
   6.263 +
   6.264 +val type_args = type_arguments type_ident;
   6.265 +val type_args_constrained = type_arguments (type_ident -- Scan.option ($$$ "::" |-- !!! sort));
   6.266 +
   6.267 +
   6.268 +(* mixfix annotations *)
   6.269 +
   6.270 +val mfix = string --
   6.271 +  !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] --
   6.272 +    Scan.optional nat Syntax.max_pri) >> (Mixfix o triple2);
   6.273 +
   6.274 +val infx = $$$ "infix" |-- !!! (string -- nat >> Infix);
   6.275 +val infxl = $$$ "infixl" |-- !!! (string -- nat >> Infixl);
   6.276 +val infxr = $$$ "infixr" |-- !!! (string -- nat >> Infixr);
   6.277 +
   6.278 +val binder = $$$ "binder" |--
   6.279 +  !!! (string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n))))
   6.280 +  >> (Binder o triple2);
   6.281 +
   6.282 +fun annotation guard fix = $$$ "(" |-- guard (fix --| $$$ ")");
   6.283 +fun opt_annotation guard fix = Scan.optional (annotation guard fix) NoSyn;
   6.284 +
   6.285 +val mixfix = annotation !!! (mfix || binder || infxl || infxr || infx);
   6.286 +val mixfix' = annotation I (mfix || binder || infxl || infxr || infx);
   6.287 +val opt_mixfix = opt_annotation !!! (mfix || binder || infxl || infxr || infx);
   6.288 +val opt_mixfix' = opt_annotation I (mfix || binder || infxl || infxr || infx);
   6.289 +
   6.290 +
   6.291 +(* fixes *)
   6.292 +
   6.293 +val where_ = $$$ "where";
   6.294 +
   6.295 +val const = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
   6.296 +val const_binding = binding -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
   6.297 +
   6.298 +val params = Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)
   6.299 +  >> (fn (xs, T) => map (rpair T) xs);
   6.300 +
   6.301 +val simple_fixes = and_list1 params >> flat;
   6.302 +
   6.303 +val fixes =
   6.304 +  and_list1 (binding -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) ||
   6.305 +    params >> map Syntax.no_syn) >> flat;
   6.306 +
   6.307 +val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) [];
   6.308 +val for_simple_fixes = Scan.optional ($$$ "for" |-- !!! simple_fixes) [];
   6.309 +
   6.310 +
   6.311 +(* embedded source text *)
   6.312 +
   6.313 +val ML_source = source_position (group "ML source" text);
   6.314 +val doc_source = source_position (group "document source" text);
   6.315 +
   6.316 +
   6.317 +(* terms *)
   6.318 +
   6.319 +val trm = short_ident || long_ident || sym_ident || term_var || number || string;
   6.320 +
   6.321 +val term_group = group "term" trm;
   6.322 +val prop_group = group "proposition" trm;
   6.323 +
   6.324 +val term = inner_syntax term_group;
   6.325 +val prop = inner_syntax prop_group;
   6.326 +
   6.327 +
   6.328 +(* patterns *)
   6.329 +
   6.330 +val is_terms = Scan.repeat1 ($$$ "is" |-- term);
   6.331 +val is_props = Scan.repeat1 ($$$ "is" |-- prop);
   6.332 +
   6.333 +val propp = prop -- Scan.optional ($$$ "(" |-- !!! (is_props --| $$$ ")")) [];
   6.334 +val termp = term -- Scan.optional ($$$ "(" |-- !!! (is_terms --| $$$ ")")) [];
   6.335 +
   6.336 +
   6.337 +(* targets *)
   6.338 +
   6.339 +val target = ($$$ "(" -- $$$ "in") |-- !!! (xname --| $$$ ")");
   6.340 +val opt_target = Scan.option target;
   6.341 +
   6.342 +end;
   6.343 +
   6.344 +type 'a parser = 'a Parse.parser;
   6.345 +type 'a context_parser = 'a Parse.context_parser;
   6.346 +
   6.347 +(*legacy alias*)
   6.348 +structure OuterParse = Parse;
   6.349 +
     7.1 --- a/src/Pure/ROOT.ML	Sat May 15 22:15:57 2010 +0200
     7.2 +++ b/src/Pure/ROOT.ML	Sat May 15 22:24:25 2010 +0200
     7.3 @@ -168,8 +168,8 @@
     7.4  
     7.5  (*outer syntax*)
     7.6  use "Isar/outer_lex.ML";
     7.7 -use "Isar/outer_keyword.ML";
     7.8 -use "Isar/outer_parse.ML";
     7.9 +use "Isar/keyword.ML";
    7.10 +use "Isar/parse.ML";
    7.11  use "Isar/value_parse.ML";
    7.12  use "Isar/args.ML";
    7.13