theory def/ref position reports, which enable hyperlinks etc.;
authorwenzelm
Sun Aug 26 21:46:50 2012 +0200 (2012-08-26)
changeset 48927ef462b5558eb
parent 48926 8d7778a19857
child 48928 698fb0e27b11
theory def/ref position reports, which enable hyperlinks etc.;
more official header command parsing;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/parse.ML
src/Pure/ML/ml_antiquote.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/isabelle_markup.ML
src/Pure/PIDE/protocol.ML
src/Pure/ProofGeneral/pgip_parser.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/ROOT.ML
src/Pure/System/build.ML
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_load.ML
src/Pure/Thy/thy_output.ML
src/Pure/theory.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Aug 26 10:20:26 2012 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Aug 26 21:46:50 2012 +0200
     1.3 @@ -934,7 +934,7 @@
     1.4  
     1.5  val _ =
     1.6    Outer_Syntax.improper_command @{command_spec "use_thy"} "use theory file"
     1.7 -    (Parse.name >> (fn name =>
     1.8 +    (Parse.position Parse.name >> (fn name =>
     1.9        Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.use_thy name)));
    1.10  
    1.11  val _ =
     2.1 --- a/src/Pure/Isar/parse.ML	Sun Aug 26 10:20:26 2012 +0200
     2.2 +++ b/src/Pure/Isar/parse.ML	Sun Aug 26 21:46:50 2012 +0200
     2.3 @@ -34,6 +34,7 @@
     2.4    val verbatim: string parser
     2.5    val sync: string parser
     2.6    val eof: string parser
     2.7 +  val command_name: string -> string parser
     2.8    val keyword_with: (string -> bool) -> string parser
     2.9    val keyword_ident_or_symbolic: string parser
    2.10    val $$$ : string -> string parser
    2.11 @@ -190,6 +191,11 @@
    2.12  fun keyword_with pred = RESET_VALUE (Scan.one (Token.keyword_with pred) >> Token.content_of);
    2.13  val keyword_ident_or_symbolic = keyword_with Token.ident_or_symbolic;
    2.14  
    2.15 +fun command_name x =
    2.16 +  group (fn () => Token.str_of_kind Token.Command ^ " " ^ quote x)
    2.17 +    (RESET_VALUE (Scan.one (fn tok => Token.is_command tok andalso Token.content_of tok = x)))
    2.18 +  >> Token.content_of;
    2.19 +
    2.20  fun $$$ x =
    2.21    group (fn () => Token.str_of_kind Token.Keyword ^ " " ^ quote x)
    2.22      (keyword_with (fn y => x = y));
     3.1 --- a/src/Pure/ML/ml_antiquote.ML	Sun Aug 26 10:20:26 2012 +0200
     3.2 +++ b/src/Pure/ML/ml_antiquote.ML	Sun Aug 26 21:46:50 2012 +0200
     3.3 @@ -71,8 +71,9 @@
     3.4      (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
     3.5  
     3.6    value (Binding.name "theory")
     3.7 -    (Scan.lift Args.name >> (fn name =>
     3.8 -      "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name)
     3.9 +    (Args.theory -- Scan.lift (Parse.position Args.name) >> (fn (thy, (name, pos)) =>
    3.10 +      (Position.report pos (Theory.get_markup (Context.get_theory thy name));
    3.11 +        "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
    3.12      || Scan.succeed "Proof_Context.theory_of ML_context") #>
    3.13  
    3.14    inline (Binding.name "context") (Scan.succeed "Isabelle.ML_context") #>
     4.1 --- a/src/Pure/PIDE/document.ML	Sun Aug 26 10:20:26 2012 +0200
     4.2 +++ b/src/Pure/PIDE/document.ML	Sun Aug 26 21:46:50 2012 +0200
     4.3 @@ -83,7 +83,7 @@
     4.4  fun make_perspective command_ids : perspective =
     4.5    (Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
     4.6  
     4.7 -val no_header = ("", Thy_Header.make "" [] [] [], ["Bad theory header"]);
     4.8 +val no_header = ("", Thy_Header.make ("", Position.none) [] [] [], ["Bad theory header"]);
     4.9  val no_perspective = make_perspective [];
    4.10  
    4.11  val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
    4.12 @@ -92,12 +92,18 @@
    4.13  
    4.14  (* basic components *)
    4.15  
    4.16 +fun set_header header =
    4.17 +  map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
    4.18 +
    4.19  fun get_header (Node {header = (master, header, errors), ...}) =
    4.20    if null errors then (master, header)
    4.21    else error (cat_lines errors);
    4.22  
    4.23 -fun set_header header =
    4.24 -  map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
    4.25 +fun read_header node span =
    4.26 +  let
    4.27 +    val (dir, {name = (name, _), imports, keywords, uses}) = get_header node;
    4.28 +    val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
    4.29 +  in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords uses) end;
    4.30  
    4.31  fun get_perspective (Node {perspective, ...}) = perspective;
    4.32  fun set_perspective ids =
    4.33 @@ -183,17 +189,18 @@
    4.34      | Edits edits => update_node name (edit_node edits) nodes
    4.35      | Deps (master, header, errors) =>
    4.36          let
    4.37 +          val imports = map fst (#imports header);
    4.38            val errors1 =
    4.39              (Thy_Header.define_keywords header; errors)
    4.40                handle ERROR msg => errors @ [msg];
    4.41            val nodes1 = nodes
    4.42              |> default_node name
    4.43 -            |> fold default_node (#imports header);
    4.44 +            |> fold default_node imports;
    4.45            val nodes2 = nodes1
    4.46              |> Graph.Keys.fold
    4.47                  (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
    4.48            val (nodes3, errors2) =
    4.49 -            (Graph.add_deps_acyclic (name, #imports header) nodes2, errors1)
    4.50 +            (Graph.add_deps_acyclic (name, imports) nodes2, errors1)
    4.51                handle Graph.CYCLES cs => (nodes2, errors1 @ map cycle_msg cs);
    4.52          in Graph.map_node name (set_header (master, header, errors2)) nodes3 end
    4.53      | Perspective perspective => update_node name (set_perspective perspective) nodes);
    4.54 @@ -373,16 +380,17 @@
    4.55            Symtab.update (a, ())) all_visible Symtab.empty;
    4.56    in Symtab.defined required end;
    4.57  
    4.58 -fun init_theory imports node =
    4.59 +fun init_theory deps node span =
    4.60    let
    4.61      (* FIXME provide files via Scala layer, not master_dir *)
    4.62 -    val (dir, header) = get_header node;
    4.63 +    val (dir, header) = read_header node span;
    4.64      val master_dir =
    4.65        (case try Url.explode dir of
    4.66          SOME (Url.File path) => path
    4.67        | _ => Path.current);
    4.68 +    val imports = #imports header;
    4.69      val parents =
    4.70 -      #imports header |> map (fn import =>
    4.71 +      imports |> map (fn (import, _) =>
    4.72          (case Thy_Info.lookup_theory import of
    4.73            SOME thy => thy
    4.74          | NONE =>
    4.75 @@ -390,7 +398,8 @@
    4.76                (fst (fst
    4.77                  (Command.memo_result
    4.78                    (the_default no_exec
    4.79 -                    (get_result (snd (the (AList.lookup (op =) imports import))))))))));
    4.80 +                    (get_result (snd (the (AList.lookup (op =) deps import))))))))));
    4.81 +    val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
    4.82    in Thy_Load.begin_theory master_dir header parents end;
    4.83  
    4.84  fun check_theory full name node =
    4.85 @@ -429,7 +438,7 @@
    4.86      else (common, flags)
    4.87    end;
    4.88  
    4.89 -fun illegal_init () = error "Illegal theory header after end of theory";
    4.90 +fun illegal_init _ = error "Illegal theory header after end of theory";
    4.91  
    4.92  fun new_exec state proper_init command_id' (execs, command_exec, init) =
    4.93    if not proper_init andalso is_none init then NONE
    4.94 @@ -438,7 +447,7 @@
    4.95        val (name, span) = the_command state command_id' ||> Lazy.force;
    4.96        val (modify_init, init') =
    4.97          if Keyword.is_theory_begin name then
    4.98 -          (Toplevel.modify_init (the_default illegal_init init), NONE)
    4.99 +          (Toplevel.modify_init (fn () => the_default illegal_init init span), NONE)
   4.100          else (I, init);
   4.101        val exec_id' = new_id ();
   4.102        val exec_id'_string = print_id exec_id';
   4.103 @@ -487,7 +496,7 @@
   4.104                  then
   4.105                    let
   4.106                      val node0 = node_of old_version name;
   4.107 -                    fun init () = init_theory imports node;
   4.108 +                    val init = init_theory imports node;
   4.109                      val proper_init =
   4.110                        check_theory false name node andalso
   4.111                        forall (fn (name, (_, node)) => check_theory true name node) imports;
     5.1 --- a/src/Pure/PIDE/isabelle_markup.ML	Sun Aug 26 10:20:26 2012 +0200
     5.2 +++ b/src/Pure/PIDE/isabelle_markup.ML	Sun Aug 26 21:46:50 2012 +0200
     5.3 @@ -26,6 +26,7 @@
     5.4    val breakN: string val break: int -> Markup.T
     5.5    val fbreakN: string val fbreak: Markup.T
     5.6    val hiddenN: string val hidden: Markup.T
     5.7 +  val theoryN: string
     5.8    val classN: string
     5.9    val type_nameN: string
    5.10    val constantN: string
    5.11 @@ -165,6 +166,7 @@
    5.12  
    5.13  (* logical entities *)
    5.14  
    5.15 +val theoryN = "theory";
    5.16  val classN = "class";
    5.17  val type_nameN = "type name";
    5.18  val constantN = "constant";
     6.1 --- a/src/Pure/PIDE/protocol.ML	Sun Aug 26 10:20:26 2012 +0200
     6.2 +++ b/src/Pure/PIDE/protocol.ML	Sun Aug 26 21:46:50 2012 +0200
     6.3 @@ -42,10 +42,11 @@
     6.4                            (pair (list (pair string
     6.5                              (option (pair (pair string (list string)) (list string)))))
     6.6                              (pair (list (pair string bool)) (list string))))) a;
     6.7 +                      val imports' = map (rpair Position.none) imports;
     6.8                        val (uses', errors') =
     6.9                          (map (apfst Path.explode) uses, errors)
    6.10                            handle ERROR msg => ([], errors @ [msg]);
    6.11 -                      val header = Thy_Header.make name imports keywords uses';
    6.12 +                      val header = Thy_Header.make (name, Position.none) imports' keywords uses';
    6.13                      in Document.Deps (master, header, errors') end,
    6.14                    fn (a, []) => Document.Perspective (map int_atom a)]))
    6.15              end;
     7.1 --- a/src/Pure/ProofGeneral/pgip_parser.ML	Sun Aug 26 10:20:26 2012 +0200
     7.2 +++ b/src/Pure/ProofGeneral/pgip_parser.ML	Sun Aug 26 21:46:50 2012 +0200
     7.3 @@ -21,8 +21,8 @@
     7.4  fun thy_begin text =
     7.5    (case try (Thy_Header.read Position.none) text of
     7.6      NONE => D.Opentheory {thyname = NONE, parentnames = [], text = text}
     7.7 -  | SOME {name, imports, ...} =>
     7.8 -       D.Opentheory {thyname = SOME name, parentnames = imports, text = text})
     7.9 +  | SOME {name = (name, _), imports, ...} =>
    7.10 +       D.Opentheory {thyname = SOME name, parentnames = map #1 imports, text = text})
    7.11    :: [D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}];
    7.12  
    7.13  fun thy_heading text =
     8.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Aug 26 10:20:26 2012 +0200
     8.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Aug 26 21:46:50 2012 +0200
     8.3 @@ -601,7 +601,7 @@
     8.4              end
     8.5  
     8.6          fun thyrefs thy =
     8.7 -            let val thyrefs = #imports (Thy_Load.check_thy Path.current thy)
     8.8 +            let val thyrefs = map #1 (#imports (Thy_Load.check_thy Path.current thy))
     8.9              in
    8.10                  issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
    8.11                                       name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,
     9.1 --- a/src/Pure/ROOT.ML	Sun Aug 26 10:20:26 2012 +0200
     9.2 +++ b/src/Pure/ROOT.ML	Sun Aug 26 21:46:50 2012 +0200
     9.3 @@ -306,7 +306,7 @@
     9.4  (* the Pure theory *)
     9.5  
     9.6  use "pure_syn.ML";
     9.7 -Thy_Info.use_thy "Pure";
     9.8 +Thy_Info.use_thy ("Pure", Position.none);
     9.9  Context.set_thread_data NONE;
    9.10  structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
    9.11  
    9.12 @@ -341,8 +341,8 @@
    9.13  
    9.14  fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));
    9.15  
    9.16 -fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
    9.17 -fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
    9.18 +fun use_thys args = Toplevel.program (fn () => Thy_Info.use_thys (map (rpair Position.none) args));
    9.19 +val use_thy = use_thys o single;
    9.20  
    9.21  val cd = File.cd o Path.explode;
    9.22  
    10.1 --- a/src/Pure/System/build.ML	Sun Aug 26 10:20:26 2012 +0200
    10.2 +++ b/src/Pure/System/build.ML	Sun Aug 26 21:46:50 2012 +0200
    10.3 @@ -47,7 +47,7 @@
    10.4  fun use_theories (options, thys) =
    10.5    let val condition = space_explode "," (Options.string options "condition") in
    10.6      (case filter_out (can getenv_strict) condition of
    10.7 -      [] => use_thys options thys
    10.8 +      [] => use_thys options (map (rpair Position.none) thys)
    10.9      | conds =>
   10.10          Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
   10.11            " (undefined " ^ commas conds ^ ")\n"))
    11.1 --- a/src/Pure/Thy/thy_header.ML	Sun Aug 26 10:20:26 2012 +0200
    11.2 +++ b/src/Pure/Thy/thy_header.ML	Sun Aug 26 21:46:50 2012 +0200
    11.3 @@ -8,16 +8,18 @@
    11.4  sig
    11.5    type keywords = (string * Keyword.spec option) list
    11.6    type header =
    11.7 -   {name: string,
    11.8 -    imports: string list,
    11.9 +   {name: string * Position.T,
   11.10 +    imports: (string * Position.T) list,
   11.11      keywords: keywords,
   11.12      uses: (Path.T * bool) list}
   11.13 -  val make: string -> string list -> keywords -> (Path.T * bool) list -> header
   11.14 +  val make: string * Position.T -> (string * Position.T) list -> keywords ->
   11.15 +    (Path.T * bool) list -> header
   11.16    val define_keywords: header -> unit
   11.17    val declare_keyword: string * Keyword.spec option -> theory -> theory
   11.18    val the_keyword: theory -> string -> Keyword.spec option
   11.19    val args: header parser
   11.20    val read: Position.T -> string -> header
   11.21 +  val read_tokens: Token.T list -> header
   11.22  end;
   11.23  
   11.24  structure Thy_Header: THY_HEADER =
   11.25 @@ -26,8 +28,8 @@
   11.26  type keywords = (string * Keyword.spec option) list;
   11.27  
   11.28  type header =
   11.29 - {name: string,
   11.30 -  imports: string list,
   11.31 + {name: string * Position.T,
   11.32 +  imports: (string * Position.T) list,
   11.33    keywords: keywords,
   11.34    uses: (Path.T * bool) list};
   11.35  
   11.36 @@ -74,10 +76,10 @@
   11.37  val usesN = "uses";
   11.38  val beginN = "begin";
   11.39  
   11.40 -val header_lexicon =
   11.41 -  Scan.make_lexicon
   11.42 -    (map Symbol.explode
   11.43 -      ["%", "(", ")", ",", "::", ";", "and", beginN, headerN, importsN, keywordsN, theoryN, usesN]);
   11.44 +val header_lexicons =
   11.45 +  pairself (Scan.make_lexicon o map Symbol.explode)
   11.46 +   (["%", "(", ")", ",", "::", ";", "and", beginN, importsN, keywordsN, usesN],
   11.47 +    [headerN, theoryN]);
   11.48  
   11.49  
   11.50  (* header args *)
   11.51 @@ -85,7 +87,7 @@
   11.52  local
   11.53  
   11.54  val file_name = Parse.group (fn () => "file name") Parse.path >> Path.explode;
   11.55 -val theory_name = Parse.group (fn () => "theory name") Parse.name;
   11.56 +val theory_name = Parse.group (fn () => "theory name") (Parse.position Parse.name);
   11.57  
   11.58  val opt_files =
   11.59    Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
   11.60 @@ -118,17 +120,20 @@
   11.61  (* read header *)
   11.62  
   11.63  val header =
   11.64 -  (Parse.$$$ headerN -- Parse.tags) |--
   11.65 +  (Parse.command_name headerN -- Parse.tags) |--
   11.66      (Parse.!!! (Parse.doc_source -- Scan.repeat Parse.semicolon --
   11.67 -      (Parse.$$$ theoryN -- Parse.tags) |-- args)) ||
   11.68 -  (Parse.$$$ theoryN -- Parse.tags) |-- Parse.!!! args;
   11.69 +      (Parse.command_name theoryN -- Parse.tags) |-- args)) ||
   11.70 +  (Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
   11.71  
   11.72 -fun read pos str =
   11.73 +fun token_source pos str =
   11.74 +  str
   11.75 +  |> Source.of_string_limited 8000
   11.76 +  |> Symbol.source
   11.77 +  |> Token.source {do_recover = NONE} (K header_lexicons) pos;
   11.78 +
   11.79 +fun read_source pos source =
   11.80    let val res =
   11.81 -    str
   11.82 -    |> Source.of_string_limited 8000
   11.83 -    |> Symbol.source
   11.84 -    |> Token.source {do_recover = NONE} (fn () => (header_lexicon, Scan.empty_lexicon)) pos
   11.85 +    source
   11.86      |> Token.source_proper
   11.87      |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
   11.88      |> Source.get_single;
   11.89 @@ -138,4 +143,7 @@
   11.90      | NONE => error ("Unexpected end of input" ^ Position.str_of pos))
   11.91    end;
   11.92  
   11.93 +fun read pos str = read_source pos (token_source pos str);
   11.94 +fun read_tokens toks = read_source Position.none (Source.of_list toks);
   11.95 +
   11.96  end;
    12.1 --- a/src/Pure/Thy/thy_info.ML	Sun Aug 26 10:20:26 2012 +0200
    12.2 +++ b/src/Pure/Thy/thy_info.ML	Sun Aug 26 21:46:50 2012 +0200
    12.3 @@ -17,9 +17,9 @@
    12.4    val loaded_files: string -> Path.T list
    12.5    val remove_thy: string -> unit
    12.6    val kill_thy: string -> unit
    12.7 -  val use_thys_wrt: Path.T -> string list -> unit
    12.8 -  val use_thys: string list -> unit
    12.9 -  val use_thy: string -> unit
   12.10 +  val use_thys_wrt: Path.T -> (string * Position.T) list -> unit
   12.11 +  val use_thys: (string * Position.T) list -> unit
   12.12 +  val use_thy: string * Position.T -> unit
   12.13    val toplevel_begin_theory: Path.T -> Thy_Header.header -> theory
   12.14    val register_thy: theory -> unit
   12.15    val finish: unit -> unit
   12.16 @@ -66,7 +66,7 @@
   12.17  
   12.18  type deps =
   12.19   {master: (Path.T * SHA1.digest),  (*master dependencies for thy file*)
   12.20 -  imports: string list};  (*source specification of imports (partially qualified)*)
   12.21 +  imports: (string * Position.T) list};  (*source specification of imports (partially qualified)*)
   12.22  
   12.23  fun make_deps master imports : deps = {master = master, imports = imports};
   12.24  
   12.25 @@ -220,18 +220,19 @@
   12.26  fun required_by _ [] = ""
   12.27    | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
   12.28  
   12.29 -fun load_thy initiators update_time deps text name uses keywords parents =
   12.30 +fun load_thy initiators update_time deps text (name, pos) uses keywords parents =
   12.31    let
   12.32      val _ = kill_thy name;
   12.33      val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
   12.34  
   12.35      val {master = (thy_path, _), imports} = deps;
   12.36      val dir = Path.dir thy_path;
   12.37 -    val pos = Path.position thy_path;
   12.38 -    val header = Thy_Header.make name imports keywords uses;
   12.39 +    val header = Thy_Header.make (name, pos) imports keywords uses;
   12.40 +
   12.41 +    val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
   12.42  
   12.43      val (theory, present) =
   12.44 -      Thy_Load.load_thy update_time dir header pos text
   12.45 +      Thy_Load.load_thy update_time dir header (Path.position thy_path) text
   12.46          (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
   12.47      fun commit () = update_thy deps theory;
   12.48    in (theory, present, commit) end;
   12.49 @@ -258,7 +259,7 @@
   12.50  
   12.51  fun require_thys initiators dir strs tasks =
   12.52        fold_map (require_thy initiators dir) strs tasks |>> forall I
   12.53 -and require_thy initiators dir str tasks =
   12.54 +and require_thy initiators dir (str, pos) tasks =
   12.55    let
   12.56      val path = Path.expand (Path.explode str);
   12.57      val name = Path.implode (Path.base path);
   12.58 @@ -273,9 +274,9 @@
   12.59            val (current, deps, imports, uses, keywords) = check_deps dir' name
   12.60              handle ERROR msg => cat_error msg
   12.61                (loader_msg "the error(s) above occurred while examining theory" [name] ^
   12.62 -                required_by "\n" initiators);
   12.63 +                Position.str_of pos ^ required_by "\n" initiators);
   12.64  
   12.65 -          val parents = map base_name imports;
   12.66 +          val parents = map (base_name o #1) imports;
   12.67            val (parents_current, tasks') =
   12.68              require_thys (name :: initiators)
   12.69                (Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
   12.70 @@ -289,7 +290,7 @@
   12.71                | SOME (dep, text) =>
   12.72                    let
   12.73                      val update_time = serial ();
   12.74 -                    val load = load_thy initiators update_time dep text name uses keywords;
   12.75 +                    val load = load_thy initiators update_time dep text (name, pos) uses keywords;
   12.76                    in Task (parents, load) end);
   12.77  
   12.78            val tasks'' = new_entry name parents task tasks';
   12.79 @@ -312,11 +313,11 @@
   12.80  
   12.81  fun toplevel_begin_theory master_dir (header: Thy_Header.header) =
   12.82    let
   12.83 -    val {name, imports, ...} = header;
   12.84 +    val {name = (name, _), imports, ...} = header;
   12.85      val _ = kill_thy name;
   12.86      val _ = use_thys_wrt master_dir imports;
   12.87      val _ = Thy_Header.define_keywords header;
   12.88 -    val parents = map (get_theory o base_name) imports;
   12.89 +    val parents = map (get_theory o base_name o fst) imports;
   12.90    in Thy_Load.begin_theory master_dir header parents end;
   12.91  
   12.92  
    13.1 --- a/src/Pure/Thy/thy_load.ML	Sun Aug 26 10:20:26 2012 +0200
    13.2 +++ b/src/Pure/Thy/thy_load.ML	Sun Aug 26 21:46:50 2012 +0200
    13.3 @@ -7,11 +7,11 @@
    13.4  signature THY_LOAD =
    13.5  sig
    13.6    val master_directory: theory -> Path.T
    13.7 -  val imports_of: theory -> string list
    13.8 +  val imports_of: theory -> (string * Position.T) list
    13.9    val thy_path: Path.T -> Path.T
   13.10    val parse_files: string -> (theory -> Token.file list) parser
   13.11    val check_thy: Path.T -> string ->
   13.12 -   {master: Path.T * SHA1.digest, text: string, imports: string list,
   13.13 +   {master: Path.T * SHA1.digest, text: string, imports: (string * Position.T) list,
   13.14      uses: (Path.T * bool) list, keywords: Thy_Header.keywords}
   13.15    val provide: Path.T * SHA1.digest -> theory -> theory
   13.16    val provide_parse_files: string -> (theory -> Token.file list * theory) parser
   13.17 @@ -35,7 +35,7 @@
   13.18  
   13.19  type files =
   13.20   {master_dir: Path.T,  (*master directory of theory source*)
   13.21 -  imports: string list,  (*source specification of imports*)
   13.22 +  imports: (string * Position.T) list,  (*source specification of imports*)
   13.23    provided: (Path.T * SHA1.digest) list};  (*source path, digest*)
   13.24  
   13.25  fun make_files (master_dir, imports, provided): files =
   13.26 @@ -132,9 +132,10 @@
   13.27      val master_file = check_file dir path;
   13.28      val text = File.read master_file;
   13.29  
   13.30 -    val {name, imports, uses, keywords} = Thy_Header.read (Path.position master_file) text;
   13.31 +    val {name = (name, pos), imports, uses, keywords} =
   13.32 +      Thy_Header.read (Path.position master_file) text;
   13.33      val _ = thy_name <> name andalso
   13.34 -      error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name);
   13.35 +      error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.str_of pos);
   13.36    in
   13.37     {master = (master_file, SHA1.digest text), text = text,
   13.38      imports = imports, uses = uses, keywords = keywords}
   13.39 @@ -233,11 +234,11 @@
   13.40      val thy = Toplevel.end_theory end_pos end_state;
   13.41    in (flat results, thy) end;
   13.42  
   13.43 -fun load_thy update_time master_dir header pos text parents =
   13.44 +fun load_thy update_time master_dir header text_pos text parents =
   13.45    let
   13.46      val time = ! Toplevel.timing;
   13.47  
   13.48 -    val {name, uses, ...} = header;
   13.49 +    val {name = (name, _), uses, ...} = header;
   13.50      val _ = Thy_Header.define_keywords header;
   13.51      val _ = Present.init_theory name;
   13.52      fun init () =
   13.53 @@ -246,7 +247,7 @@
   13.54  
   13.55      val lexs = Keyword.get_lexicons ();
   13.56  
   13.57 -    val toks = Thy_Syntax.parse_tokens lexs pos text;
   13.58 +    val toks = Thy_Syntax.parse_tokens lexs text_pos text;
   13.59      val spans = map (resolve_files master_dir) (Thy_Syntax.parse_spans toks);
   13.60      val elements = Thy_Syntax.parse_elements spans;
   13.61  
    14.1 --- a/src/Pure/Thy/thy_output.ML	Sun Aug 26 10:20:26 2012 +0200
    14.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Aug 26 21:46:50 2012 +0200
    14.3 @@ -532,8 +532,11 @@
    14.4  
    14.5  fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
    14.6  
    14.7 -fun pretty_theory ctxt name =
    14.8 -  (Theory.requires (Proof_Context.theory_of ctxt) name "presentation"; Pretty.str name);
    14.9 +fun pretty_theory ctxt (name, pos) =
   14.10 +  (case find_first (fn thy => Context.theory_name thy = name)
   14.11 +      (Theory.nodes_of (Proof_Context.theory_of ctxt)) of
   14.12 +    NONE => error ("No ancestor theory " ^ quote name ^ Position.str_of pos)
   14.13 +  | SOME thy => (Position.report pos (Theory.get_markup thy); Pretty.str name));
   14.14  
   14.15  
   14.16  (* default output *)
   14.17 @@ -591,7 +594,7 @@
   14.18      basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
   14.19      basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>
   14.20      basic_entities (Binding.name "full_prf") Attrib.thms (pretty_prf true) #>
   14.21 -    basic_entity (Binding.name "theory") (Scan.lift Args.name) pretty_theory #>
   14.22 +    basic_entity (Binding.name "theory") (Scan.lift (Parse.position Args.name)) pretty_theory #>
   14.23      basic_entities_style (Binding.name "thm_style")
   14.24        (Term_Style.parse_bare -- Attrib.thms) pretty_thm_style #>
   14.25      basic_entity (Binding.name "term_style")
    15.1 --- a/src/Pure/theory.ML	Sun Aug 26 10:20:26 2012 +0200
    15.2 +++ b/src/Pure/theory.ML	Sun Aug 26 21:46:50 2012 +0200
    15.3 @@ -20,6 +20,7 @@
    15.4    val checkpoint: theory -> theory
    15.5    val copy: theory -> theory
    15.6    val requires: theory -> string -> string -> unit
    15.7 +  val get_markup: theory -> Markup.T
    15.8    val axiom_space: theory -> Name_Space.T
    15.9    val axiom_table: theory -> term Symtab.table
   15.10    val axioms_of: theory -> (string * term) list
   15.11 @@ -27,7 +28,7 @@
   15.12    val defs_of: theory -> Defs.T
   15.13    val at_begin: (theory -> theory option) -> theory -> theory
   15.14    val at_end: (theory -> theory option) -> theory -> theory
   15.15 -  val begin_theory: string -> theory list -> theory
   15.16 +  val begin_theory: string * Position.T -> theory list -> theory
   15.17    val end_theory: theory -> theory
   15.18    val add_axiom: Proof.context -> binding * term -> theory -> theory
   15.19    val add_deps: Proof.context -> string -> string * typ -> (string * typ) list -> theory -> theory
   15.20 @@ -80,42 +81,63 @@
   15.21    perhaps (perhaps_loop (perhaps_apply (map fst wrappers)));
   15.22  
   15.23  datatype thy = Thy of
   15.24 - {axioms: term Name_Space.table,
   15.25 + {pos: Position.T,
   15.26 +  id: serial,
   15.27 +  axioms: term Name_Space.table,
   15.28    defs: Defs.T,
   15.29    wrappers: wrapper list * wrapper list};
   15.30  
   15.31 -fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers};
   15.32 +fun make_thy (pos, id, axioms, defs, wrappers) =
   15.33 +  Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers};
   15.34  
   15.35  structure Thy = Theory_Data_PP
   15.36  (
   15.37    type T = thy;
   15.38    val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
   15.39 -  val empty = make_thy (empty_axioms, Defs.empty, ([], []));
   15.40 +  val empty = make_thy (Position.none, 0, empty_axioms, Defs.empty, ([], []));
   15.41  
   15.42 -  fun extend (Thy {axioms = _, defs, wrappers}) = make_thy (empty_axioms, defs, wrappers);
   15.43 +  fun extend (Thy {pos = _, id = _, axioms = _, defs, wrappers}) =
   15.44 +    make_thy (Position.none, 0, empty_axioms, defs, wrappers);
   15.45  
   15.46    fun merge pp (thy1, thy2) =
   15.47      let
   15.48        val ctxt = Syntax.init_pretty pp;
   15.49 -      val Thy {axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
   15.50 -      val Thy {axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
   15.51 +      val Thy {pos = _, id = _, axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
   15.52 +      val Thy {pos = _, id = _, axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
   15.53  
   15.54        val axioms' = empty_axioms;
   15.55        val defs' = Defs.merge ctxt (defs1, defs2);
   15.56        val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
   15.57        val ens' = Library.merge (eq_snd op =) (ens1, ens2);
   15.58 -    in make_thy (axioms', defs', (bgs', ens')) end;
   15.59 +    in make_thy (Position.none, 0, axioms', defs', (bgs', ens')) end;
   15.60  );
   15.61  
   15.62  fun rep_theory thy = Thy.get thy |> (fn Thy args => args);
   15.63  
   15.64 -fun map_thy f = Thy.map (fn (Thy {axioms, defs, wrappers}) =>
   15.65 -  make_thy (f (axioms, defs, wrappers)));
   15.66 +fun map_thy f = Thy.map (fn (Thy {pos, id, axioms, defs, wrappers}) =>
   15.67 +  make_thy (f (pos, id, axioms, defs, wrappers)));
   15.68 +
   15.69 +fun map_axioms f =
   15.70 +  map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, f axioms, defs, wrappers));
   15.71 +
   15.72 +fun map_defs f =
   15.73 +  map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, f defs, wrappers));
   15.74 +
   15.75 +fun map_wrappers f =
   15.76 +  map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, defs, f wrappers));
   15.77  
   15.78  
   15.79 -fun map_axioms f = map_thy (fn (axioms, defs, wrappers) => (f axioms, defs, wrappers));
   15.80 -fun map_defs f = map_thy (fn (axioms, defs, wrappers) => (axioms, f defs, wrappers));
   15.81 -fun map_wrappers f = map_thy (fn (axioms, defs, wrappers) => (axioms, defs, f wrappers));
   15.82 +(* entity markup *)
   15.83 +
   15.84 +fun theory_markup def name id pos =
   15.85 +  if id = 0 then Markup.empty
   15.86 +  else
   15.87 +    Markup.properties (Position.entity_properties_of def id pos)
   15.88 +      (Isabelle_Markup.entity Isabelle_Markup.theoryN name);
   15.89 +
   15.90 +fun get_markup thy =
   15.91 +  let val {pos, id, ...} = rep_theory thy
   15.92 +  in theory_markup false (Context.theory_name thy) id pos end;
   15.93  
   15.94  
   15.95  (* basic operations *)
   15.96 @@ -137,12 +159,17 @@
   15.97  fun at_begin f = map_wrappers (apfst (cons (f, stamp ())));
   15.98  fun at_end f = map_wrappers (apsnd (cons (f, stamp ())));
   15.99  
  15.100 -fun begin_theory name imports =
  15.101 +fun begin_theory (name, pos) imports =
  15.102    if name = Context.PureN then
  15.103      (case imports of [thy] => thy | _ => error "Bad bootstrapping of theory Pure")
  15.104    else
  15.105      let
  15.106 -      val thy = Context.begin_thy Context.pretty_global name imports;
  15.107 +      val id = serial ();
  15.108 +      val thy =
  15.109 +        Context.begin_thy Context.pretty_global name imports
  15.110 +        |> map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers));
  15.111 +      val _ = Position.report pos (theory_markup true name id pos);
  15.112 +
  15.113        val wrappers = begin_wrappers thy;
  15.114      in
  15.115        thy