simplified keyword kinds;
authorwenzelm
Thu Nov 06 11:44:41 2014 +0100 (2014-11-06)
changeset 589188d36bc5eaed3
parent 58910 edcd9339bda1
child 58919 82a71046dce8
simplified keyword kinds;
more explicit bootstrap syntax;
src/Pure/Isar/keyword.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/resources.ML
src/Pure/Pure.thy
src/Pure/Thy/thy_header.ML
src/Pure/Tools/build.scala
src/Pure/build-jars
src/Pure/pure_syn.ML
src/Pure/pure_syn.scala
     1.1 --- a/src/Pure/Isar/keyword.ML	Wed Nov 05 22:39:49 2014 +0100
     1.2 +++ b/src/Pure/Isar/keyword.ML	Thu Nov 06 11:44:41 2014 +0100
     1.3 @@ -16,7 +16,6 @@
     1.4    val thy_decl: T
     1.5    val thy_decl_block: T
     1.6    val thy_load: T
     1.7 -  val thy_load_files: string list -> T
     1.8    val thy_goal: T
     1.9    val qed: T
    1.10    val qed_script: T
    1.11 @@ -32,12 +31,6 @@
    1.12    val prf_asm_goal: T
    1.13    val prf_asm_goal_script: T
    1.14    val prf_script: T
    1.15 -  val kinds: T list
    1.16 -  val tag: string -> T -> T
    1.17 -  val tags_of: T -> string list
    1.18 -  val tag_theory: T -> T
    1.19 -  val tag_proof: T -> T
    1.20 -  val tag_ml: T -> T
    1.21    type spec = (string * string list) * string list
    1.22    val spec: spec -> T
    1.23    val command_spec: (string * spec) * Position.T -> (string * T) * Position.T
    1.24 @@ -75,21 +68,17 @@
    1.25  
    1.26  (** keyword classification **)
    1.27  
    1.28 +(* kinds *)
    1.29 +
    1.30  datatype T = Keyword of
    1.31   {kind: string,
    1.32    files: string list,  (*extensions of embedded files*)
    1.33 -  tags: string list};  (*tags in canonical reverse order*)
    1.34 +  tags: string list};
    1.35  
    1.36  fun kind s = Keyword {kind = s, files = [], tags = []};
    1.37  fun kind_of (Keyword {kind, ...}) = kind;
    1.38  fun kind_files_of (Keyword {kind, files, ...}) = (kind, files);
    1.39  
    1.40 -fun add_files fs (Keyword {kind, files, tags}) =
    1.41 -  Keyword {kind = kind, files = files @ fs, tags = tags};
    1.42 -
    1.43 -
    1.44 -(* kinds *)
    1.45 -
    1.46  val diag = kind "diag";
    1.47  val heading = kind "heading";
    1.48  val thy_begin = kind "thy_begin";
    1.49 @@ -97,7 +86,6 @@
    1.50  val thy_decl = kind "thy_decl";
    1.51  val thy_decl_block = kind "thy_decl_block";
    1.52  val thy_load = kind "thy_load";
    1.53 -fun thy_load_files files = Keyword {kind = "thy_load", files = files, tags = []};
    1.54  val thy_goal = kind "thy_goal";
    1.55  val qed = kind "qed";
    1.56  val qed_script = kind "qed_script";
    1.57 @@ -117,35 +105,20 @@
    1.58  val kinds =
    1.59    [diag, heading, thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal,
    1.60      qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close,
    1.61 -    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
    1.62 +    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script]
    1.63 +  |> map kind_of;
    1.64  
    1.65  
    1.66 -(* tags *)
    1.67 -
    1.68 -fun tag t (Keyword {kind, files, tags}) =
    1.69 -  Keyword {kind = kind, files = files, tags = update (op =) t tags};
    1.70 -fun tags_of (Keyword {tags, ...}) = tags;
    1.71 -
    1.72 -val tag_theory = tag "theory";
    1.73 -val tag_proof = tag "proof";
    1.74 -val tag_ml = tag "ML";
    1.75 -
    1.76 -
    1.77 -(* external names *)
    1.78 -
    1.79 -val name_table = Symtab.make (map (`kind_of) kinds);
    1.80 +(* specifications *)
    1.81  
    1.82  type spec = (string * string list) * string list;
    1.83  
    1.84 -fun spec ((name, files), tags) =
    1.85 -  (case Symtab.lookup name_table name of
    1.86 -    SOME kind =>
    1.87 -      let val kind' = kind |> fold tag tags in
    1.88 -        if null files then kind'
    1.89 -        else if name = kind_of thy_load then kind' |> add_files files
    1.90 -        else error ("Illegal specification of files for " ^ quote name)
    1.91 -      end
    1.92 -  | NONE => error ("Unknown outer syntax keyword kind " ^ quote name));
    1.93 +fun spec ((kind, files), tags) =
    1.94 +  if not (member (op =) kinds kind) then
    1.95 +    error ("Unknown outer syntax keyword kind " ^ quote kind)
    1.96 +  else if not (null files) andalso kind <> kind_of thy_load then
    1.97 +    error ("Illegal specification of files for " ^ quote kind)
    1.98 +  else Keyword {kind = kind, files = files, tags = tags};
    1.99  
   1.100  fun command_spec ((name, s), pos) = ((name, spec s), pos);
   1.101  
   1.102 @@ -234,7 +207,10 @@
   1.103        else if null files then [path]
   1.104        else map (fn ext => Path.ext ext path) files);
   1.105  
   1.106 -val command_tags = these o Option.map tags_of o command_keyword;
   1.107 +fun command_tags name =
   1.108 +  (case command_keyword name of
   1.109 +    SOME (Keyword {tags, ...}) => tags
   1.110 +  | NONE => []);
   1.111  
   1.112  
   1.113  (* command categories *)
     2.1 --- a/src/Pure/Isar/outer_syntax.ML	Wed Nov 05 22:39:49 2014 +0100
     2.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Nov 06 11:44:41 2014 +0100
     2.3 @@ -116,12 +116,11 @@
     2.4        (case try (Thy_Header.the_keyword thy) name of
     2.5          SOME spec =>
     2.6            if Option.map #1 spec = SOME (Keyword.kind_files_of kind) then ()
     2.7 -          else error ("Inconsistent outer syntax keyword declaration " ^
     2.8 -            command_name ^ Position.here pos)
     2.9 +          else
    2.10 +            error ("Inconsistent outer syntax keyword declaration " ^
    2.11 +              command_name ^ Position.here pos)
    2.12        | NONE =>
    2.13 -          if Context.theory_name thy = Context.PureN
    2.14 -          then Keyword.define (name, SOME kind)
    2.15 -          else error ("Undeclared outer syntax command " ^ command_name ^ Position.here pos));
    2.16 +          error ("Undeclared outer syntax command " ^ command_name ^ Position.here pos));
    2.17      val _ = Context_Position.report_generic context pos (command_markup true (name, cmd));
    2.18    in
    2.19      Unsynchronized.change global_syntax (map_commands (fn commands =>
     3.1 --- a/src/Pure/PIDE/document.ML	Wed Nov 05 22:39:49 2014 +0100
     3.2 +++ b/src/Pure/PIDE/document.ML	Thu Nov 06 11:44:41 2014 +0100
     3.3 @@ -208,7 +208,7 @@
     3.4          let
     3.5            val imports = map fst (#imports header);
     3.6            val errors1 =
     3.7 -            (Thy_Header.define_keywords header; errors)
     3.8 +            (Thy_Header.define_keywords (#keywords header); errors)
     3.9                handle ERROR msg => errors @ [msg];
    3.10            val nodes1 = nodes
    3.11              |> default_node name
     4.1 --- a/src/Pure/PIDE/resources.ML	Wed Nov 05 22:39:49 2014 +0100
     4.2 +++ b/src/Pure/PIDE/resources.ML	Thu Nov 06 11:44:41 2014 +0100
     4.3 @@ -145,8 +145,8 @@
     4.4  
     4.5  fun load_thy document last_timing update_time master_dir header text_pos text parents =
     4.6    let
     4.7 -    val {name = (name, _), ...} = header;
     4.8 -    val _ = Thy_Header.define_keywords header;
     4.9 +    val (name, _) = #name header;
    4.10 +    val _ = Thy_Header.define_keywords (#keywords header);
    4.11      val keywords = Keyword.get_keywords ();
    4.12  
    4.13      val toks = Outer_Syntax.scan keywords text_pos text;
     5.1 --- a/src/Pure/Pure.thy	Wed Nov 05 22:39:49 2014 +0100
     5.2 +++ b/src/Pure/Pure.thy	Thu Nov 06 11:44:41 2014 +0100
     5.3 @@ -13,7 +13,6 @@
     5.4      "identifier" "if" "imports" "in" "includes" "infix" "infixl"
     5.5      "infixr" "is" "keywords" "notes" "obtains" "open" "output"
     5.6      "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
     5.7 -  and "theory" :: thy_begin % "theory"
     5.8    and "header" :: heading
     5.9    and "chapter" :: heading
    5.10    and "section" :: heading
    5.11 @@ -27,7 +26,7 @@
    5.12      "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
    5.13      "no_notation" "axiomatization" "theorems" "lemmas" "declare"
    5.14      "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
    5.15 -  and "SML_file" "ML_file" :: thy_load % "ML"
    5.16 +  and "SML_file" :: thy_load % "ML"
    5.17    and "SML_import" "SML_export" :: thy_decl % "ML"
    5.18    and "ML" :: thy_decl % "ML"
    5.19    and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
     6.1 --- a/src/Pure/Thy/thy_header.ML	Wed Nov 05 22:39:49 2014 +0100
     6.2 +++ b/src/Pure/Thy/thy_header.ML	Thu Nov 06 11:44:41 2014 +0100
     6.3 @@ -12,7 +12,7 @@
     6.4      imports: (string * Position.T) list,
     6.5      keywords: keywords}
     6.6    val make: string * Position.T -> (string * Position.T) list -> keywords -> header
     6.7 -  val define_keywords: header -> unit
     6.8 +  val define_keywords: keywords -> unit
     6.9    val declare_keyword: string * Keyword.spec option -> theory -> theory
    6.10    val the_keyword: theory -> string -> Keyword.spec option
    6.11    val args: header parser
    6.12 @@ -37,7 +37,7 @@
    6.13  
    6.14  (** keyword declarations **)
    6.15  
    6.16 -fun define_keywords ({keywords, ...}: header) =
    6.17 +fun define_keywords (keywords: keywords) =
    6.18    List.app (Keyword.define o apsnd (Option.map Keyword.spec)) keywords;
    6.19  
    6.20  fun err_dup name = error ("Duplicate declaration of outer syntax keyword " ^ quote name);
     7.1 --- a/src/Pure/Tools/build.scala	Wed Nov 05 22:39:49 2014 +0100
     7.2 +++ b/src/Pure/Tools/build.scala	Thu Nov 06 11:44:41 2014 +0100
     7.3 @@ -437,7 +437,7 @@
     7.4              val (loaded_theories0, known_theories0, syntax0) =
     7.5                info.parent.map(deps(_)) match {
     7.6                  case None =>
     7.7 -                  (Set.empty[String], Map.empty[String, Document.Node.Name], Outer_Syntax.init())
     7.8 +                  (Set.empty[String], Map.empty[String, Document.Node.Name], Pure_Syn.init())
     7.9                  case Some(parent) =>
    7.10                    (parent.loaded_theories, parent.known_theories, parent.syntax)
    7.11                }
     8.1 --- a/src/Pure/build-jars	Wed Nov 05 22:39:49 2014 +0100
     8.2 +++ b/src/Pure/build-jars	Thu Nov 06 11:44:41 2014 +0100
     8.3 @@ -99,6 +99,7 @@
     8.4    Tools/update_header.scala
     8.5    Tools/update_semicolons.scala
     8.6    library.scala
     8.7 +  pure_syn.scala
     8.8    term.scala
     8.9    term_xml.scala
    8.10    "../Tools/Graphview/src/graph_panel.scala"
     9.1 --- a/src/Pure/pure_syn.ML	Wed Nov 05 22:39:49 2014 +0100
     9.2 +++ b/src/Pure/pure_syn.ML	Thu Nov 06 11:44:41 2014 +0100
     9.3 @@ -7,15 +7,32 @@
     9.4  structure Pure_Syn: sig end =
     9.5  struct
     9.6  
     9.7 +(* keywords *)
     9.8 +
     9.9 +val keywords: Thy_Header.keywords =
    9.10 + [("theory", SOME (("thy_begin", []), ["theory"])),
    9.11 +  ("ML_file", SOME (("thy_load", []), ["ML"]))];
    9.12 +
    9.13 +fun command_spec (name, pos) =
    9.14 +  (case AList.lookup (op =) keywords name of
    9.15 +    SOME (SOME spec) => Keyword.command_spec ((name, spec), pos)
    9.16 +  | _ => error ("Bad command specification " ^ quote name ^ Position.here pos));
    9.17 +
    9.18 +val _ = Thy_Header.define_keywords keywords;
    9.19 +val _ = Theory.setup (fold Thy_Header.declare_keyword keywords);
    9.20 +
    9.21 +
    9.22 +(* commands *)
    9.23 +
    9.24  val _ =
    9.25    Outer_Syntax.command
    9.26 -    (("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory"
    9.27 +    (command_spec ("theory", @{here})) "begin theory"
    9.28      (Thy_Header.args >>
    9.29        (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
    9.30  
    9.31  val _ =
    9.32    Outer_Syntax.command
    9.33 -    (("ML_file", Keyword.tag_ml Keyword.thy_load), @{here}) "ML text from file"
    9.34 +    (command_spec ("ML_file", @{here})) "ML text from file"
    9.35      (Resources.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
    9.36          let
    9.37            val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/Pure/pure_syn.scala	Thu Nov 06 11:44:41 2014 +0100
    10.3 @@ -0,0 +1,19 @@
    10.4 +/*  Title:      Pure/pure_syn.scala
    10.5 +    Author:     Makarius
    10.6 +
    10.7 +Minimal outer syntax for bootstrapping Isabelle/Pure.
    10.8 +*/
    10.9 +
   10.10 +package isabelle
   10.11 +
   10.12 +
   10.13 +object Pure_Syn
   10.14 +{
   10.15 +  private val keywords: Thy_Header.Keywords =
   10.16 +    List(
   10.17 +      ("theory", Some((("thy_begin", Nil), List("theory"))), None),
   10.18 +      ("ML_file", Some((("thy_load", Nil), List("ML"))), None))
   10.19 +
   10.20 +  def init(): Outer_Syntax = Outer_Syntax.init().add_keywords(keywords)
   10.21 +}
   10.22 +