# HG changeset patch
# User wenzelm
# Date 1346010410 -7200
# Node ID ef462b5558ebed5b2991e0c020712a7c8349c122
# Parent  8d7778a1985702baedc450aa3ff59e6cced8f5ed
theory def/ref position reports, which enable hyperlinks etc.;
more official header command parsing;

diff -r 8d7778a19857 -r ef462b5558eb src/Pure/Isar/isar_syn.ML
--- 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 _ =
diff -r 8d7778a19857 -r ef462b5558eb src/Pure/Isar/parse.ML
--- 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));
diff -r 8d7778a19857 -r ef462b5558eb src/Pure/ML/ml_antiquote.ML
--- 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") #>
diff -r 8d7778a19857 -r ef462b5558eb src/Pure/PIDE/document.ML
--- 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;
diff -r 8d7778a19857 -r ef462b5558eb src/Pure/PIDE/isabelle_markup.ML
--- 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";
diff -r 8d7778a19857 -r ef462b5558eb src/Pure/PIDE/protocol.ML
--- 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;
diff -r 8d7778a19857 -r ef462b5558eb src/Pure/ProofGeneral/pgip_parser.ML
--- 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 =
diff -r 8d7778a19857 -r ef462b5558eb src/Pure/ProofGeneral/proof_general_pgip.ML
--- 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,
diff -r 8d7778a19857 -r ef462b5558eb src/Pure/ROOT.ML
--- 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;
 
diff -r 8d7778a19857 -r ef462b5558eb src/Pure/System/build.ML
--- 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"))
diff -r 8d7778a19857 -r ef462b5558eb src/Pure/Thy/thy_header.ML
--- 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;
diff -r 8d7778a19857 -r ef462b5558eb src/Pure/Thy/thy_info.ML
--- 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;
 
 
diff -r 8d7778a19857 -r ef462b5558eb src/Pure/Thy/thy_load.ML
--- 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;
 
diff -r 8d7778a19857 -r ef462b5558eb src/Pure/Thy/thy_output.ML
--- 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")
diff -r 8d7778a19857 -r ef462b5558eb src/Pure/theory.ML
--- 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