# HG changeset patch
# User haftmann
# Date 1192692060 -7200
# Node ID 21d44e3aea4ccedd5957febf03a12b73593ff9fa
# Parent  db5fdc34f3af16df21a09e4d9a3f9dcd158541fc
evaluation is CRITICAL

diff -r db5fdc34f3af -r 21d44e3aea4c src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Thu Oct 18 09:20:59 2007 +0200
+++ b/src/Tools/nbe.ML	Thu Oct 18 09:21:00 2007 +0200
@@ -103,6 +103,17 @@
 
 val gr_ref = ref NONE : Nbe_Functions.T option ref;
 
+fun compile tab raw_s () =
+  let
+    val _ = univs_ref := (fn () => []);
+    val s = "Nbe.univs_ref := " ^ raw_s;
+    val _ = tracing (fn () => "\n--- generated code:\n" ^ s) ();
+    val _ = gr_ref := SOME tab;
+    val _ = 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 _ = gr_ref := NONE;
+  in !univs_ref end;
 in
 
 fun lookup_fun s = case ! gr_ref
@@ -110,18 +121,9 @@
   | SOME gr => Graph.get_node gr s;
 
 fun compile_univs tab ([], _) = []
-  | compile_univs tab (cs, raw_s) =
-      let
-        val _ = univs_ref := (fn () => []);
-        val s = "Nbe.univs_ref := " ^ raw_s;
-        val _ = tracing (fn () => "\n--- generated code:\n" ^ s) ();
-        val _ = gr_ref := SOME tab;
-        val _ = 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 _ = gr_ref := NONE;
-        val univs = case !univs_ref () of [] => error "compile_univs" | univs => univs;
-      in cs ~~ univs end;
+  | compile_univs tab (cs, raw_s) = case CRITICAL (compile tab raw_s) ()
+     of [] => error "compile_univs"
+      | univs => cs ~~ univs;
 
 end; (*local*)