# HG changeset patch
# User wenzelm
# Date 1439660555 -7200
# Node ID 51425cbe8ce9f1f616fbf477a7f92346d9f1c5bb
# Parent  2751f7f31be2666180270b78157978b2dc2532cb
clarified context;

diff -r 2751f7f31be2 -r 51425cbe8ce9 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Sat Aug 15 19:11:11 2015 +0200
+++ b/src/Pure/Isar/proof_display.ML	Sat Aug 15 19:42:35 2015 +0200
@@ -7,11 +7,11 @@
 signature PROOF_DISPLAY =
 sig
   val pp_context: Proof.context -> Pretty.T
-  val pp_thm: thm -> Pretty.T
-  val pp_typ: theory -> typ -> Pretty.T
-  val pp_term: theory -> term -> Pretty.T
-  val pp_ctyp: ctyp -> Pretty.T
-  val pp_cterm: cterm -> Pretty.T
+  val pp_thm: (unit -> theory) -> thm -> Pretty.T
+  val pp_typ: (unit -> theory) -> typ -> Pretty.T
+  val pp_term: (unit -> theory) -> term -> Pretty.T
+  val pp_ctyp: (unit -> theory) -> ctyp -> Pretty.T
+  val pp_cterm: (unit -> theory) -> cterm -> Pretty.T
   val pretty_theorems_diff: bool -> theory list -> theory -> Pretty.T list
   val pretty_theorems: bool -> theory -> Pretty.T list
   val pretty_full_theory: bool -> theory -> Pretty.T
@@ -38,24 +38,23 @@
     Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt))
   else Pretty.str "<context>");
 
-fun default_context thy0 =
+fun default_context mk_thy =
   (case Context.thread_data () of
     SOME (Context.Proof ctxt) => ctxt
   | SOME (Context.Theory thy) =>
       (case try Syntax.init_pretty_global thy of
         SOME ctxt => ctxt
-      | NONE => Syntax.init_pretty_global thy0)
-  | NONE => Syntax.init_pretty_global thy0);
+      | NONE => Syntax.init_pretty_global (mk_thy ()))
+  | NONE => Syntax.init_pretty_global (mk_thy ()));
+
+fun pp_thm mk_thy th =
+  Display.pretty_thm_raw (default_context mk_thy) {quote = true, show_hyps = false} th;
 
-fun pp_thm th =
-  let val ctxt = default_context (Thm.theory_of_thm th);
-  in Display.pretty_thm_raw ctxt {quote = true, show_hyps = false} th end;
+fun pp_typ mk_thy T = Pretty.quote (Syntax.pretty_typ (default_context mk_thy) T);
+fun pp_term mk_thy t = Pretty.quote (Syntax.pretty_term (default_context mk_thy) t);
 
-fun pp_typ thy T = Pretty.quote (Syntax.pretty_typ (default_context thy) T);
-fun pp_term thy t = Pretty.quote (Syntax.pretty_term (default_context thy) t);
-
-fun pp_ctyp cT = pp_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
-fun pp_cterm ct = pp_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
+fun pp_ctyp mk_thy cT = pp_typ mk_thy (Thm.typ_of cT);
+fun pp_cterm mk_thy ct = pp_term mk_thy (Thm.term_of ct);
 
 
 (* theorems and theory *)
diff -r 2751f7f31be2 -r 51425cbe8ce9 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sat Aug 15 19:11:11 2015 +0200
+++ b/src/Pure/PIDE/document.ML	Sat Aug 15 19:42:35 2015 +0200
@@ -544,7 +544,7 @@
         |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy))));
 
     val parents =
-      if null parents_reports then [Thy_Info.get_theory "Pure"] else map #1 parents_reports;
+      if null parents_reports then [Thy_Info.pure_theory ()] else map #1 parents_reports;
     val _ = Position.reports (map #2 parents_reports);
   in Resources.begin_theory master_dir header parents end;
 
diff -r 2751f7f31be2 -r 51425cbe8ce9 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Aug 15 19:11:11 2015 +0200
+++ b/src/Pure/ROOT.ML	Sat Aug 15 19:42:35 2015 +0200
@@ -344,9 +344,10 @@
 toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
 toplevel_pp ["Position", "T"] "Pretty.position";
 toplevel_pp ["Binding", "binding"] "Binding.pp";
-toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm";
-toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm";
-toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp";
+toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm Thy_Info.pure_theory";
+toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm Thy_Info.pure_theory";
+toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp Thy_Info.pure_theory";
+toplevel_pp ["typ"] "Proof_Display.pp_typ Thy_Info.pure_theory";
 toplevel_pp ["Context", "theory"] "Context.pretty_thy";
 toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
 toplevel_pp ["Ast", "ast"] "Ast.pretty_ast";
@@ -364,9 +365,7 @@
 use "ML/ml_file.ML";
 Runtime.toplevel_program (fn () => Thy_Info.use_thy ("Pure", Position.none));
 Context.set_thread_data NONE;
-structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
-
-toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy";
+structure Pure = struct val thy = Thy_Info.pure_theory () end;
 
 
 (* ML toplevel commands *)
diff -r 2751f7f31be2 -r 51425cbe8ce9 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Aug 15 19:11:11 2015 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sat Aug 15 19:42:35 2015 +0200
@@ -10,6 +10,7 @@
   val get_names: unit -> string list
   val lookup_theory: string -> theory option
   val get_theory: string -> theory
+  val pure_theory: unit -> theory
   val master_directory: string -> Path.T
   val remove_thy: string -> unit
   val use_theories:
@@ -100,6 +101,8 @@
     SOME theory => theory
   | _ => error ("Theory loader: undefined entry for theory " ^ quote name));
 
+fun pure_theory () = get_theory "Pure";
+
 val get_imports = Resources.imports_of o get_theory;