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 messages;
authorwenzelm
Fri, 22 Nov 2013 20:36:57 +0100
changeset 54559 39d91cac6e91
parent 54558 31844ca390ad
child 54560 7f36da77130d
tuned messages;
src/Pure/System/session.scala file | annotate | diff | comparison | revisions
src/Pure/Thy/thy_info.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/System/session.scala	Fri Nov 22 20:28:49 2013 +0100
+++ b/src/Pure/System/session.scala	Fri Nov 22 20:36:57 2013 +0100
@@ -240,7 +240,7 @@
   {
     val header1 =
       if (thy_load.loaded_theories(name.theory))
-        header.error("Attempt to update loaded theory " + quote(name.theory))
+        header.error("Cannot update finished theory " + quote(name.theory))
       else header
     (name, Document.Node.Deps(header1))
   }
--- a/src/Pure/Thy/thy_info.ML	Fri Nov 22 20:28:49 2013 +0100
+++ b/src/Pure/Thy/thy_info.ML	Fri Nov 22 20:36:57 2013 +0100
@@ -140,7 +140,7 @@
 (* main loader actions *)
 
 fun remove_thy name = NAMED_CRITICAL "Thy_Info" (fn () =>
-  if is_finished name then error (loader_msg "attempt to change finished theory" [name])
+  if is_finished name then error (loader_msg "cannot update finished theory" [name])
   else
     let
       val succs = thy_graph String_Graph.all_succs [name];
isabelle