theory def/ref position reports, which enable hyperlinks etc.;
more official header command parsing;
--- a/src/Pure/Isar/isar_syn.ML Sun Aug 26 10:20:26 2012 +0200
+++ b/src/Pure/Isar/isar_syn.ML Sun Aug 26 21:46:50 2012 +0200
@@ -934,7 +934,7 @@
val _ =
Outer_Syntax.improper_command @{command_spec "use_thy"} "use theory file"
- (Parse.name >> (fn name =>
+ (Parse.position Parse.name >> (fn name =>
Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.use_thy name)));
val _ =
--- a/src/Pure/Isar/parse.ML Sun Aug 26 10:20:26 2012 +0200
+++ b/src/Pure/Isar/parse.ML Sun Aug 26 21:46:50 2012 +0200
@@ -34,6 +34,7 @@
val verbatim: string parser
val sync: string parser
val eof: string parser
+ val command_name: string -> string parser
val keyword_with: (string -> bool) -> string parser
val keyword_ident_or_symbolic: string parser
val $$$ : string -> string parser
@@ -190,6 +191,11 @@
fun keyword_with pred = RESET_VALUE (Scan.one (Token.keyword_with pred) >> Token.content_of);
val keyword_ident_or_symbolic = keyword_with Token.ident_or_symbolic;
+fun command_name x =
+ group (fn () => Token.str_of_kind Token.Command ^ " " ^ quote x)
+ (RESET_VALUE (Scan.one (fn tok => Token.is_command tok andalso Token.content_of tok = x)))
+ >> Token.content_of;
+
fun $$$ x =
group (fn () => Token.str_of_kind Token.Keyword ^ " " ^ quote x)
(keyword_with (fn y => x = y));
--- a/src/Pure/ML/ml_antiquote.ML Sun Aug 26 10:20:26 2012 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Sun Aug 26 21:46:50 2012 +0200
@@ -71,8 +71,9 @@
(Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
value (Binding.name "theory")
- (Scan.lift Args.name >> (fn name =>
- "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name)
+ (Args.theory -- Scan.lift (Parse.position Args.name) >> (fn (thy, (name, pos)) =>
+ (Position.report pos (Theory.get_markup (Context.get_theory thy name));
+ "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
|| Scan.succeed "Proof_Context.theory_of ML_context") #>
inline (Binding.name "context") (Scan.succeed "Isabelle.ML_context") #>
--- a/src/Pure/PIDE/document.ML Sun Aug 26 10:20:26 2012 +0200
+++ b/src/Pure/PIDE/document.ML Sun Aug 26 21:46:50 2012 +0200
@@ -83,7 +83,7 @@
fun make_perspective command_ids : perspective =
(Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
-val no_header = ("", Thy_Header.make "" [] [] [], ["Bad theory header"]);
+val no_header = ("", Thy_Header.make ("", Position.none) [] [] [], ["Bad theory header"]);
val no_perspective = make_perspective [];
val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
@@ -92,12 +92,18 @@
(* basic components *)
+fun set_header header =
+ map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
+
fun get_header (Node {header = (master, header, errors), ...}) =
if null errors then (master, header)
else error (cat_lines errors);
-fun set_header header =
- map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
+fun read_header node span =
+ let
+ val (dir, {name = (name, _), imports, keywords, uses}) = get_header node;
+ val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
+ in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords uses) end;
fun get_perspective (Node {perspective, ...}) = perspective;
fun set_perspective ids =
@@ -183,17 +189,18 @@
| Edits edits => update_node name (edit_node edits) nodes
| Deps (master, header, errors) =>
let
+ val imports = map fst (#imports header);
val errors1 =
(Thy_Header.define_keywords header; errors)
handle ERROR msg => errors @ [msg];
val nodes1 = nodes
|> default_node name
- |> fold default_node (#imports header);
+ |> fold default_node imports;
val nodes2 = nodes1
|> Graph.Keys.fold
(fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
val (nodes3, errors2) =
- (Graph.add_deps_acyclic (name, #imports header) nodes2, errors1)
+ (Graph.add_deps_acyclic (name, imports) nodes2, errors1)
handle Graph.CYCLES cs => (nodes2, errors1 @ map cycle_msg cs);
in Graph.map_node name (set_header (master, header, errors2)) nodes3 end
| Perspective perspective => update_node name (set_perspective perspective) nodes);
@@ -373,16 +380,17 @@
Symtab.update (a, ())) all_visible Symtab.empty;
in Symtab.defined required end;
-fun init_theory imports node =
+fun init_theory deps node span =
let
(* FIXME provide files via Scala layer, not master_dir *)
- val (dir, header) = get_header node;
+ val (dir, header) = read_header node span;
val master_dir =
(case try Url.explode dir of
SOME (Url.File path) => path
| _ => Path.current);
+ val imports = #imports header;
val parents =
- #imports header |> map (fn import =>
+ imports |> map (fn (import, _) =>
(case Thy_Info.lookup_theory import of
SOME thy => thy
| NONE =>
@@ -390,7 +398,8 @@
(fst (fst
(Command.memo_result
(the_default no_exec
- (get_result (snd (the (AList.lookup (op =) imports import))))))))));
+ (get_result (snd (the (AList.lookup (op =) deps import))))))))));
+ val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
in Thy_Load.begin_theory master_dir header parents end;
fun check_theory full name node =
@@ -429,7 +438,7 @@
else (common, flags)
end;
-fun illegal_init () = error "Illegal theory header after end of theory";
+fun illegal_init _ = error "Illegal theory header after end of theory";
fun new_exec state proper_init command_id' (execs, command_exec, init) =
if not proper_init andalso is_none init then NONE
@@ -438,7 +447,7 @@
val (name, span) = the_command state command_id' ||> Lazy.force;
val (modify_init, init') =
if Keyword.is_theory_begin name then
- (Toplevel.modify_init (the_default illegal_init init), NONE)
+ (Toplevel.modify_init (fn () => the_default illegal_init init span), NONE)
else (I, init);
val exec_id' = new_id ();
val exec_id'_string = print_id exec_id';
@@ -487,7 +496,7 @@
then
let
val node0 = node_of old_version name;
- fun init () = init_theory imports node;
+ val init = init_theory imports node;
val proper_init =
check_theory false name node andalso
forall (fn (name, (_, node)) => check_theory true name node) imports;
--- a/src/Pure/PIDE/isabelle_markup.ML Sun Aug 26 10:20:26 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML Sun Aug 26 21:46:50 2012 +0200
@@ -26,6 +26,7 @@
val breakN: string val break: int -> Markup.T
val fbreakN: string val fbreak: Markup.T
val hiddenN: string val hidden: Markup.T
+ val theoryN: string
val classN: string
val type_nameN: string
val constantN: string
@@ -165,6 +166,7 @@
(* logical entities *)
+val theoryN = "theory";
val classN = "class";
val type_nameN = "type name";
val constantN = "constant";
--- a/src/Pure/PIDE/protocol.ML Sun Aug 26 10:20:26 2012 +0200
+++ b/src/Pure/PIDE/protocol.ML Sun Aug 26 21:46:50 2012 +0200
@@ -42,10 +42,11 @@
(pair (list (pair string
(option (pair (pair string (list string)) (list string)))))
(pair (list (pair string bool)) (list string))))) a;
+ val imports' = map (rpair Position.none) imports;
val (uses', errors') =
(map (apfst Path.explode) uses, errors)
handle ERROR msg => ([], errors @ [msg]);
- val header = Thy_Header.make name imports keywords uses';
+ val header = Thy_Header.make (name, Position.none) imports' keywords uses';
in Document.Deps (master, header, errors') end,
fn (a, []) => Document.Perspective (map int_atom a)]))
end;
--- a/src/Pure/ProofGeneral/pgip_parser.ML Sun Aug 26 10:20:26 2012 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML Sun Aug 26 21:46:50 2012 +0200
@@ -21,8 +21,8 @@
fun thy_begin text =
(case try (Thy_Header.read Position.none) text of
NONE => D.Opentheory {thyname = NONE, parentnames = [], text = text}
- | SOME {name, imports, ...} =>
- D.Opentheory {thyname = SOME name, parentnames = imports, text = text})
+ | SOME {name = (name, _), imports, ...} =>
+ D.Opentheory {thyname = SOME name, parentnames = map #1 imports, text = text})
:: [D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}];
fun thy_heading text =
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sun Aug 26 10:20:26 2012 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sun Aug 26 21:46:50 2012 +0200
@@ -601,7 +601,7 @@
end
fun thyrefs thy =
- let val thyrefs = #imports (Thy_Load.check_thy Path.current thy)
+ let val thyrefs = map #1 (#imports (Thy_Load.check_thy Path.current thy))
in
issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,
--- a/src/Pure/ROOT.ML Sun Aug 26 10:20:26 2012 +0200
+++ b/src/Pure/ROOT.ML Sun Aug 26 21:46:50 2012 +0200
@@ -306,7 +306,7 @@
(* the Pure theory *)
use "pure_syn.ML";
-Thy_Info.use_thy "Pure";
+Thy_Info.use_thy ("Pure", Position.none);
Context.set_thread_data NONE;
structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
@@ -341,8 +341,8 @@
fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));
-fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
-fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
+fun use_thys args = Toplevel.program (fn () => Thy_Info.use_thys (map (rpair Position.none) args));
+val use_thy = use_thys o single;
val cd = File.cd o Path.explode;
--- a/src/Pure/System/build.ML Sun Aug 26 10:20:26 2012 +0200
+++ b/src/Pure/System/build.ML Sun Aug 26 21:46:50 2012 +0200
@@ -47,7 +47,7 @@
fun use_theories (options, thys) =
let val condition = space_explode "," (Options.string options "condition") in
(case filter_out (can getenv_strict) condition of
- [] => use_thys options thys
+ [] => use_thys options (map (rpair Position.none) thys)
| conds =>
Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
" (undefined " ^ commas conds ^ ")\n"))
--- a/src/Pure/Thy/thy_header.ML Sun Aug 26 10:20:26 2012 +0200
+++ b/src/Pure/Thy/thy_header.ML Sun Aug 26 21:46:50 2012 +0200
@@ -8,16 +8,18 @@
sig
type keywords = (string * Keyword.spec option) list
type header =
- {name: string,
- imports: string list,
+ {name: string * Position.T,
+ imports: (string * Position.T) list,
keywords: keywords,
uses: (Path.T * bool) list}
- val make: string -> string list -> keywords -> (Path.T * bool) list -> header
+ val make: string * Position.T -> (string * Position.T) list -> keywords ->
+ (Path.T * bool) list -> header
val define_keywords: header -> unit
val declare_keyword: string * Keyword.spec option -> theory -> theory
val the_keyword: theory -> string -> Keyword.spec option
val args: header parser
val read: Position.T -> string -> header
+ val read_tokens: Token.T list -> header
end;
structure Thy_Header: THY_HEADER =
@@ -26,8 +28,8 @@
type keywords = (string * Keyword.spec option) list;
type header =
- {name: string,
- imports: string list,
+ {name: string * Position.T,
+ imports: (string * Position.T) list,
keywords: keywords,
uses: (Path.T * bool) list};
@@ -74,10 +76,10 @@
val usesN = "uses";
val beginN = "begin";
-val header_lexicon =
- Scan.make_lexicon
- (map Symbol.explode
- ["%", "(", ")", ",", "::", ";", "and", beginN, headerN, importsN, keywordsN, theoryN, usesN]);
+val header_lexicons =
+ pairself (Scan.make_lexicon o map Symbol.explode)
+ (["%", "(", ")", ",", "::", ";", "and", beginN, importsN, keywordsN, usesN],
+ [headerN, theoryN]);
(* header args *)
@@ -85,7 +87,7 @@
local
val file_name = Parse.group (fn () => "file name") Parse.path >> Path.explode;
-val theory_name = Parse.group (fn () => "theory name") Parse.name;
+val theory_name = Parse.group (fn () => "theory name") (Parse.position Parse.name);
val opt_files =
Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
@@ -118,17 +120,20 @@
(* read header *)
val header =
- (Parse.$$$ headerN -- Parse.tags) |--
+ (Parse.command_name headerN -- Parse.tags) |--
(Parse.!!! (Parse.doc_source -- Scan.repeat Parse.semicolon --
- (Parse.$$$ theoryN -- Parse.tags) |-- args)) ||
- (Parse.$$$ theoryN -- Parse.tags) |-- Parse.!!! args;
+ (Parse.command_name theoryN -- Parse.tags) |-- args)) ||
+ (Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
-fun read pos str =
+fun token_source pos str =
+ str
+ |> Source.of_string_limited 8000
+ |> Symbol.source
+ |> Token.source {do_recover = NONE} (K header_lexicons) pos;
+
+fun read_source pos source =
let val res =
- str
- |> Source.of_string_limited 8000
- |> Symbol.source
- |> Token.source {do_recover = NONE} (fn () => (header_lexicon, Scan.empty_lexicon)) pos
+ source
|> Token.source_proper
|> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
|> Source.get_single;
@@ -138,4 +143,7 @@
| NONE => error ("Unexpected end of input" ^ Position.str_of pos))
end;
+fun read pos str = read_source pos (token_source pos str);
+fun read_tokens toks = read_source Position.none (Source.of_list toks);
+
end;
--- a/src/Pure/Thy/thy_info.ML Sun Aug 26 10:20:26 2012 +0200
+++ b/src/Pure/Thy/thy_info.ML Sun Aug 26 21:46:50 2012 +0200
@@ -17,9 +17,9 @@
val loaded_files: string -> Path.T list
val remove_thy: string -> unit
val kill_thy: string -> unit
- val use_thys_wrt: Path.T -> string list -> unit
- val use_thys: string list -> unit
- val use_thy: string -> unit
+ val use_thys_wrt: Path.T -> (string * Position.T) list -> unit
+ val use_thys: (string * Position.T) list -> unit
+ val use_thy: string * Position.T -> unit
val toplevel_begin_theory: Path.T -> Thy_Header.header -> theory
val register_thy: theory -> unit
val finish: unit -> unit
@@ -66,7 +66,7 @@
type deps =
{master: (Path.T * SHA1.digest), (*master dependencies for thy file*)
- imports: string list}; (*source specification of imports (partially qualified)*)
+ imports: (string * Position.T) list}; (*source specification of imports (partially qualified)*)
fun make_deps master imports : deps = {master = master, imports = imports};
@@ -220,18 +220,19 @@
fun required_by _ [] = ""
| required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
-fun load_thy initiators update_time deps text name uses keywords parents =
+fun load_thy initiators update_time deps text (name, pos) uses keywords parents =
let
val _ = kill_thy name;
val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
val {master = (thy_path, _), imports} = deps;
val dir = Path.dir thy_path;
- val pos = Path.position thy_path;
- val header = Thy_Header.make name imports keywords uses;
+ val header = Thy_Header.make (name, pos) imports keywords uses;
+
+ val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
val (theory, present) =
- Thy_Load.load_thy update_time dir header pos text
+ Thy_Load.load_thy update_time dir header (Path.position thy_path) text
(if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
fun commit () = update_thy deps theory;
in (theory, present, commit) end;
@@ -258,7 +259,7 @@
fun require_thys initiators dir strs tasks =
fold_map (require_thy initiators dir) strs tasks |>> forall I
-and require_thy initiators dir str tasks =
+and require_thy initiators dir (str, pos) tasks =
let
val path = Path.expand (Path.explode str);
val name = Path.implode (Path.base path);
@@ -273,9 +274,9 @@
val (current, deps, imports, uses, keywords) = check_deps dir' name
handle ERROR msg => cat_error msg
(loader_msg "the error(s) above occurred while examining theory" [name] ^
- required_by "\n" initiators);
+ Position.str_of pos ^ required_by "\n" initiators);
- val parents = map base_name imports;
+ val parents = map (base_name o #1) imports;
val (parents_current, tasks') =
require_thys (name :: initiators)
(Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
@@ -289,7 +290,7 @@
| SOME (dep, text) =>
let
val update_time = serial ();
- val load = load_thy initiators update_time dep text name uses keywords;
+ val load = load_thy initiators update_time dep text (name, pos) uses keywords;
in Task (parents, load) end);
val tasks'' = new_entry name parents task tasks';
@@ -312,11 +313,11 @@
fun toplevel_begin_theory master_dir (header: Thy_Header.header) =
let
- val {name, imports, ...} = header;
+ val {name = (name, _), imports, ...} = header;
val _ = kill_thy name;
val _ = use_thys_wrt master_dir imports;
val _ = Thy_Header.define_keywords header;
- val parents = map (get_theory o base_name) imports;
+ val parents = map (get_theory o base_name o fst) imports;
in Thy_Load.begin_theory master_dir header parents end;
--- a/src/Pure/Thy/thy_load.ML Sun Aug 26 10:20:26 2012 +0200
+++ b/src/Pure/Thy/thy_load.ML Sun Aug 26 21:46:50 2012 +0200
@@ -7,11 +7,11 @@
signature THY_LOAD =
sig
val master_directory: theory -> Path.T
- val imports_of: theory -> string list
+ val imports_of: theory -> (string * Position.T) list
val thy_path: Path.T -> Path.T
val parse_files: string -> (theory -> Token.file list) parser
val check_thy: Path.T -> string ->
- {master: Path.T * SHA1.digest, text: string, imports: string list,
+ {master: Path.T * SHA1.digest, text: string, imports: (string * Position.T) list,
uses: (Path.T * bool) list, keywords: Thy_Header.keywords}
val provide: Path.T * SHA1.digest -> theory -> theory
val provide_parse_files: string -> (theory -> Token.file list * theory) parser
@@ -35,7 +35,7 @@
type files =
{master_dir: Path.T, (*master directory of theory source*)
- imports: string list, (*source specification of imports*)
+ imports: (string * Position.T) list, (*source specification of imports*)
provided: (Path.T * SHA1.digest) list}; (*source path, digest*)
fun make_files (master_dir, imports, provided): files =
@@ -132,9 +132,10 @@
val master_file = check_file dir path;
val text = File.read master_file;
- val {name, imports, uses, keywords} = Thy_Header.read (Path.position master_file) text;
+ val {name = (name, pos), imports, uses, keywords} =
+ Thy_Header.read (Path.position master_file) text;
val _ = thy_name <> name andalso
- error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name);
+ error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.str_of pos);
in
{master = (master_file, SHA1.digest text), text = text,
imports = imports, uses = uses, keywords = keywords}
@@ -233,11 +234,11 @@
val thy = Toplevel.end_theory end_pos end_state;
in (flat results, thy) end;
-fun load_thy update_time master_dir header pos text parents =
+fun load_thy update_time master_dir header text_pos text parents =
let
val time = ! Toplevel.timing;
- val {name, uses, ...} = header;
+ val {name = (name, _), uses, ...} = header;
val _ = Thy_Header.define_keywords header;
val _ = Present.init_theory name;
fun init () =
@@ -246,7 +247,7 @@
val lexs = Keyword.get_lexicons ();
- val toks = Thy_Syntax.parse_tokens lexs pos text;
+ val toks = Thy_Syntax.parse_tokens lexs text_pos text;
val spans = map (resolve_files master_dir) (Thy_Syntax.parse_spans toks);
val elements = Thy_Syntax.parse_elements spans;
--- a/src/Pure/Thy/thy_output.ML Sun Aug 26 10:20:26 2012 +0200
+++ b/src/Pure/Thy/thy_output.ML Sun Aug 26 21:46:50 2012 +0200
@@ -532,8 +532,11 @@
fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
-fun pretty_theory ctxt name =
- (Theory.requires (Proof_Context.theory_of ctxt) name "presentation"; Pretty.str name);
+fun pretty_theory ctxt (name, pos) =
+ (case find_first (fn thy => Context.theory_name thy = name)
+ (Theory.nodes_of (Proof_Context.theory_of ctxt)) of
+ NONE => error ("No ancestor theory " ^ quote name ^ Position.str_of pos)
+ | SOME thy => (Position.report pos (Theory.get_markup thy); Pretty.str name));
(* default output *)
@@ -591,7 +594,7 @@
basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
- basic_entity (Binding.name "theory") (Scan.lift Args.name) pretty_theory #>
+ basic_entity (Binding.name "theory") (Scan.lift (Parse.position Args.name)) pretty_theory #>
basic_entities_style (Binding.name "thm_style")
(Term_Style.parse_bare -- Attrib.thms) pretty_thm_style #>
basic_entity (Binding.name "term_style")
--- a/src/Pure/theory.ML Sun Aug 26 10:20:26 2012 +0200
+++ b/src/Pure/theory.ML Sun Aug 26 21:46:50 2012 +0200
@@ -20,6 +20,7 @@
val checkpoint: theory -> theory
val copy: theory -> theory
val requires: theory -> string -> string -> unit
+ val get_markup: theory -> Markup.T
val axiom_space: theory -> Name_Space.T
val axiom_table: theory -> term Symtab.table
val axioms_of: theory -> (string * term) list
@@ -27,7 +28,7 @@
val defs_of: theory -> Defs.T
val at_begin: (theory -> theory option) -> theory -> theory
val at_end: (theory -> theory option) -> theory -> theory
- val begin_theory: string -> theory list -> theory
+ val begin_theory: string * Position.T -> theory list -> theory
val end_theory: theory -> theory
val add_axiom: Proof.context -> binding * term -> theory -> theory
val add_deps: Proof.context -> string -> string * typ -> (string * typ) list -> theory -> theory
@@ -80,42 +81,63 @@
perhaps (perhaps_loop (perhaps_apply (map fst wrappers)));
datatype thy = Thy of
- {axioms: term Name_Space.table,
+ {pos: Position.T,
+ id: serial,
+ axioms: term Name_Space.table,
defs: Defs.T,
wrappers: wrapper list * wrapper list};
-fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers};
+fun make_thy (pos, id, axioms, defs, wrappers) =
+ Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers};
structure Thy = Theory_Data_PP
(
type T = thy;
val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
- val empty = make_thy (empty_axioms, Defs.empty, ([], []));
+ val empty = make_thy (Position.none, 0, empty_axioms, Defs.empty, ([], []));
- fun extend (Thy {axioms = _, defs, wrappers}) = make_thy (empty_axioms, defs, wrappers);
+ fun extend (Thy {pos = _, id = _, axioms = _, defs, wrappers}) =
+ make_thy (Position.none, 0, empty_axioms, defs, wrappers);
fun merge pp (thy1, thy2) =
let
val ctxt = Syntax.init_pretty pp;
- val Thy {axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
- val Thy {axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
+ val Thy {pos = _, id = _, axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
+ val Thy {pos = _, id = _, axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
val axioms' = empty_axioms;
val defs' = Defs.merge ctxt (defs1, defs2);
val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
val ens' = Library.merge (eq_snd op =) (ens1, ens2);
- in make_thy (axioms', defs', (bgs', ens')) end;
+ in make_thy (Position.none, 0, axioms', defs', (bgs', ens')) end;
);
fun rep_theory thy = Thy.get thy |> (fn Thy args => args);
-fun map_thy f = Thy.map (fn (Thy {axioms, defs, wrappers}) =>
- make_thy (f (axioms, defs, wrappers)));
+fun map_thy f = Thy.map (fn (Thy {pos, id, axioms, defs, wrappers}) =>
+ make_thy (f (pos, id, axioms, defs, wrappers)));
+
+fun map_axioms f =
+ map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, f axioms, defs, wrappers));
+
+fun map_defs f =
+ map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, f defs, wrappers));
+
+fun map_wrappers f =
+ map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, defs, f wrappers));
-fun map_axioms f = map_thy (fn (axioms, defs, wrappers) => (f axioms, defs, wrappers));
-fun map_defs f = map_thy (fn (axioms, defs, wrappers) => (axioms, f defs, wrappers));
-fun map_wrappers f = map_thy (fn (axioms, defs, wrappers) => (axioms, defs, f wrappers));
+(* entity markup *)
+
+fun theory_markup def name id pos =
+ if id = 0 then Markup.empty
+ else
+ Markup.properties (Position.entity_properties_of def id pos)
+ (Isabelle_Markup.entity Isabelle_Markup.theoryN name);
+
+fun get_markup thy =
+ let val {pos, id, ...} = rep_theory thy
+ in theory_markup false (Context.theory_name thy) id pos end;
(* basic operations *)
@@ -137,12 +159,17 @@
fun at_begin f = map_wrappers (apfst (cons (f, stamp ())));
fun at_end f = map_wrappers (apsnd (cons (f, stamp ())));
-fun begin_theory name imports =
+fun begin_theory (name, pos) imports =
if name = Context.PureN then
(case imports of [thy] => thy | _ => error "Bad bootstrapping of theory Pure")
else
let
- val thy = Context.begin_thy Context.pretty_global name imports;
+ val id = serial ();
+ val thy =
+ Context.begin_thy Context.pretty_global name imports
+ |> map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers));
+ val _ = Position.report pos (theory_markup true name id pos);
+
val wrappers = begin_wrappers thy;
in
thy