# HG changeset patch
# User wenzelm
# Date 1214408312 -7200
# Node ID 71c4dd53d4cbcf1af3daa6876352875f5f464755
# Parent  8adeff7fd4bc9e317594f2acc326cb70efa6af0f
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;

diff -r 8adeff7fd4bc -r 71c4dd53d4cb doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Wed Jun 25 14:54:45 2008 +0200
+++ b/doc-src/antiquote_setup.ML	Wed Jun 25 17:38:32 2008 +0200
@@ -190,9 +190,9 @@
 
 val _ = O.add_commands
  (entity_antiqs no_check "" "syntax" @
-  entity_antiqs (K (is_some o OuterSyntax.command_keyword)) "isacommand" "command" @
-  entity_antiqs (K OuterSyntax.is_keyword) "isakeyword" "keyword" @
-  entity_antiqs (K OuterSyntax.is_keyword) "isakeyword" "element" @
+  entity_antiqs (K (is_some o OuterKeyword.command_keyword)) "isacommand" "command" @
+  entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "keyword" @
+  entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "element" @
   entity_antiqs (thy_check Method.intern Method.defined) "" "method" @
   entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute" @
   entity_antiqs no_check "" "fact" @
diff -r 8adeff7fd4bc -r 71c4dd53d4cb src/HOL/Import/import_syntax.ML
--- a/src/HOL/Import/import_syntax.ML	Wed Jun 25 14:54:45 2008 +0200
+++ b/src/HOL/Import/import_syntax.ML	Wed Jun 25 17:38:32 2008 +0200
@@ -223,7 +223,7 @@
 val append_dump = (P.verbatim || P.string) >> add_dump
 
 fun setup () =
-  (OuterSyntax.keywords[">"];
+  (OuterKeyword.keyword ">";
    OuterSyntax.command "import_segment"
 		       "Set import segment name"
 		       K.thy_decl (import_segment >> Toplevel.theory);
diff -r 8adeff7fd4bc -r 71c4dd53d4cb src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Wed Jun 25 14:54:45 2008 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Wed Jun 25 17:38:32 2008 +0200
@@ -190,7 +190,7 @@
   else Syntax.literal c
 
 fun quotename c =
-  if Syntax.is_identifier c andalso not (OuterSyntax.is_keyword c) then c else quote c
+  if Syntax.is_identifier c andalso not (OuterKeyword.is_keyword c) then c else quote c
 
 fun simple_smart_string_of_cterm ct =
     let
diff -r 8adeff7fd4bc -r 71c4dd53d4cb src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Wed Jun 25 14:54:45 2008 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Jun 25 17:38:32 2008 +0200
@@ -668,7 +668,7 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-val _ = OuterSyntax.keywords ["avoids"];
+val _ = OuterKeyword.keyword "avoids";
 
 val _ =
   OuterSyntax.command "nominal_inductive"
diff -r 8adeff7fd4bc -r 71c4dd53d4cb src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Jun 25 14:54:45 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Jun 25 17:38:32 2008 +0200
@@ -193,7 +193,7 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-val _ = OuterSyntax.keywords ["otherwise"];
+val _ = OuterKeyword.keyword "otherwise";
 
 val _ =
   OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal
diff -r 8adeff7fd4bc -r 71c4dd53d4cb src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Wed Jun 25 14:54:45 2008 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Wed Jun 25 17:38:32 2008 +0200
@@ -932,7 +932,7 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-val _ = OuterSyntax.keywords ["monos"];
+val _ = OuterKeyword.keyword "monos";
 
 fun flatten_specification specs = specs |> maps
   (fn (a, (concl, [])) => concl |> map
diff -r 8adeff7fd4bc -r 71c4dd53d4cb src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Wed Jun 25 14:54:45 2008 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Wed Jun 25 17:38:32 2008 +0200
@@ -291,7 +291,7 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-val _ = OuterSyntax.keywords ["permissive", "congs", "hints"];
+val _ = List.app OuterKeyword.keyword ["permissive", "congs", "hints"];
 
 val hints =
   P.$$$ "(" |-- P.!!! (P.position (P.$$$ "hints" -- P.arguments) --| P.$$$ ")") >> Args.src;
diff -r 8adeff7fd4bc -r 71c4dd53d4cb src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Wed Jun 25 14:54:45 2008 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Wed Jun 25 17:38:32 2008 +0200
@@ -260,7 +260,7 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-val _ = OuterSyntax.keywords ["morphisms"];
+val _ = OuterKeyword.keyword "morphisms";
 
 val typedef_decl =
   Scan.optional (P.$$$ "(" |--
diff -r 8adeff7fd4bc -r 71c4dd53d4cb src/HOLCF/IOA/meta_theory/ioa_package.ML
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Wed Jun 25 14:54:45 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Wed Jun 25 17:38:32 2008 +0200
@@ -485,7 +485,7 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-val _ = OuterSyntax.keywords ["signature", "actions", "inputs",
+val _ = List.app OuterKeyword.keyword ["signature", "actions", "inputs",
   "outputs", "internals", "states", "initially", "transitions", "pre",
   "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to",
   "rename"];
diff -r 8adeff7fd4bc -r 71c4dd53d4cb src/HOLCF/Tools/domain/domain_extender.ML
--- a/src/HOLCF/Tools/domain/domain_extender.ML	Wed Jun 25 14:54:45 2008 +0200
+++ b/src/HOLCF/Tools/domain/domain_extender.ML	Wed Jun 25 17:38:32 2008 +0200
@@ -146,7 +146,7 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-val _ = OuterSyntax.keywords ["lazy"];
+val _ = OuterKeyword.keyword "lazy";
 
 val dest_decl =
   P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false --
diff -r 8adeff7fd4bc -r 71c4dd53d4cb src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Jun 25 14:54:45 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Jun 25 17:38:32 2008 +0200
@@ -16,7 +16,7 @@
 (*keep keywords consistent with the parsers, otherwise be prepared for
   unexpected errors*)
 
-val _ = OuterSyntax.keywords
+val _ = List.app OuterKeyword.keyword
  ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
   "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
   "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
diff -r 8adeff7fd4bc -r 71c4dd53d4cb src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed Jun 25 14:54:45 2008 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Jun 25 17:38:32 2008 +0200
@@ -2,19 +2,16 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-The global Isabelle/Isar outer syntax. Note: the syntax for files is
-statically determined at the very beginning; for interactive processing
-it may change dynamically.
+The global Isabelle/Isar outer syntax.
+
+Note: the syntax for files is statically determined at the very
+beginning; for interactive processing it may change dynamically.
 *)
 
 signature OUTER_SYNTAX =
 sig
   type parser_fn = OuterLex.token list ->
     (Toplevel.transition -> Toplevel.transition) * OuterLex.token list
-  val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
-  val command_keyword: string -> OuterKeyword.T option
-  val is_keyword: string -> bool
-  val keywords: string list -> unit
   val command: string -> string -> OuterKeyword.T -> parser_fn -> unit
   val markup_command: ThyOutput.markup -> string -> string -> OuterKeyword.T -> parser_fn -> unit
   val improper_command: string -> string -> OuterKeyword.T -> parser_fn -> unit
@@ -24,11 +21,7 @@
     (OuterParse.token list -> (bool -> local_theory -> Proof.state) * OuterLex.token list) -> unit
   val local_theory_to_proof: string -> string -> OuterKeyword.T ->
     (OuterParse.token list -> (local_theory -> Proof.state) * OuterLex.token list) -> unit
-  val dest_keywords: unit -> string list
-  val dest_parsers: unit -> (string * string * string * bool) list
   val print_outer_syntax: unit -> unit
-  val report: unit -> unit
-  val check_text: string * Position.T -> Toplevel.node option -> unit
   val scan: string -> OuterLex.token list
   val parse: Position.T -> string -> Toplevel.transition list
   val process_file: Path.T -> theory -> theory
@@ -46,30 +39,18 @@
 
 (** outer syntax **)
 
-(* diagnostics *)
-
-fun report_keyword name =
-  Pretty.mark (Markup.keyword_decl name)
-    (Pretty.str ("Outer syntax keyword: " ^ quote name));
-
-fun report_command name kind =
-  Pretty.mark (Markup.command_decl name kind)
-    (Pretty.str ("Outer syntax command: " ^ quote name ^ " (" ^ kind ^ ")"));
-
-
 (* parsers *)
 
 type parser_fn = T.token list -> (Toplevel.transition -> Toplevel.transition) * T.token list;
 
 datatype parser = Parser of
  {comment: string,
-  kind: OuterKeyword.T,
   markup: ThyOutput.markup option,
   int_only: bool,
   parse: parser_fn};
 
-fun make_parser comment kind markup int_only parse =
-  Parser {comment = comment, kind = kind, markup = markup, int_only = int_only, parse = parse};
+fun make_parser comment markup int_only parse =
+  Parser {comment = comment, markup = markup, int_only = int_only, parse = parse};
 
 
 (* parse command *)
@@ -103,17 +84,9 @@
 
 local
 
-val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon);
 val global_parsers = ref (Symtab.empty: parser Symtab.table);
 val global_markups = ref ([]: (string * ThyOutput.markup) list);
 
-fun change_lexicons f = CRITICAL (fn () =>
-  let val lexs = f (! global_lexicons) in
-    (case (op inter_string) (pairself Scan.dest_lexicon lexs) of
-      [] => global_lexicons := lexs
-    | bads => error ("Clash of outer syntax commands and keywords: " ^ commas_quote bads))
-  end);
-
 fun change_parsers f = CRITICAL (fn () =>
  (change global_parsers f;
   global_markups :=
@@ -124,44 +97,30 @@
 
 (* access current syntax *)
 
-fun get_lexicons () = CRITICAL (fn () => ! global_lexicons);
 fun get_parsers () = CRITICAL (fn () => ! global_parsers);
 fun get_markups () = CRITICAL (fn () => ! global_markups);
 
 fun get_parser () = Symtab.lookup (get_parsers ());
 
-fun command_keyword name =
-  (case Symtab.lookup (get_parsers ()) name of
-    SOME (Parser {kind, ...}) => SOME kind
-  | NONE => NONE);
-
-fun command_tags name = these (Option.map OuterKeyword.tags_of (command_keyword name));
-
 fun is_markup kind name = AList.lookup (op =) (get_markups ()) name = SOME kind;
 
 
 (* augment syntax *)
 
-fun keywords names =
- (change_lexicons (apfst (Scan.extend_lexicon (map Symbol.explode names)));
-  List.app (Pretty.writeln o report_keyword) names);
-
-
-fun add_parser (name, parser as Parser {kind, ...}) =
- (if not (Symtab.defined (get_parsers ()) name) then ()
+fun add_parser name kind parser = CRITICAL (fn () =>
+ (OuterKeyword.command name kind;
+  if not (Symtab.defined (get_parsers ()) name) then ()
   else warning ("Redefining outer syntax command " ^ quote name);
-  change_parsers (Symtab.update (name, parser));
-  change_lexicons (apsnd (Scan.extend_lexicon [Symbol.explode name]));
-  Pretty.writeln (report_command name (OuterKeyword.kind_of kind)));
+  change_parsers (Symtab.update (name, parser))));
 
 fun command name comment kind parse =
-  add_parser (name, make_parser comment kind NONE false parse);
+  add_parser name kind (make_parser comment NONE false parse);
 
 fun markup_command markup name comment kind parse =
-  add_parser (name, make_parser comment kind (SOME markup) false parse);
+  add_parser name kind (make_parser comment (SOME markup) false parse);
 
 fun improper_command name comment kind parse =
-  add_parser (name, make_parser comment kind NONE true parse);
+  add_parser name kind (make_parser comment NONE true parse);
 
 end;
 
@@ -179,31 +138,22 @@
 
 (* inspect syntax *)
 
-fun is_keyword s = Scan.is_literal (#1 (get_lexicons ())) (Symbol.explode s);
-fun dest_keywords () = Scan.dest_lexicon (#1 (get_lexicons ()));
-
 fun dest_parsers () =
   get_parsers () |> Symtab.dest |> sort_wrt #1
-  |> map (fn (name, Parser {comment, kind, int_only, ...}) =>
-    (name, comment, OuterKeyword.kind_of kind, int_only));
+  |> map (fn (name, Parser {comment, int_only, ...}) => (name, comment, int_only));
 
 fun print_outer_syntax () =
   let
-    fun pretty_cmd (name, comment, _, _) =
+    fun pretty_cmd (name, comment, _) =
       Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
-    val (int_cmds, cmds) = List.partition #4 (dest_parsers ());
+    val (int_cmds, cmds) = List.partition #3 (dest_parsers ());
   in
-    [Pretty.strs ("syntax keywords:" :: map quote (dest_keywords ())),
+    [Pretty.strs ("syntax keywords:" :: map quote (OuterKeyword.dest_keywords ())),
       Pretty.big_list "commands:" (map pretty_cmd cmds),
       Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)]
     |> Pretty.chunks |> Pretty.writeln
   end;
 
-fun report () =
-  (map report_keyword (dest_keywords ()) @
-    map (fn (name, _, kind, _) => report_command name kind) (dest_parsers ()))
-  |> Pretty.chunks |> Pretty.writeln;
-
 
 
 (** toplevel parsing **)
@@ -235,13 +185,13 @@
 fun scan str =
   Source.of_string str
   |> Symbol.source false
-  |> T.source (SOME false) get_lexicons Position.none
+  |> T.source (SOME false) OuterKeyword.get_lexicons Position.none
   |> Source.exhaust;
 
 fun parse pos str =
   Source.of_string str
   |> Symbol.source false
-  |> T.source (SOME false) get_lexicons pos
+  |> T.source (SOME false) OuterKeyword.get_lexicons pos
   |> toplevel_source false NONE get_parser
   |> Source.exhaust;
 
@@ -268,37 +218,30 @@
 fun isar term : isar =
   Source.tty
   |> Symbol.source true
-  |> T.source (SOME true) get_lexicons Position.none
+  |> T.source (SOME true) OuterKeyword.get_lexicons Position.none
   |> toplevel_source term (SOME true) get_parser;
 
 
-
-(** read theory **)
-
-(* check_text *)
-
-fun check_text s state = (ThyOutput.eval_antiquote (#1 (get_lexicons ())) state s; ());
-
-
 (* load_thy *)
 
 fun load_thy dir name pos text time =
   let
     val text_src = Source.of_list (Library.untabify text);
+    val (lexs, parser) = CRITICAL (fn () => (OuterKeyword.get_lexicons (), get_parser ()));
 
     val _ = Present.init_theory name;
     val _ = Present.verbatim_source name (fn () => Source.exhaust (Symbol.source false text_src));
     val toks = text_src
       |> Symbol.source false
-      |> T.source NONE (K (get_lexicons ())) pos
+      |> T.source NONE (K lexs) pos
       |> Source.exhausted;
     val trs = toks
-      |> toplevel_source false NONE (K (get_parser ()))
+      |> toplevel_source false NONE (K parser)
       |> Source.exhaust;
 
     val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
     val _ = cond_timeit time "" (fn () =>
-      ThyOutput.process_thy (#1 (get_lexicons ())) command_tags is_markup trs toks
+      ThyOutput.process_thy (#1 lexs) OuterKeyword.command_tags is_markup trs toks
       |> Buffer.content
       |> Present.theory_output name);
     val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
diff -r 8adeff7fd4bc -r 71c4dd53d4cb src/Pure/ProofGeneral/pgip_parser.ML
--- a/src/Pure/ProofGeneral/pgip_parser.ML	Wed Jun 25 14:54:45 2008 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Wed Jun 25 17:38:32 2008 +0200
@@ -83,7 +83,7 @@
 
 fun parse_command "sorry" text = [D.Postponegoal {text = text}, D.Closeblock {}]
   | parse_command name text =
-      (case OuterSyntax.command_keyword name of
+      (case OuterKeyword.command_keyword name of
         NONE => [D.Unparseable {text = text}]
       | SOME k =>
           (case Symtab.lookup command_keywords (OuterKeyword.kind_of k) of
diff -r 8adeff7fd4bc -r 71c4dd53d4cb src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Jun 25 14:54:45 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Jun 25 17:38:32 2008 +0200
@@ -359,16 +359,15 @@
 (** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
 
 fun lexicalstructure_keywords () =
-    let val commands = OuterSyntax.dest_keywords ()
-        fun category_of k = if k mem commands then "major" else "minor"
-         (* NB: we might filter to only include words like elisp case (OuterSyntax.is_keyword). *)
-        fun keyword_elt (keyword,help,kind,_) =
-            XML.Elem("keyword", [("word", keyword), ("category", category_of kind)],
-                     [XML.Elem("shorthelp", [], [XML.Text help])])
+    let val keywords = OuterKeyword.dest_keywords ()
+        val commands = OuterKeyword.dest_commands ()
+        fun keyword_elt kind keyword =
+            XML.Elem("keyword", [("word", keyword), ("category", kind)], [])
         in
             (* Also, note we don't call init_outer_syntax here to add interface commands,
             but they should never appear in scripts anyway so it shouldn't matter *)
-            Lexicalstructure {content = map keyword_elt (OuterSyntax.dest_parsers()) }
+            Lexicalstructure
+              {content = map (keyword_elt "minor") keywords @ map (keyword_elt "major") commands}
         end
 
 (* TODO: we can issue a lexicalstructure/keyword when the syntax gets extended dynamically;
diff -r 8adeff7fd4bc -r 71c4dd53d4cb src/Pure/Thy/thy_edit.ML
--- a/src/Pure/Thy/thy_edit.ML	Wed Jun 25 14:54:45 2008 +0200
+++ b/src/Pure/Thy/thy_edit.ML	Wed Jun 25 17:38:32 2008 +0200
@@ -35,7 +35,7 @@
 
 fun token_source pos src =
   Symbol.source true src
-  |> T.source (SOME false) OuterSyntax.get_lexicons pos;
+  |> T.source (SOME false) OuterKeyword.get_lexicons pos;
 
 fun parse_tokens pos src = Source.exhaust (token_source pos src);
 
diff -r 8adeff7fd4bc -r 71c4dd53d4cb src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Wed Jun 25 14:54:45 2008 +0200
+++ b/src/Pure/codegen.ML	Wed Jun 25 17:38:32 2008 +0200
@@ -1111,7 +1111,7 @@
 
 structure P = OuterParse and K = OuterKeyword;
 
-val _ = OuterSyntax.keywords ["attach", "file", "contains"];
+val _ = List.app OuterKeyword.keyword ["attach", "file", "contains"];
 
 fun strip_whitespace s = implode (fst (take_suffix (equal "\n" orf equal " ")
   (snd (take_prefix (equal "\n" orf equal " ") (explode s))))) ^ "\n";
diff -r 8adeff7fd4bc -r 71c4dd53d4cb src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Wed Jun 25 14:54:45 2008 +0200
+++ b/src/Tools/code/code_target.ML	Wed Jun 25 17:38:32 2008 +0200
@@ -2216,7 +2216,7 @@
      -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") []
   ) >> (fn (raw_cs, seris) => cmd raw_cs seris));
 
-val _ = OuterSyntax.keywords [infixK, infixlK, infixrK, inK, module_nameK, fileK];
+val _ = List.app OuterKeyword.keyword [infixK, infixlK, infixrK, inK, module_nameK, fileK];
 
 val _ =
   OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl (
diff -r 8adeff7fd4bc -r 71c4dd53d4cb src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Wed Jun 25 14:54:45 2008 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Wed Jun 25 17:38:32 2008 +0200
@@ -188,7 +188,7 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-val _ = OuterSyntax.keywords ["elimination", "induction", "case_eqns", "recursor_eqns"];
+val _ = List.app OuterKeyword.keyword ["elimination", "induction", "case_eqns", "recursor_eqns"];
 
 val rep_datatype_decl =
   (P.$$$ "elimination" |-- P.!!! SpecParse.xthm) --