# HG changeset patch
# User wenzelm
# Date 1346012590 -7200
# Node ID 05d4e5f660aefce08a6300a619d0c5e514f473c3
# Parent  698fb0e27b111f8d7aa2fa89a4b276b5085e40f6
entity markup for theory Pure, to enable hyperlinks etc.;

diff -r 698fb0e27b11 -r 05d4e5f660ae src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sun Aug 26 22:10:27 2012 +0200
+++ b/src/Pure/Pure.thy	Sun Aug 26 22:23:10 2012 +0200
@@ -1,3 +1,9 @@
+(*  Title:      Pure/Pure.thy
+    Author:     Makarius
+
+Final stage of bootstrapping Pure, based on implicit background theory.
+*)
+
 theory Pure
   keywords
     "!!" "!" "%" "(" ")" "+" "," "--" ":" "::" ";" "<" "<=" "=" "=="
diff -r 698fb0e27b11 -r 05d4e5f660ae src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sun Aug 26 22:10:27 2012 +0200
+++ b/src/Pure/theory.ML	Sun Aug 26 22:23:10 2012 +0200
@@ -135,6 +135,12 @@
     Markup.properties (Position.entity_properties_of def id pos)
       (Isabelle_Markup.entity Isabelle_Markup.theoryN name);
 
+fun init_markup (name, pos) thy =
+  let
+    val id = serial ();
+    val _ = Position.report pos (theory_markup true name id pos);
+  in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end;
+
 fun get_markup thy =
   let val {pos, id, ...} = rep_theory thy
   in theory_markup false (Context.theory_name thy) id pos end;
@@ -161,18 +167,16 @@
 
 fun begin_theory (name, pos) imports =
   if name = Context.PureN then
-    (case imports of [thy] => thy | _ => error "Bad bootstrapping of theory Pure")
+    (case imports of
+      [thy] => init_markup (name, pos) thy
+    | _ => error "Bad bootstrapping of theory Pure")
   else
     let
-      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 thy = Context.begin_thy Context.pretty_global name imports;
       val wrappers = begin_wrappers thy;
     in
       thy
+      |> init_markup (name, pos)
       |> Sign.local_path
       |> Sign.map_naming (Name_Space.set_theory_name name)
       |> apply_wrappers wrappers