clarified context;
authorwenzelm
Sat Aug 15 19:42:35 2015 +0200 (2015-08-15)
changeset 6093751425cbe8ce9
parent 60936 2751f7f31be2
child 60938 b316f218ef34
clarified context;
src/Pure/Isar/proof_display.ML
src/Pure/PIDE/document.ML
src/Pure/ROOT.ML
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Isar/proof_display.ML	Sat Aug 15 19:11:11 2015 +0200
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Sat Aug 15 19:42:35 2015 +0200
     1.3 @@ -7,11 +7,11 @@
     1.4  signature PROOF_DISPLAY =
     1.5  sig
     1.6    val pp_context: Proof.context -> Pretty.T
     1.7 -  val pp_thm: thm -> Pretty.T
     1.8 -  val pp_typ: theory -> typ -> Pretty.T
     1.9 -  val pp_term: theory -> term -> Pretty.T
    1.10 -  val pp_ctyp: ctyp -> Pretty.T
    1.11 -  val pp_cterm: cterm -> Pretty.T
    1.12 +  val pp_thm: (unit -> theory) -> thm -> Pretty.T
    1.13 +  val pp_typ: (unit -> theory) -> typ -> Pretty.T
    1.14 +  val pp_term: (unit -> theory) -> term -> Pretty.T
    1.15 +  val pp_ctyp: (unit -> theory) -> ctyp -> Pretty.T
    1.16 +  val pp_cterm: (unit -> theory) -> cterm -> Pretty.T
    1.17    val pretty_theorems_diff: bool -> theory list -> theory -> Pretty.T list
    1.18    val pretty_theorems: bool -> theory -> Pretty.T list
    1.19    val pretty_full_theory: bool -> theory -> Pretty.T
    1.20 @@ -38,24 +38,23 @@
    1.21      Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt))
    1.22    else Pretty.str "<context>");
    1.23  
    1.24 -fun default_context thy0 =
    1.25 +fun default_context mk_thy =
    1.26    (case Context.thread_data () of
    1.27      SOME (Context.Proof ctxt) => ctxt
    1.28    | SOME (Context.Theory thy) =>
    1.29        (case try Syntax.init_pretty_global thy of
    1.30          SOME ctxt => ctxt
    1.31 -      | NONE => Syntax.init_pretty_global thy0)
    1.32 -  | NONE => Syntax.init_pretty_global thy0);
    1.33 +      | NONE => Syntax.init_pretty_global (mk_thy ()))
    1.34 +  | NONE => Syntax.init_pretty_global (mk_thy ()));
    1.35 +
    1.36 +fun pp_thm mk_thy th =
    1.37 +  Display.pretty_thm_raw (default_context mk_thy) {quote = true, show_hyps = false} th;
    1.38  
    1.39 -fun pp_thm th =
    1.40 -  let val ctxt = default_context (Thm.theory_of_thm th);
    1.41 -  in Display.pretty_thm_raw ctxt {quote = true, show_hyps = false} th end;
    1.42 +fun pp_typ mk_thy T = Pretty.quote (Syntax.pretty_typ (default_context mk_thy) T);
    1.43 +fun pp_term mk_thy t = Pretty.quote (Syntax.pretty_term (default_context mk_thy) t);
    1.44  
    1.45 -fun pp_typ thy T = Pretty.quote (Syntax.pretty_typ (default_context thy) T);
    1.46 -fun pp_term thy t = Pretty.quote (Syntax.pretty_term (default_context thy) t);
    1.47 -
    1.48 -fun pp_ctyp cT = pp_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
    1.49 -fun pp_cterm ct = pp_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
    1.50 +fun pp_ctyp mk_thy cT = pp_typ mk_thy (Thm.typ_of cT);
    1.51 +fun pp_cterm mk_thy ct = pp_term mk_thy (Thm.term_of ct);
    1.52  
    1.53  
    1.54  (* theorems and theory *)
     2.1 --- a/src/Pure/PIDE/document.ML	Sat Aug 15 19:11:11 2015 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Sat Aug 15 19:42:35 2015 +0200
     2.3 @@ -544,7 +544,7 @@
     2.4          |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy))));
     2.5  
     2.6      val parents =
     2.7 -      if null parents_reports then [Thy_Info.get_theory "Pure"] else map #1 parents_reports;
     2.8 +      if null parents_reports then [Thy_Info.pure_theory ()] else map #1 parents_reports;
     2.9      val _ = Position.reports (map #2 parents_reports);
    2.10    in Resources.begin_theory master_dir header parents end;
    2.11  
     3.1 --- a/src/Pure/ROOT.ML	Sat Aug 15 19:11:11 2015 +0200
     3.2 +++ b/src/Pure/ROOT.ML	Sat Aug 15 19:42:35 2015 +0200
     3.3 @@ -344,9 +344,10 @@
     3.4  toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
     3.5  toplevel_pp ["Position", "T"] "Pretty.position";
     3.6  toplevel_pp ["Binding", "binding"] "Binding.pp";
     3.7 -toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm";
     3.8 -toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm";
     3.9 -toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp";
    3.10 +toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm Thy_Info.pure_theory";
    3.11 +toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm Thy_Info.pure_theory";
    3.12 +toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp Thy_Info.pure_theory";
    3.13 +toplevel_pp ["typ"] "Proof_Display.pp_typ Thy_Info.pure_theory";
    3.14  toplevel_pp ["Context", "theory"] "Context.pretty_thy";
    3.15  toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
    3.16  toplevel_pp ["Ast", "ast"] "Ast.pretty_ast";
    3.17 @@ -364,9 +365,7 @@
    3.18  use "ML/ml_file.ML";
    3.19  Runtime.toplevel_program (fn () => Thy_Info.use_thy ("Pure", Position.none));
    3.20  Context.set_thread_data NONE;
    3.21 -structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
    3.22 -
    3.23 -toplevel_pp ["typ"] "Proof_Display.pp_typ Pure.thy";
    3.24 +structure Pure = struct val thy = Thy_Info.pure_theory () end;
    3.25  
    3.26  
    3.27  (* ML toplevel commands *)
     4.1 --- a/src/Pure/Thy/thy_info.ML	Sat Aug 15 19:11:11 2015 +0200
     4.2 +++ b/src/Pure/Thy/thy_info.ML	Sat Aug 15 19:42:35 2015 +0200
     4.3 @@ -10,6 +10,7 @@
     4.4    val get_names: unit -> string list
     4.5    val lookup_theory: string -> theory option
     4.6    val get_theory: string -> theory
     4.7 +  val pure_theory: unit -> theory
     4.8    val master_directory: string -> Path.T
     4.9    val remove_thy: string -> unit
    4.10    val use_theories:
    4.11 @@ -100,6 +101,8 @@
    4.12      SOME theory => theory
    4.13    | _ => error ("Theory loader: undefined entry for theory " ^ quote name));
    4.14  
    4.15 +fun pure_theory () = get_theory "Pure";
    4.16 +
    4.17  val get_imports = Resources.imports_of o get_theory;
    4.18  
    4.19