--- 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 *)
--- 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 =>
--- 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
--- 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;
--- 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" ?? *)
--- 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);
--- 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)
}
--- 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"
--- 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);
--- /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)
+}
+