Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more robust ML pretty printing (cf. b6c527c64789);
authorwenzelm
Wed, 26 Oct 2011 22:51:06 +0200
changeset 45269 6f8949e6c71a
parent 45268 a42624e9de09
child 45271 8f204549c2a5
more robust ML pretty printing (cf. b6c527c64789);
src/Pure/Isar/proof_display.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/proof_display.ML	Wed Oct 26 22:50:40 2011 +0200
+++ b/src/Pure/Isar/proof_display.ML	Wed Oct 26 22:51:06 2011 +0200
@@ -31,9 +31,14 @@
     Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt))
   else Pretty.str "<context>");
 
-fun default_context thy =
-  Context.cases Syntax.init_pretty_global I
-    (the_default (Context.Theory thy) (try ML_Context.the_generic_context ()));
+fun default_context thy0 =
+  (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);
 
 fun pp_thm th =
   let
isabelle