# HG changeset patch
# User wenzelm
# Date 1415270681 -3600
# Node ID 8d36bc5eaed322101b993cb1dc5fd46b4160f624
# Parent  edcd9339bda1f8d80a168f183532881b84ff02c9
simplified keyword kinds;
more explicit bootstrap syntax;

diff -r edcd9339bda1 -r 8d36bc5eaed3 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Wed Nov 05 22:39:49 2014 +0100
+++ b/src/Pure/Isar/keyword.ML	Thu Nov 06 11:44:41 2014 +0100
@@ -16,7 +16,6 @@
   val thy_decl: T
   val thy_decl_block: T
   val thy_load: T
-  val thy_load_files: string list -> T
   val thy_goal: T
   val qed: T
   val qed_script: T
@@ -32,12 +31,6 @@
   val prf_asm_goal: T
   val prf_asm_goal_script: T
   val prf_script: T
-  val kinds: T 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
   type spec = (string * string list) * string list
   val spec: spec -> T
   val command_spec: (string * spec) * Position.T -> (string * T) * Position.T
@@ -75,21 +68,17 @@
 
 (** keyword classification **)
 
+(* kinds *)
+
 datatype T = Keyword of
  {kind: string,
   files: string list,  (*extensions of embedded files*)
-  tags: string list};  (*tags in canonical reverse order*)
+  tags: string list};
 
 fun kind s = Keyword {kind = s, files = [], tags = []};
 fun kind_of (Keyword {kind, ...}) = kind;
 fun kind_files_of (Keyword {kind, files, ...}) = (kind, files);
 
-fun add_files fs (Keyword {kind, files, tags}) =
-  Keyword {kind = kind, files = files @ fs, tags = tags};
-
-
-(* kinds *)
-
 val diag = kind "diag";
 val heading = kind "heading";
 val thy_begin = kind "thy_begin";
@@ -97,7 +86,6 @@
 val thy_decl = kind "thy_decl";
 val thy_decl_block = kind "thy_decl_block";
 val thy_load = kind "thy_load";
-fun thy_load_files files = Keyword {kind = "thy_load", files = files, tags = []};
 val thy_goal = kind "thy_goal";
 val qed = kind "qed";
 val qed_script = kind "qed_script";
@@ -117,35 +105,20 @@
 val kinds =
   [diag, heading, thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal,
     qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close,
-    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
+    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script]
+  |> map kind_of;
 
 
-(* tags *)
-
-fun tag t (Keyword {kind, files, tags}) =
-  Keyword {kind = kind, files = files, tags = update (op =) t tags};
-fun tags_of (Keyword {tags, ...}) = tags;
-
-val tag_theory = tag "theory";
-val tag_proof = tag "proof";
-val tag_ml = tag "ML";
-
-
-(* external names *)
-
-val name_table = Symtab.make (map (`kind_of) kinds);
+(* specifications *)
 
 type spec = (string * string list) * string list;
 
-fun spec ((name, files), tags) =
-  (case Symtab.lookup name_table name of
-    SOME kind =>
-      let val kind' = kind |> fold tag tags in
-        if null files then kind'
-        else if name = kind_of thy_load then kind' |> add_files files
-        else error ("Illegal specification of files for " ^ quote name)
-      end
-  | NONE => error ("Unknown outer syntax keyword kind " ^ quote name));
+fun spec ((kind, files), tags) =
+  if not (member (op =) kinds kind) then
+    error ("Unknown outer syntax keyword kind " ^ quote kind)
+  else if not (null files) andalso kind <> kind_of thy_load then
+    error ("Illegal specification of files for " ^ quote kind)
+  else Keyword {kind = kind, files = files, tags = tags};
 
 fun command_spec ((name, s), pos) = ((name, spec s), pos);
 
@@ -234,7 +207,10 @@
       else if null files then [path]
       else map (fn ext => Path.ext ext path) files);
 
-val command_tags = these o Option.map tags_of o command_keyword;
+fun command_tags name =
+  (case command_keyword name of
+    SOME (Keyword {tags, ...}) => tags
+  | NONE => []);
 
 
 (* command categories *)
diff -r edcd9339bda1 -r 8d36bc5eaed3 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed Nov 05 22:39:49 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Nov 06 11:44:41 2014 +0100
@@ -116,12 +116,11 @@
       (case try (Thy_Header.the_keyword thy) name of
         SOME spec =>
           if Option.map #1 spec = SOME (Keyword.kind_files_of kind) then ()
-          else error ("Inconsistent outer syntax keyword declaration " ^
-            command_name ^ Position.here pos)
+          else
+            error ("Inconsistent outer syntax keyword declaration " ^
+              command_name ^ Position.here pos)
       | NONE =>
-          if Context.theory_name thy = Context.PureN
-          then Keyword.define (name, SOME kind)
-          else error ("Undeclared outer syntax command " ^ command_name ^ Position.here pos));
+          error ("Undeclared outer syntax command " ^ command_name ^ Position.here pos));
     val _ = Context_Position.report_generic context pos (command_markup true (name, cmd));
   in
     Unsynchronized.change global_syntax (map_commands (fn commands =>
diff -r edcd9339bda1 -r 8d36bc5eaed3 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Nov 05 22:39:49 2014 +0100
+++ b/src/Pure/PIDE/document.ML	Thu Nov 06 11:44:41 2014 +0100
@@ -208,7 +208,7 @@
         let
           val imports = map fst (#imports header);
           val errors1 =
-            (Thy_Header.define_keywords header; errors)
+            (Thy_Header.define_keywords (#keywords header); errors)
               handle ERROR msg => errors @ [msg];
           val nodes1 = nodes
             |> default_node name
diff -r edcd9339bda1 -r 8d36bc5eaed3 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Wed Nov 05 22:39:49 2014 +0100
+++ b/src/Pure/PIDE/resources.ML	Thu Nov 06 11:44:41 2014 +0100
@@ -145,8 +145,8 @@
 
 fun load_thy document last_timing update_time master_dir header text_pos text parents =
   let
-    val {name = (name, _), ...} = header;
-    val _ = Thy_Header.define_keywords header;
+    val (name, _) = #name header;
+    val _ = Thy_Header.define_keywords (#keywords header);
     val keywords = Keyword.get_keywords ();
 
     val toks = Outer_Syntax.scan keywords text_pos text;
diff -r edcd9339bda1 -r 8d36bc5eaed3 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Nov 05 22:39:49 2014 +0100
+++ b/src/Pure/Pure.thy	Thu Nov 06 11:44:41 2014 +0100
@@ -13,7 +13,6 @@
     "identifier" "if" "imports" "in" "includes" "infix" "infixl"
     "infixr" "is" "keywords" "notes" "obtains" "open" "output"
     "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
-  and "theory" :: thy_begin % "theory"
   and "header" :: heading
   and "chapter" :: heading
   and "section" :: heading
@@ -27,7 +26,7 @@
     "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
     "no_notation" "axiomatization" "theorems" "lemmas" "declare"
     "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
-  and "SML_file" "ML_file" :: thy_load % "ML"
+  and "SML_file" :: thy_load % "ML"
   and "SML_import" "SML_export" :: thy_decl % "ML"
   and "ML" :: thy_decl % "ML"
   and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
diff -r edcd9339bda1 -r 8d36bc5eaed3 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Wed Nov 05 22:39:49 2014 +0100
+++ b/src/Pure/Thy/thy_header.ML	Thu Nov 06 11:44:41 2014 +0100
@@ -12,7 +12,7 @@
     imports: (string * Position.T) list,
     keywords: keywords}
   val make: string * Position.T -> (string * Position.T) list -> keywords -> header
-  val define_keywords: header -> unit
+  val define_keywords: keywords -> unit
   val declare_keyword: string * Keyword.spec option -> theory -> theory
   val the_keyword: theory -> string -> Keyword.spec option
   val args: header parser
@@ -37,7 +37,7 @@
 
 (** keyword declarations **)
 
-fun define_keywords ({keywords, ...}: header) =
+fun define_keywords (keywords: keywords) =
   List.app (Keyword.define o apsnd (Option.map Keyword.spec)) keywords;
 
 fun err_dup name = error ("Duplicate declaration of outer syntax keyword " ^ quote name);
diff -r edcd9339bda1 -r 8d36bc5eaed3 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Nov 05 22:39:49 2014 +0100
+++ b/src/Pure/Tools/build.scala	Thu Nov 06 11:44:41 2014 +0100
@@ -437,7 +437,7 @@
             val (loaded_theories0, known_theories0, syntax0) =
               info.parent.map(deps(_)) match {
                 case None =>
-                  (Set.empty[String], Map.empty[String, Document.Node.Name], Outer_Syntax.init())
+                  (Set.empty[String], Map.empty[String, Document.Node.Name], Pure_Syn.init())
                 case Some(parent) =>
                   (parent.loaded_theories, parent.known_theories, parent.syntax)
               }
diff -r edcd9339bda1 -r 8d36bc5eaed3 src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Nov 05 22:39:49 2014 +0100
+++ b/src/Pure/build-jars	Thu Nov 06 11:44:41 2014 +0100
@@ -99,6 +99,7 @@
   Tools/update_header.scala
   Tools/update_semicolons.scala
   library.scala
+  pure_syn.scala
   term.scala
   term_xml.scala
   "../Tools/Graphview/src/graph_panel.scala"
diff -r edcd9339bda1 -r 8d36bc5eaed3 src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Wed Nov 05 22:39:49 2014 +0100
+++ b/src/Pure/pure_syn.ML	Thu Nov 06 11:44:41 2014 +0100
@@ -7,15 +7,32 @@
 structure Pure_Syn: sig end =
 struct
 
+(* keywords *)
+
+val keywords: Thy_Header.keywords =
+ [("theory", SOME (("thy_begin", []), ["theory"])),
+  ("ML_file", SOME (("thy_load", []), ["ML"]))];
+
+fun command_spec (name, pos) =
+  (case AList.lookup (op =) keywords name of
+    SOME (SOME spec) => Keyword.command_spec ((name, spec), pos)
+  | _ => error ("Bad command specification " ^ quote name ^ Position.here pos));
+
+val _ = Thy_Header.define_keywords keywords;
+val _ = Theory.setup (fold Thy_Header.declare_keyword keywords);
+
+
+(* commands *)
+
 val _ =
   Outer_Syntax.command
-    (("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory"
+    (command_spec ("theory", @{here})) "begin theory"
     (Thy_Header.args >>
       (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
 
 val _ =
   Outer_Syntax.command
-    (("ML_file", Keyword.tag_ml Keyword.thy_load), @{here}) "ML text from file"
+    (command_spec ("ML_file", @{here})) "ML text from file"
     (Resources.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
         let
           val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
diff -r edcd9339bda1 -r 8d36bc5eaed3 src/Pure/pure_syn.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/pure_syn.scala	Thu Nov 06 11:44:41 2014 +0100
@@ -0,0 +1,19 @@
+/*  Title:      Pure/pure_syn.scala
+    Author:     Makarius
+
+Minimal outer syntax for bootstrapping Isabelle/Pure.
+*/
+
+package isabelle
+
+
+object Pure_Syn
+{
+  private val keywords: Thy_Header.Keywords =
+    List(
+      ("theory", Some((("thy_begin", Nil), List("theory"))), None),
+      ("ML_file", Some((("thy_load", Nil), List("ML"))), None))
+
+  def init(): Outer_Syntax = Outer_Syntax.init().add_keywords(keywords)
+}
+