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.
fixed output
authorhaftmann
Thu, 04 Jan 2007 14:01:41 +0100
changeset 21991 04528ce9ded5
parent 21990 d382f901304c
child 21992 337990f42ce0
fixed output
src/Pure/Tools/nbe.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Tools/nbe.ML	Thu Jan 04 14:01:40 2007 +0100
+++ b/src/Pure/Tools/nbe.ML	Thu Jan 04 14:01:41 2007 +0100
@@ -114,12 +114,12 @@
         with implicit side effect *)
     fun use_code NONE = ()
       | use_code (SOME s) =
-          (tracing (fn () => "\n---generated code:\n" ^ s);
+          (tracing (fn () => "\n---generated code:\n" ^ s) ();
            use_text (Output.tracing o enclose "\n---compiler echo:\n" "\n---\n",
                 Output.tracing o enclose "\n--- compiler echo (with error!):\n" "\n---\n")
             (!trace) s);
 
-    val _ = tracing (fn () => "new definitions: " ^ (commas o maps (map fst)) funs);
+    val _ = tracing (fn () => "new definitions: " ^ (commas o maps (map fst)) funs) ();
     val _ = tab := NBE_Data.get thy;;
     val _ = Library.seq (use_code o NBE_Codegen.generate thy
       (fn s => Symtab.defined (!tab) s)) funs;
isabelle