# HG changeset patch # User wenzelm # Date 1331766645 -3600 # Node ID cda0182945152358ef46c82d802a67f6e651e68a # Parent efb98d27dc1a41dd3e566e68095b2920918d0e89 some support for outer syntax keyword declarations within theory header; more uniform Thy_Header.header as argument for begin_theory etc.; diff -r efb98d27dc1a -r cda018294515 etc/isar-keywords-ZF.el --- a/etc/isar-keywords-ZF.el Wed Mar 14 22:34:18 2012 +0100 +++ b/etc/isar-keywords-ZF.el Thu Mar 15 00:10:45 2012 +0100 @@ -229,6 +229,7 @@ "infixr" "intros" "is" + "keywords" "monos" "notes" "obtains" diff -r efb98d27dc1a -r cda018294515 etc/isar-keywords.el --- a/etc/isar-keywords.el Wed Mar 14 22:34:18 2012 +0100 +++ b/etc/isar-keywords.el Thu Mar 15 00:10:45 2012 +0100 @@ -305,6 +305,7 @@ "infixl" "infixr" "is" + "keywords" "lazy" "module_name" "monos" diff -r efb98d27dc1a -r cda018294515 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Wed Mar 14 22:34:18 2012 +0100 +++ b/src/Pure/Isar/isar_syn.ML Thu Mar 15 00:10:45 2012 +0100 @@ -18,7 +18,7 @@ "\\", "\\", "\\", "]", "advanced", "and", "assumes", "attach", "begin", "binder", "constrains", "defines", "fixes", "for", "identifier", "if", - "imports", "in", "infix", "infixl", "infixr", "is", + "imports", "in", "infix", "infixl", "infixr", "is", "keywords", "notes", "obtains", "open", "output", "overloaded", "pervasive", "shows", "structure", "unchecked", "uses", "where", "|"]; @@ -28,12 +28,10 @@ val _ = Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin) - (Thy_Header.args >> (fn (name, imports, uses) => + (Thy_Header.args >> (fn header => Toplevel.print o Toplevel.init_theory - (fn () => - Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) - name imports (map (apfst Path.explode) uses)))); + (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header))); val _ = Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end) diff -r efb98d27dc1a -r cda018294515 src/Pure/Isar/keyword.ML --- a/src/Pure/Isar/keyword.ML Wed Mar 14 22:34:18 2012 +0100 +++ b/src/Pure/Isar/keyword.ML Thu Mar 15 00:10:45 2012 +0100 @@ -37,6 +37,7 @@ val tag_theory: T -> T val tag_proof: T -> T val tag_ml: T -> T + val make: string * string list -> T val get_lexicons: unit -> Scan.lexicon * Scan.lexicon val is_keyword: string -> bool val dest_keywords: unit -> string list @@ -115,6 +116,39 @@ val tag_ml = tag "ML"; +(* external names *) + +val name_table = Symtab.make + [("control", control), + ("diag", diag), + ("thy_begin", thy_begin), + ("thy_switch", thy_switch), + ("thy_end", thy_end), + ("thy_heading", thy_heading), + ("thy_decl", thy_decl), + ("thy_script", thy_script), + ("thy_goal", thy_goal), + ("thy_schematic_goal", thy_schematic_goal), + ("qed", qed), + ("qed_block", qed_block), + ("qed_global", qed_global), + ("prf_heading", prf_heading), + ("prf_goal", prf_goal), + ("prf_block", prf_block), + ("prf_open", prf_open), + ("prf_close", prf_close), + ("prf_chain", prf_chain), + ("prf_decl", prf_decl), + ("prf_asm", prf_asm), + ("prf_asm_goal", prf_asm_goal), + ("prf_script", prf_script)]; + +fun make (kind, tags) = + (case Symtab.lookup name_table kind of + SOME k => k |> fold tag tags + | NONE => error ("Unknown outer syntax keyword kind " ^ quote kind)); + + (** global keyword tables **) diff -r efb98d27dc1a -r cda018294515 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Wed Mar 14 22:34:18 2012 +0100 +++ b/src/Pure/PIDE/document.ML Thu Mar 15 00:10:45 2012 +0100 @@ -15,7 +15,7 @@ val new_id: unit -> id val parse_id: string -> id val print_id: id -> string - type node_header = ((string * string) * string list * (string * bool) list) Exn.result + type node_header = (string * Thy_Header.header) Exn.result datatype node_edit = Clear | Edits of (command_id option * command_id option) list | @@ -58,7 +58,7 @@ (** document structure **) -type node_header = ((string * string) * string list * (string * bool) list) Exn.result; +type node_header = (string * Thy_Header.header) Exn.result; type perspective = (command_id -> bool) * command_id option; (*visible commands, last*) structure Entries = Linear_Set(type key = command_id val ord = int_ord); @@ -212,7 +212,7 @@ |> touch_node name | Header header => let - val imports = (case header of Exn.Res (_, imports, _) => imports | _ => []); + val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []); val nodes1 = nodes |> default_node name |> fold default_node imports; @@ -307,7 +307,6 @@ end; - (* toplevel transactions *) local @@ -447,16 +446,15 @@ fun init_theory deps node = let (* FIXME provide files via Scala layer, not master_dir *) - val ((master_dir, thy_name), imports, uses) = Exn.release (get_header node); - val files = map (apfst Path.explode) uses; + val (master_dir, header) = Exn.release (get_header node); val parents = - imports |> map (fn import => + #imports header |> map (fn import => (case Thy_Info.lookup_theory import of (* FIXME more robust!? *) SOME thy => thy | NONE => get_theory (Position.file_only import) (snd (Future.join (the (AList.lookup (op =) deps import)))))); - in Thy_Load.begin_theory (Path.explode master_dir) thy_name imports files parents end; + in Thy_Load.begin_theory (Path.explode master_dir) header parents end; in diff -r efb98d27dc1a -r cda018294515 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Wed Mar 14 22:34:18 2012 +0100 +++ b/src/Pure/PIDE/document.scala Thu Mar 15 00:10:45 2012 +0100 @@ -39,7 +39,10 @@ object Node { - sealed case class Deps(imports: List[Name], uses: List[(String, Boolean)]) + sealed case class Deps( + imports: List[Name], + keywords: List[(String, Option[(String, List[String])])], + uses: List[(String, Boolean)]) object Name { diff -r efb98d27dc1a -r cda018294515 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Wed Mar 14 22:34:18 2012 +0100 +++ b/src/Pure/PIDE/protocol.ML Thu Mar 15 00:10:45 2012 +0100 @@ -46,9 +46,16 @@ [fn ([], []) => Document.Clear, fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), fn ([], a) => - Document.Header - (Exn.Res - (triple (pair string string) (list string) (list (pair string bool)) a)), + let + val ((((master, name), imports), keywords), uses) = + pair (pair (pair (pair string string) (list string)) + (list (pair string (option (pair string (list string)))))) + (list (pair string bool)) a; + val res = + Exn.capture (fn () => + (master, Thy_Header.make name imports keywords + (map (apfst Path.explode) uses))) (); + in Document.Header res end, fn ([a], []) => Document.Header (Exn.Exn (ERROR a)), fn (a, []) => Document.Perspective (map int_atom a)])) end; diff -r efb98d27dc1a -r cda018294515 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Wed Mar 14 22:34:18 2012 +0100 +++ b/src/Pure/PIDE/protocol.scala Thu Mar 15 00:10:45 2012 +0100 @@ -225,8 +225,10 @@ // FIXME val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2)) val uses = deps.uses (Nil, - triple(pair(symbol_string, symbol_string), list(symbol_string), - list(pair(symbol_string, bool)))((dir, name.theory), imports, uses)) }, + pair(pair(pair(pair(symbol_string, symbol_string), list(symbol_string)), + list(pair(symbol_string, option(pair(symbol_string, list(symbol_string)))))), + list(pair(symbol_string, bool)))( + (((dir, name.theory), imports), deps.keywords), uses)) }, { case Document.Node.Header(Exn.Exn(e)) => (List(Symbol.encode(Exn.message(e))), Nil) }, { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) })) def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) => diff -r efb98d27dc1a -r cda018294515 src/Pure/ProofGeneral/pgip_parser.ML --- a/src/Pure/ProofGeneral/pgip_parser.ML Wed Mar 14 22:34:18 2012 +0100 +++ b/src/Pure/ProofGeneral/pgip_parser.ML Thu Mar 15 00:10:45 2012 +0100 @@ -21,7 +21,7 @@ fun thy_begin text = (case try (Thy_Header.read Position.none) text of NONE => D.Opentheory {thyname = NONE, parentnames = [], text = text} - | SOME (name, imports, _) => + | SOME {name, imports, ...} => D.Opentheory {thyname = SOME name, parentnames = imports, text = text}) :: [D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}]; diff -r efb98d27dc1a -r cda018294515 src/Pure/Thy/thy_header.ML --- a/src/Pure/Thy/thy_header.ML Wed Mar 14 22:34:18 2012 +0100 +++ b/src/Pure/Thy/thy_header.ML Thu Mar 15 00:10:45 2012 +0100 @@ -6,40 +6,97 @@ signature THY_HEADER = sig - val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list - val read: Position.T -> string -> string * string list * (Path.T * bool) list + type header = + {name: string, imports: string list, + keywords: (string * (string * string list) option) list, + uses: (Path.T * bool) list} + val make: string -> string list -> (string * (string * string list) option) list -> + (Path.T * bool) list -> header + val declare_keyword: string * (string * string list) option -> theory -> theory + val the_keyword: theory -> string -> Keyword.T option + val args: header parser + val read: Position.T -> string -> header end; structure Thy_Header: THY_HEADER = struct -(* keywords *) +type header = + {name: string, imports: string list, + keywords: (string * (string * string list) option) list, + uses: (Path.T * bool) list}; + +fun make name imports keywords uses : header = + {name = name, imports = imports, keywords = keywords, uses = uses}; + + + +(** keyword declarations **) + +fun err_dup name = error ("Inconsistent declaration of outer syntax keyword " ^ quote name); + +structure Data = Theory_Data +( + type T = Keyword.T option Symtab.table; + val empty = Symtab.empty; + val extend = I; + fun merge data : T = Symtab.merge (op =) data handle Symtab.DUP name => err_dup name; +); + +fun declare_keyword (name, kind) = + Data.map (fn data => + Symtab.update_new (name, Option.map Keyword.make kind) data + handle Symtab.DUP name => err_dup name); + +fun the_keyword thy name = + (case Symtab.lookup (Data.get thy) name of + SOME decl => decl + | NONE => error ("Unknown outer syntax keyword " ^ quote name)); + + + +(** concrete syntax **) + +(* header keywords *) val headerN = "header"; val theoryN = "theory"; val importsN = "imports"; +val keywordsN = "keywords"; val usesN = "uses"; val beginN = "begin"; -val header_lexicon = Scan.make_lexicon - (map Symbol.explode ["%", "(", ")", ";", beginN, headerN, importsN, theoryN, usesN]); +val header_lexicon = + Scan.make_lexicon + (map Symbol.explode + ["%", "(", ")", "::", ";", "and", beginN, headerN, importsN, keywordsN, theoryN, usesN]); (* header args *) -val file_name = Parse.group (fn () => "file name") Parse.name; +local + +val file_name = Parse.group (fn () => "file name") Parse.path; val theory_name = Parse.group (fn () => "theory name") Parse.name; +val keyword_kind = Parse.group (fn () => "outer syntax keyword kind") (Parse.name -- Parse.tags); +val keyword_decl = Parse.name -- Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_kind); + val file = Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false || file_name >> rpair true; -val uses = Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) []; +in val args = - theory_name -- (Parse.$$$ importsN |-- - Parse.!!! (Scan.repeat1 theory_name -- uses --| Parse.$$$ beginN)) - >> Parse.triple2; + theory_name -- + (Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name)) -- + Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! (Parse.and_list1 keyword_decl)) [] -- + Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) [] --| + Parse.$$$ beginN >> + (fn (((name, imports), keywords), uses) => make name imports keywords uses); + +end; (* read header *) @@ -61,7 +118,7 @@ |> Source.get_single; in (case res of - SOME ((name, imports, uses), _) => (name, imports, map (apfst Path.explode) uses) + SOME (h, _) => h | NONE => error ("Unexpected end of input" ^ Position.str_of pos)) end; diff -r efb98d27dc1a -r cda018294515 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Wed Mar 14 22:34:18 2012 +0100 +++ b/src/Pure/Thy/thy_header.scala Thu Mar 15 00:10:45 2012 +0100 @@ -20,10 +20,13 @@ val HEADER = "header" val THEORY = "theory" val IMPORTS = "imports" + val KEYWORDS = "keywords" + val AND = "and" val USES = "uses" val BEGIN = "begin" - private val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES) + private val lexicon = + Scan.Lexicon("%", "(", ")", "::", ";", AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY, USES) /* theory file name */ @@ -45,15 +48,26 @@ val file_name = atom("file name", _.is_name) val theory_name = atom("theory name", _.is_name) + val keyword_kind = + atom("outer syntax keyword kind", _.is_name) ~ tags ^^ { case x ~ y => (x, y) } + val keyword_decl = + name ~ opt(keyword("::") ~! keyword_kind ^^ { case _ ~ x => x }) ^^ + { case x ~ y => (x, y) } + val keywords = + keyword_decl ~ rep(keyword(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^ + { case x ~ ys => x :: ys } + val file = keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => (x, false) } | file_name ^^ (x => (x, true)) - val uses = opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs } - val args = - theory_name ~ (keyword(IMPORTS) ~! (rep1(theory_name) ~ uses ~ keyword(BEGIN))) ^^ - { case x ~ (_ ~ (ys ~ zs ~ _)) => Thy_Header(x, ys, zs) } + theory_name ~ + (keyword(IMPORTS) ~! (rep1(theory_name)) ^^ { case _ ~ xs => xs }) ~ + (opt(keyword(KEYWORDS) ~! keywords) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ + (opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ + keyword(BEGIN) ^^ + { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) } (keyword(HEADER) ~ tags) ~! ((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } | @@ -98,9 +112,11 @@ sealed case class Thy_Header( - val name: String, val imports: List[String], val uses: List[(String, Boolean)]) + name: String, imports: List[String], + keywords: List[(String, Option[(String, List[String])])], + uses: List[(String, Boolean)]) { def map(f: String => String): Thy_Header = - Thy_Header(f(name), imports.map(f), uses.map(p => (f(p._1), p._2))) + Thy_Header(f(name), imports.map(f), keywords, uses.map(p => (f(p._1), p._2))) } diff -r efb98d27dc1a -r cda018294515 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Wed Mar 14 22:34:18 2012 +0100 +++ b/src/Pure/Thy/thy_info.ML Thu Mar 15 00:10:45 2012 +0100 @@ -21,7 +21,7 @@ val use_thys_wrt: Path.T -> string list -> unit val use_thys: string list -> unit val use_thy: string -> unit - val toplevel_begin_theory: Path.T -> string -> string list -> (Path.T * bool) list -> theory + val toplevel_begin_theory: Path.T -> Thy_Header.header -> theory val register_thy: theory -> unit val finish: unit -> unit end; @@ -233,9 +233,10 @@ val {master = (thy_path, _), imports} = deps; val dir = Path.dir thy_path; val pos = Path.position thy_path; - val (_, _, uses) = Thy_Header.read pos text; + val {uses, keywords, ...} = Thy_Header.read pos text; + val header = Thy_Header.make name imports keywords uses; - val (theory, present) = Thy_Load.load_thy update_time dir name imports uses pos text parents; + val (theory, present) = Thy_Load.load_thy update_time dir header pos text parents; fun commit () = update_thy deps theory; in (theory, present, commit) end; @@ -308,12 +309,13 @@ (* toplevel begin theory -- without maintaining database *) -fun toplevel_begin_theory dir name imports uses = +fun toplevel_begin_theory dir (header: Thy_Header.header) = let + val {name, imports, ...} = header; val _ = kill_thy name; val _ = use_thys_wrt dir imports; val parents = map (get_theory o base_name) imports; - in Thy_Load.begin_theory dir name imports uses parents end; + in Thy_Load.begin_theory dir header parents end; (* register theory *) diff -r efb98d27dc1a -r cda018294515 src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Wed Mar 14 22:34:18 2012 +0100 +++ b/src/Pure/Thy/thy_load.ML Thu Mar 15 00:10:45 2012 +0100 @@ -19,10 +19,9 @@ val all_current: theory -> bool val use_ml: Path.T -> unit val exec_ml: Path.T -> generic_theory -> generic_theory - val begin_theory: Path.T -> string -> string list -> (Path.T * bool) list -> - theory list -> theory - val load_thy: int -> Path.T -> string -> string list -> (Path.T * bool) list -> - Position.T -> string -> theory list -> theory * unit future + val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory + val load_thy: int -> Path.T -> Thy_Header.header -> Position.T -> string -> + theory list -> theory * unit future val set_master_path: Path.T -> unit val get_master_path: unit -> Path.T end; @@ -85,7 +84,9 @@ val text = File.read master_file; val (name', imports, uses) = if name = Context.PureN then (Context.PureN, [], []) - else Thy_Header.read (Path.position master_file) text; + else + let val {name, imports, uses, ...} = Thy_Header.read (Path.position master_file) text + in (name, imports, uses) end; val _ = name <> name' andalso error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name'); in {master = (master_file, SHA1.digest text), text = text, imports = imports, uses = uses} end; @@ -159,21 +160,23 @@ (* load_thy *) -fun begin_theory dir name imports uses parents = +fun begin_theory dir {name, imports, keywords, uses} parents = Theory.begin_theory name parents |> put_deps dir imports + |> fold Thy_Header.declare_keyword keywords |> fold (require o fst) uses |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses |> Theory.checkpoint; -fun load_thy update_time dir name imports uses pos text parents = +fun load_thy update_time dir header pos text parents = let val (lexs, outer_syntax) = Outer_Syntax.get_syntax (); val time = ! Toplevel.timing; + val {name, imports, uses, ...} = header; val _ = Present.init_theory name; fun init () = - begin_theory dir name imports uses parents + begin_theory dir header parents |> Present.begin_theory update_time dir uses; val toks = Thy_Syntax.parse_tokens lexs pos text; diff -r efb98d27dc1a -r cda018294515 src/Pure/Thy/thy_load.scala --- a/src/Pure/Thy/thy_load.scala Wed Mar 14 22:34:18 2012 +0100 +++ b/src/Pure/Thy/thy_load.scala Thu Mar 15 00:10:45 2012 +0100 @@ -61,7 +61,7 @@ val uses = header.uses if (name.theory != name1) error("Bad file name " + thy_path(Path.basic(name.theory)) + " for theory " + quote(name1)) - Document.Node.Deps(imports, uses) + Document.Node.Deps(imports, header.keywords, uses) } def check_thy(name: Document.Node.Name): Document.Node.Deps =