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.
tuned message;
authorwenzelm
Tue, 09 Jul 2013 16:32:51 +0200
changeset 52565 b04cbc49bdcf
parent 52564 4e855c120f6a
child 52566 52a0eacf04d1
tuned message;
src/Pure/Isar/toplevel.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/toplevel.ML	Tue Jul 09 13:24:17 2013 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jul 09 16:32:51 2013 +0200
@@ -154,7 +154,9 @@
   | level (State (SOME (Proof (prf, _)), _)) = Proof.level (Proof_Node.current prf)
   | level (State (SOME (Skipped_Proof (d, _)), _)) = d + 1;   (*different notion of proof depth!*)
 
-fun str_of_state (State (NONE, _)) = "at top level"
+fun str_of_state (State (NONE, SOME (Theory (Context.Theory thy, _)))) =
+      "at top level, result theory " ^ quote (Context.theory_name thy)
+  | str_of_state (State (NONE, _)) = "at top level"
   | str_of_state (State (SOME (Theory (Context.Theory _, _)), _)) = "in theory mode"
   | str_of_state (State (SOME (Theory (Context.Proof _, _)), _)) = "in local theory mode"
   | str_of_state (State (SOME (Proof _), _)) = "in proof mode"
isabelle