# HG changeset patch
# User huffman
# Date 1244433472 25200
# Node ID ff0ab207849a367a22c61bdda833d806695b7ee2
# Parent  1ba61c7b129f3175c9aa9071e7a28890ab3bd14c# Parent  eced346b2231081e544236f15ed8a4f00f003cde
merged

diff -r 1ba61c7b129f -r ff0ab207849a Admin/isatest/isatest-makeall
--- a/Admin/isatest/isatest-makeall	Sun Jun 07 20:57:24 2009 -0700
+++ b/Admin/isatest/isatest-makeall	Sun Jun 07 20:57:52 2009 -0700
@@ -76,6 +76,11 @@
         NICE=""
         ;;
 
+    macbroy23)
+        MFLAGS=""
+        NICE=""
+        ;;
+
     macbroy2[0-9])
         MFLAGS="-j 2"
         NICE=""
diff -r 1ba61c7b129f -r ff0ab207849a doc-src/System/Thy/Misc.thy
--- a/doc-src/System/Thy/Misc.thy	Sun Jun 07 20:57:24 2009 -0700
+++ b/doc-src/System/Thy/Misc.thy	Sun Jun 07 20:57:52 2009 -0700
@@ -85,6 +85,8 @@
   Options are:
     -a           display complete environment
     -b           print values only (doesn't work for -a)
+    -d FILE      dump complete environment to FILE
+                 (null terminated entries)
 
   Get value of VARNAMES from the Isabelle settings.
 \end{ttbox}
@@ -95,6 +97,10 @@
   Normally, output is a list of lines of the form @{text
   name}@{verbatim "="}@{text value}. The @{verbatim "-b"} option
   causes only the values to be printed.
+
+  Option @{verbatim "-d"} produces a dump of the complete environment
+  to the specified file.  Entries are terminated by the ASCII null
+  character, i.e.\ the C string terminator.
 *}
 
 
diff -r 1ba61c7b129f -r ff0ab207849a doc-src/System/Thy/document/Misc.tex
--- a/doc-src/System/Thy/document/Misc.tex	Sun Jun 07 20:57:24 2009 -0700
+++ b/doc-src/System/Thy/document/Misc.tex	Sun Jun 07 20:57:52 2009 -0700
@@ -110,6 +110,8 @@
   Options are:
     -a           display complete environment
     -b           print values only (doesn't work for -a)
+    -d FILE      dump complete environment to FILE
+                 (null terminated entries)
 
   Get value of VARNAMES from the Isabelle settings.
 \end{ttbox}
@@ -118,7 +120,11 @@
   environment that Isabelle related programs are run in. This usually
   contains much more variables than are actually Isabelle settings.
   Normally, output is a list of lines of the form \isa{name}\verb|=|\isa{value}. The \verb|-b| option
-  causes only the values to be printed.%
+  causes only the values to be printed.
+
+  Option \verb|-d| produces a dump of the complete environment
+  to the specified file.  Entries are terminated by the ASCII null
+  character, i.e.\ the C string terminator.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 1ba61c7b129f -r ff0ab207849a lib/Tools/getenv
--- a/lib/Tools/getenv	Sun Jun 07 20:57:24 2009 -0700
+++ b/lib/Tools/getenv	Sun Jun 07 20:57:52 2009 -0700
@@ -17,6 +17,8 @@
   echo "  Options are:"
   echo "    -a           display complete environment"
   echo "    -b           print values only (doesn't work for -a)"
+  echo "    -d FILE      dump complete environment to FILE"
+  echo "                 (null terminated entries)"
   echo
   echo "  Get value of VARNAMES from the Isabelle settings."
   echo
@@ -30,8 +32,9 @@
 
 ALL=""
 BASE=""
+DUMP=""
 
-while getopts "ab" OPT
+while getopts "abd:" OPT
 do
   case "$OPT" in
     a)
@@ -40,6 +43,9 @@
     b)
       BASE=true
       ;;
+    d)
+      DUMP="$OPTARG"
+      ;;
     \?)
       usage
       ;;
@@ -68,3 +74,8 @@
     fi
   done
 fi
+
+if [ -n "$DUMP" ]; then
+  exec perl -w -e 'for $key (keys %ENV) { print $key, "=", $ENV{$key}, "\x00"; }' > "$DUMP"
+fi
+
diff -r 1ba61c7b129f -r ff0ab207849a src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Sun Jun 07 20:57:24 2009 -0700
+++ b/src/HOL/Tools/res_reconstruct.ML	Sun Jun 07 20:57:52 2009 -0700
@@ -452,7 +452,7 @@
     isar_header (map #1 fixes) ^ String.concat ilines ^ "qed\n"
   end
   handle e => (*FIXME: exn handler is too general!*)
-    let val msg = "Translation of TSTP raised an exception: " ^ Toplevel.exn_message e
+    let val msg = "Translation of TSTP raised an exception: " ^ ML_Compiler.exn_message e
     in  trace msg; msg  end;
 
 
diff -r 1ba61c7b129f -r ff0ab207849a src/Pure/General/basics.ML
--- a/src/Pure/General/basics.ML	Sun Jun 07 20:57:24 2009 -0700
+++ b/src/Pure/General/basics.ML	Sun Jun 07 20:57:52 2009 -0700
@@ -94,7 +94,7 @@
 (* partiality *)
 
 fun try f x = SOME (f x)
-  handle Exn.Interrupt => raise Exn.Interrupt | _ => NONE;
+  handle (exn as Exn.Interrupt) => reraise exn | _ => NONE;
 
 fun can f x = is_some (try f x);
 
diff -r 1ba61c7b129f -r ff0ab207849a src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sun Jun 07 20:57:24 2009 -0700
+++ b/src/Pure/General/markup.ML	Sun Jun 07 20:57:52 2009 -0700
@@ -71,6 +71,8 @@
   val ML_commentN: string val ML_comment: T
   val ML_malformedN: string val ML_malformed: T
   val ML_defN: string val ML_def: T
+  val ML_openN: string val ML_open: T
+  val ML_structN: string val ML_struct: T
   val ML_refN: string val ML_ref: T
   val ML_typingN: string val ML_typing: T
   val ML_sourceN: string val ML_source: T
@@ -237,6 +239,8 @@
 val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed";
 
 val (ML_defN, ML_def) = markup_elem "ML_def";
+val (ML_openN, ML_open) = markup_elem "ML_open";
+val (ML_structN, ML_struct) = markup_elem "ML_struct";
 val (ML_refN, ML_ref) = markup_elem "ML_ref";
 val (ML_typingN, ML_typing) = markup_elem "ML_typing";
 
diff -r 1ba61c7b129f -r ff0ab207849a src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sun Jun 07 20:57:24 2009 -0700
+++ b/src/Pure/General/markup.scala	Sun Jun 07 20:57:52 2009 -0700
@@ -92,6 +92,8 @@
   val ML_MALFORMED = "ML_malformed"
 
   val ML_DEF = "ML_def"
+  val ML_OPEN = "ML_open"
+  val ML_STRUCT = "ML_struct"
   val ML_REF = "ML_ref"
   val ML_TYPING = "ML_typing"
 
diff -r 1ba61c7b129f -r ff0ab207849a src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Sun Jun 07 20:57:24 2009 -0700
+++ b/src/Pure/General/secure.ML	Sun Jun 07 20:57:52 2009 -0700
@@ -70,7 +70,7 @@
 val use_text = Secure.use_text;
 val use_file = Secure.use_file;
 fun use s = Secure.use_file ML_Parse.global_context true s
-  handle ERROR msg => (writeln msg; raise Fail "ML error");
+  handle ERROR msg => (writeln msg; error "ML error");
 val toplevel_pp = Secure.toplevel_pp;
 val system_out = Secure.system_out;
 val system = Secure.system;
diff -r 1ba61c7b129f -r ff0ab207849a src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Sun Jun 07 20:57:24 2009 -0700
+++ b/src/Pure/IsaMakefile	Sun Jun 07 20:57:52 2009 -0700
@@ -62,12 +62,12 @@
   Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML		\
   Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML		\
   Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML	\
-  Isar/rule_cases.ML Isar/rule_insts.ML Isar/skip_proof.ML		\
-  Isar/spec_parse.ML Isar/specification.ML Isar/theory_target.ML	\
-  Isar/toplevel.ML Isar/value_parse.ML ML/ml_antiquote.ML		\
-  ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML	\
-  ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML		\
-  ML/ml_thms.ML ML-Systems/install_pp_polyml.ML				\
+  Isar/rule_cases.ML Isar/rule_insts.ML Isar/runtime.ML			\
+  Isar/skip_proof.ML Isar/spec_parse.ML Isar/specification.ML		\
+  Isar/theory_target.ML Isar/toplevel.ML Isar/value_parse.ML		\
+  ML/ml_antiquote.ML ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML	\
+  ML/ml_context.ML ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML		\
+  ML/ml_syntax.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML		\
   ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML		\
   Proof/extraction.ML Proof/proof_rewrite_rules.ML			\
   Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML	\
@@ -118,8 +118,9 @@
   General/position.scala General/swing.scala General/symbol.scala	\
   General/xml.scala General/yxml.scala Isar/isar.scala			\
   Isar/isar_document.scala Isar/outer_keyword.scala			\
-  System/isabelle_process.scala System/isabelle_system.scala		\
-  Thy/thy_header.scala Tools/isabelle_syntax.scala
+  System/cygwin.scala System/isabelle_process.scala			\
+  System/isabelle_system.scala Thy/thy_header.scala			\
+  Tools/isabelle_syntax.scala
 
 
 SCALA_TARGET = $(ISABELLE_HOME)/lib/classes/Pure.jar
diff -r 1ba61c7b129f -r ff0ab207849a src/Pure/Isar/runtime.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/runtime.ML	Sun Jun 07 20:57:52 2009 -0700
@@ -0,0 +1,107 @@
+(*  Title:      Pure/Isar/runtime.ML
+    Author:     Makarius
+
+Isar toplevel runtime support.
+*)
+
+signature RUNTIME =
+sig
+  exception UNDEF
+  exception TERMINATE
+  exception EXCURSION_FAIL of exn * string
+  exception TOPLEVEL_ERROR
+  val exn_context: Proof.context option -> exn -> exn
+  val exn_message: (exn -> Position.T) -> exn -> string
+  val debugging: ('a -> 'b) -> 'a -> 'b
+  val controlled_execution: ('a -> 'b) -> 'a -> 'b
+  val toplevel_error: (exn -> string) -> ('a -> 'b) -> 'a -> 'b
+end;
+
+structure Runtime: RUNTIME =
+struct
+
+(** exceptions **)
+
+exception UNDEF;
+exception TERMINATE;
+exception EXCURSION_FAIL of exn * string;
+exception TOPLEVEL_ERROR;
+
+
+(* exn_context *)
+
+exception CONTEXT of Proof.context * exn;
+
+fun exn_context NONE exn = exn
+  | exn_context (SOME ctxt) exn = CONTEXT (ctxt, exn);
+
+
+(* exn_message *)
+
+fun if_context NONE _ _ = []
+  | if_context (SOME ctxt) f xs = map (f ctxt) xs;
+
+fun exn_message exn_position e =
+  let
+    fun raised exn name msgs =
+      let val pos = Position.str_of (exn_position exn) in
+        (case msgs of
+          [] => "exception " ^ name ^ " raised" ^ pos
+        | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
+        | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
+      end;
+
+    val detailed = ! Output.debugging;
+
+    fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn
+      | exn_msg ctxt (Exn.EXCEPTIONS exns) = cat_lines (map (exn_msg ctxt) exns)
+      | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) =
+          exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc)
+      | exn_msg _ TERMINATE = "Exit."
+      | exn_msg _ Exn.Interrupt = "Interrupt."
+      | exn_msg _ TimeLimit.TimeOut = "Timeout."
+      | exn_msg _ TOPLEVEL_ERROR = "Error."
+      | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
+      | exn_msg _ (ERROR msg) = msg
+      | exn_msg _ (exn as Fail msg) = raised exn "Fail" [msg]
+      | exn_msg _ (exn as THEORY (msg, thys)) =
+          raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))
+      | exn_msg _ (exn as Syntax.AST (msg, asts)) = raised exn "AST" (msg ::
+            (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))
+      | exn_msg ctxt (exn as TYPE (msg, Ts, ts)) = raised exn "TYPE" (msg ::
+            (if detailed then
+              if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts
+             else []))
+      | exn_msg ctxt (exn as TERM (msg, ts)) = raised exn "TERM" (msg ::
+            (if detailed then if_context ctxt Syntax.string_of_term ts else []))
+      | exn_msg ctxt (exn as THM (msg, i, thms)) = raised exn ("THM " ^ string_of_int i) (msg ::
+            (if detailed then if_context ctxt ProofContext.string_of_thm thms else []))
+      | exn_msg _ exn = raised exn (General.exnMessage exn) [];
+  in exn_msg NONE e end;
+
+
+
+(** controlled execution **)
+
+fun debugging f x =
+  if ! Output.debugging then
+    Exn.release (exception_trace (fn () =>
+      Exn.Result (f x) handle
+        exn as UNDEF => Exn.Exn exn
+      | exn as EXCURSION_FAIL _ => Exn.Exn exn))
+  else f x;
+
+fun controlled_execution f =
+  f
+  |> debugging
+  |> Future.interruptible_task;
+
+fun toplevel_error exn_message f x =
+  let val ctxt = Option.map Context.proof_of (Context.thread_data ()) in
+    f x handle exn =>
+      (Output.error_msg (exn_message (exn_context ctxt exn));
+        raise TOPLEVEL_ERROR)
+  end;
+
+end;
+
diff -r 1ba61c7b129f -r ff0ab207849a src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun Jun 07 20:57:24 2009 -0700
+++ b/src/Pure/Isar/toplevel.ML	Sun Jun 07 20:57:52 2009 -0700
@@ -32,8 +32,6 @@
   val skip_proofs: bool ref
   exception TERMINATE
   exception TOPLEVEL_ERROR
-  exception CONTEXT of Proof.context * exn
-  val exn_message: exn -> string
   val program: (unit -> 'a) -> 'a
   type transition
   val empty: transition
@@ -98,7 +96,7 @@
 
 (** toplevel state **)
 
-exception UNDEF;
+exception UNDEF = Runtime.UNDEF;
 
 
 (* local theory wrappers *)
@@ -225,102 +223,20 @@
 val profiling = ref 0;
 val skip_proofs = ref false;
 
-exception TERMINATE;
-exception EXCURSION_FAIL of exn * string;
-exception FAILURE of state * exn;
-exception TOPLEVEL_ERROR;
-
-
-(* print exceptions *)
-
-exception CONTEXT of Proof.context * exn;
-
-fun exn_context NONE exn = exn
-  | exn_context (SOME ctxt) exn = CONTEXT (ctxt, exn);
-
-local
-
-fun if_context NONE _ _ = []
-  | if_context (SOME ctxt) f xs = map (f ctxt) xs;
-
-fun raised exn name msgs =
-  let val pos = Position.str_of (ML_Compiler.exception_position exn) in
-    (case msgs of
-      [] => "exception " ^ name ^ " raised" ^ pos
-    | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
-    | _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
-  end;
-
-in
-
-fun exn_message e =
-  let
-    val detailed = ! debug;
-
-    fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn
-      | exn_msg ctxt (Exn.EXCEPTIONS exns) = cat_lines (map (exn_msg ctxt) exns)
-      | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) =
-          exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc)
-      | exn_msg _ TERMINATE = "Exit."
-      | exn_msg _ Exn.Interrupt = "Interrupt."
-      | exn_msg _ TimeLimit.TimeOut = "Timeout."
-      | exn_msg _ TOPLEVEL_ERROR = "Error."
-      | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
-      | exn_msg _ (ERROR msg) = msg
-      | exn_msg _ (exn as Fail msg) = raised exn "Fail" [msg]
-      | exn_msg _ (exn as THEORY (msg, thys)) =
-          raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))
-      | exn_msg _ (exn as Syntax.AST (msg, asts)) = raised exn "AST" (msg ::
-            (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))
-      | exn_msg ctxt (exn as TYPE (msg, Ts, ts)) = raised exn "TYPE" (msg ::
-            (if detailed then
-              if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts
-             else []))
-      | exn_msg ctxt (exn as TERM (msg, ts)) = raised exn "TERM" (msg ::
-            (if detailed then if_context ctxt Syntax.string_of_term ts else []))
-      | exn_msg ctxt (exn as THM (msg, i, thms)) = raised exn ("THM " ^ string_of_int i) (msg ::
-            (if detailed then if_context ctxt ProofContext.string_of_thm thms else []))
-      | exn_msg _ exn = raised exn (General.exnMessage exn) []
-  in exn_msg NONE e end;
-
-end;
-
-
-(* controlled execution *)
-
-local
-
-fun debugging f x =
-  if ! debug then
-    Exn.release (exception_trace (fn () =>
-      Exn.Result (f x) handle
-        exn as UNDEF => Exn.Exn exn
-      | exn as EXCURSION_FAIL _ => Exn.Exn exn))
-  else f x;
-
-fun toplevel_error f x =
-  let val ctxt = try ML_Context.the_local_context () in
-    f x handle exn =>
-      (Output.error_msg (exn_message (exn_context ctxt exn)); raise TOPLEVEL_ERROR)
-  end;
-
-in
-
-fun controlled_execution f =
-  f
-  |> debugging
-  |> Future.interruptible_task;
+exception TERMINATE = Runtime.TERMINATE;
+exception EXCURSION_FAIL = Runtime.EXCURSION_FAIL;
+exception TOPLEVEL_ERROR = Runtime.TOPLEVEL_ERROR;
 
 fun program f =
  (f
-  |> controlled_execution
-  |> toplevel_error) ();
-
-end;
+  |> Runtime.controlled_execution
+  |> Runtime.toplevel_error ML_Compiler.exn_message) ();
 
 
 (* node transactions -- maintaining stable checkpoints *)
 
+exception FAILURE of state * exn;
+
 local
 
 fun reset_presentation (Theory (gthy, _)) = Theory (gthy, NONE)
@@ -329,7 +245,7 @@
 fun is_draft_theory (Theory (gthy, _)) = Context.is_draft (Context.theory_of gthy)
   | is_draft_theory _ = false;
 
-fun is_stale state = Context.is_stale (theory_of state) handle UNDEF => false;
+fun is_stale state = Context.is_stale (theory_of state) handle Runtime.UNDEF => false;
 
 fun stale_error NONE = SOME (ERROR "Stale theory encountered after successful execution!")
   | stale_error some = some;
@@ -349,7 +265,7 @@
 
     val (result, err) =
       cont_node
-      |> controlled_execution f
+      |> Runtime.controlled_execution f
       |> map_theory Theory.checkpoint
       |> state_error NONE
       handle exn => state_error (SOME exn) cont_node;
@@ -382,9 +298,9 @@
   | apply_tr _ _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) =
       State (NONE, prev)
   | apply_tr _ _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =
-      (controlled_execution exit thy; toplevel)
+      (Runtime.controlled_execution exit thy; toplevel)
   | apply_tr int _ (Keep f) state =
-      controlled_execution (fn x => tap (f int) x) state
+      Runtime.controlled_execution (fn x => tap (f int) x) state
   | apply_tr int pos (Transaction (f, g)) (State (SOME state, _)) =
       apply_transaction pos (fn x => f int x) g state
   | apply_tr _ _ _ _ = raise UNDEF;
@@ -392,7 +308,7 @@
 fun apply_union _ _ [] state = raise FAILURE (state, UNDEF)
   | apply_union int pos (tr :: trs) state =
       apply_union int pos trs state
-        handle UNDEF => apply_tr int pos tr state
+        handle Runtime.UNDEF => apply_tr int pos tr state
           | FAILURE (alt_state, UNDEF) => apply_tr int pos tr alt_state
           | exn as FAILURE _ => raise exn
           | exn => raise FAILURE (state, exn);
@@ -628,7 +544,8 @@
   setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
 
 fun error_msg tr exn_info =
-  setmp_thread_position tr (fn () => Output.error_msg (exn_message (EXCURSION_FAIL exn_info))) ();
+  setmp_thread_position tr (fn () =>
+    Output.error_msg (ML_Compiler.exn_message (EXCURSION_FAIL exn_info))) ();
 
 
 (* post-transition hooks *)
@@ -671,7 +588,7 @@
       (case app int tr st of
         (_, SOME TERMINATE) => NONE
       | (st', SOME (EXCURSION_FAIL exn_info)) => SOME (st', SOME exn_info)
-      | (st', SOME exn) => SOME (st', SOME (exn_context ctxt exn, at_command tr))
+      | (st', SOME exn) => SOME (st', SOME (Runtime.exn_context ctxt exn, at_command tr))
       | (st', NONE) => SOME (st', NONE));
     val _ = (case res of SOME (st', NONE) => apply_hooks st' | _ => ());
   in res end;
diff -r 1ba61c7b129f -r ff0ab207849a src/Pure/ML-Systems/compiler_polyml-5.0.ML
--- a/src/Pure/ML-Systems/compiler_polyml-5.0.ML	Sun Jun 07 20:57:24 2009 -0700
+++ b/src/Pure/ML-Systems/compiler_polyml-5.0.ML	Sun Jun 07 20:57:52 2009 -0700
@@ -21,7 +21,7 @@
         [] => ()
       | _ => (PolyML.compilerEx (get, put, fn () => ! current_line, name) (); exec ()));
   in
-    exec () handle exn => (error (output ()); raise exn);
+    exec () handle exn => (error (output ()); reraise exn);
     if verbose then print (output ()) else ()
   end;
 
diff -r 1ba61c7b129f -r ff0ab207849a src/Pure/ML-Systems/compiler_polyml-5.2.ML
--- a/src/Pure/ML-Systems/compiler_polyml-5.2.ML	Sun Jun 07 20:57:24 2009 -0700
+++ b/src/Pure/ML-Systems/compiler_polyml-5.2.ML	Sun Jun 07 20:57:52 2009 -0700
@@ -38,7 +38,7 @@
         PolyML.compiler (get, parameters) ())
       handle exn =>
        (put ("Exception- " ^ General.exnMessage exn ^ " raised");
-        error (output ()); raise exn);
+        error (output ()); reraise exn);
   in if verbose then print (output ()) else () end;
 
 fun use_file context verbose name =
diff -r 1ba61c7b129f -r ff0ab207849a src/Pure/ML-Systems/compiler_polyml-5.3.ML
--- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Sun Jun 07 20:57:24 2009 -0700
+++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Sun Jun 07 20:57:52 2009 -0700
@@ -14,7 +14,7 @@
 fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
     (start_line, name) verbose txt =
   let
-    val current_line = ref start_line;
+    val line = ref start_line;
     val in_buffer = ref (String.explode (tune_source txt));
     val out_buffer = ref ([]: string list);
     fun output () = drop_newline (implode (rev (! out_buffer)));
@@ -22,8 +22,7 @@
     fun get () =
       (case ! in_buffer of
         [] => NONE
-      | c :: cs =>
-          (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
+      | c :: cs => (in_buffer := cs; if c = #"\n" then line := ! line + 1 else (); SOME c));
     fun put s = out_buffer := s :: ! out_buffer;
     fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} =
      (put (if hard then "Error: " else "Warning: ");
@@ -33,16 +32,17 @@
 
     val parameters =
      [PolyML.Compiler.CPOutStream put,
-      PolyML.Compiler.CPLineNo (fn () => ! current_line),
+      PolyML.Compiler.CPNameSpace name_space,
       PolyML.Compiler.CPErrorMessageProc put_message,
-      PolyML.Compiler.CPNameSpace name_space,
+      PolyML.Compiler.CPLineNo (fn () => ! line),
+      PolyML.Compiler.CPFileName name,
       PolyML.Compiler.CPPrintInAlphabeticalOrder false];
     val _ =
       (while not (List.null (! in_buffer)) do
         PolyML.compiler (get, parameters) ())
       handle exn =>
        (put ("Exception- " ^ General.exnMessage exn ^ " raised");
-        error (output ()); raise exn);
+        error (output ()); reraise exn);
   in if verbose then print (output ()) else () end;
 
 fun use_file context verbose name =
diff -r 1ba61c7b129f -r ff0ab207849a src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Sun Jun 07 20:57:24 2009 -0700
+++ b/src/Pure/ML/ml_compiler.ML	Sun Jun 07 20:57:52 2009 -0700
@@ -6,14 +6,16 @@
 
 signature ML_COMPILER =
 sig
-  val exception_position: exn -> Position.T
+  val exn_position: exn -> Position.T
+  val exn_message: exn -> string
   val eval: bool -> Position.T -> ML_Lex.token list -> unit
 end
 
 structure ML_Compiler: ML_COMPILER =
 struct
 
-fun exception_position _ = Position.none;
+fun exn_position _ = Position.none;
+val exn_message = Runtime.exn_message exn_position;
 
 fun eval verbose pos toks =
   let
diff -r 1ba61c7b129f -r ff0ab207849a src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Sun Jun 07 20:57:24 2009 -0700
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Sun Jun 07 20:57:52 2009 -0700
@@ -1,12 +1,13 @@
 (*  Title:      Pure/ML/ml_compiler_polyml-5.3.ML
     Author:     Makarius
 
-Advanced runtime compilation for Poly/ML 5.3 (SVN 762).
+Advanced runtime compilation for Poly/ML 5.3 (SVN 773).
 *)
 
 signature ML_COMPILER =
 sig
-  val exception_position: exn -> Position.T
+  val exn_position: exn -> Position.T
+  val exn_message: exn -> string
   val eval: bool -> Position.T -> ML_Lex.token list -> unit
 end
 
@@ -31,24 +32,28 @@
     loc_props
   end |> Position.of_properties;
 
-fun exception_position exn =
+fun exn_position exn =
   (case PolyML.exceptionLocation exn of
     NONE => Position.none
   | SOME loc => position_of loc);
 
+val exn_message = Runtime.exn_message exn_position;
+
 
 (* parse trees *)
 
 fun report_parse_tree depth space =
   let
+    fun report_decl markup loc decl =
+      Position.report_text Markup.ML_ref (position_of loc)
+        (Markup.markup (Markup.properties (Position.properties_of (position_of decl)) markup) "");
     fun report loc (PolyML.PTtype types) =
           PolyML.NameSpace.displayTypeExpression (types, depth, space)
           |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
           |> Position.report_text Markup.ML_typing (position_of loc)
-      | report loc (PolyML.PTdeclaredAt decl) =
-          Markup.markup
-            (Markup.properties (Position.properties_of (position_of decl)) Markup.ML_def) ""
-          |> Position.report_text Markup.ML_ref (position_of loc)
+      | report loc (PolyML.PTdeclaredAt decl) = report_decl Markup.ML_def loc decl
+      | report loc (PolyML.PTopenedAt decl) = report_decl Markup.ML_open loc decl
+      | report loc (PolyML.PTstructureAt decl) = report_decl Markup.ML_struct loc decl
       | report _ (PolyML.PTnextSibling tree) = report_tree (tree ())
       | report _ (PolyML.PTfirstChild tree) = report_tree (tree ())
       | report _ _ = ()
@@ -77,7 +82,11 @@
           (Position.reset_range (ML_Lex.pos_of tok));
       in ps ~~ map (String.explode o Symbol.esc) syms end);
 
-    val input_buffer = ref input;
+    val end_pos =
+      if null toks then Position.none
+      else ML_Lex.end_pos_of (List.last toks);
+
+    val input_buffer = ref (input @ [(end_pos, [#"\n"])]);
     val line = ref (the_default 1 (Position.line_of pos));
 
     fun get_offset () =
@@ -139,10 +148,13 @@
       end;
 
     fun result_fun (phase1, phase2) () =
-     (case phase1 of NONE => ()
-      | SOME parse_tree => report_parse_tree depth space parse_tree;
-      case phase2 of NONE => err "Static Errors"
-      | SOME code => apply_result (code ()));  (* FIXME cf. Toplevel.program *)
+     ((case phase1 of
+        NONE => ()
+      | SOME parse_tree => report_parse_tree depth space parse_tree);
+      (case phase2 of
+        NONE => err "Static Errors"
+      | SOME code =>
+          apply_result ((code |> Runtime.debugging |> Runtime.toplevel_error exn_message) ())));
 
 
     (* compiler invocation *)
@@ -152,15 +164,16 @@
       PolyML.Compiler.CPNameSpace space,
       PolyML.Compiler.CPErrorMessageProc put_message,
       PolyML.Compiler.CPLineNo (fn () => ! line),
+      PolyML.Compiler.CPLineOffset get_offset,
       PolyML.Compiler.CPFileName location_props,
-      PolyML.Compiler.CPLineOffset get_offset,
-      PolyML.Compiler.CPCompilerResultFun result_fun];
+      PolyML.Compiler.CPCompilerResultFun result_fun,
+      PolyML.Compiler.CPPrintInAlphabeticalOrder false];
     val _ =
       (while not (List.null (! input_buffer)) do
         PolyML.compiler (get, parameters) ())
       handle exn =>
        (put ("Exception- " ^ General.exnMessage exn ^ " raised");
-        err (output ()); raise exn);
+        err (output ()); reraise exn);
   in if verbose then print (output ()) else () end;
 
 end;
diff -r 1ba61c7b129f -r ff0ab207849a src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Sun Jun 07 20:57:24 2009 -0700
+++ b/src/Pure/ML/ml_env.ML	Sun Jun 07 20:57:52 2009 -0700
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML/ml_env.ML
     Author:     Makarius
 
-Local environment of ML sources and results.
+Local environment of ML results.
 *)
 
 signature ML_ENV =
diff -r 1ba61c7b129f -r ff0ab207849a src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Sun Jun 07 20:57:24 2009 -0700
+++ b/src/Pure/ML/ml_lex.ML	Sun Jun 07 20:57:52 2009 -0700
@@ -15,6 +15,7 @@
   val is_improper: token -> bool
   val set_range: Position.range -> token -> token
   val pos_of: token -> Position.T
+  val end_pos_of: token -> Position.T
   val kind_of: token -> token_kind
   val content_of: token -> string
   val check_content_of: token -> string
diff -r 1ba61c7b129f -r ff0ab207849a src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Jun 07 20:57:24 2009 -0700
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Jun 07 20:57:52 2009 -0700
@@ -1000,7 +1000,7 @@
       | (Toplevel.UNDEF,SOME src) =>
         (Output.error_msg "No working context defined"; loop true src)
       | (e,SOME src) =>
-        (Output.error_msg (Toplevel.exn_message e); loop true src)
+        (Output.error_msg (ML_Compiler.exn_message e); loop true src)
       | (PGIP_QUIT,_) => ()
       | (_,NONE) => ()
 in
diff -r 1ba61c7b129f -r ff0ab207849a src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sun Jun 07 20:57:24 2009 -0700
+++ b/src/Pure/ROOT.ML	Sun Jun 07 20:57:52 2009 -0700
@@ -155,6 +155,7 @@
 (*ML support*)
 use "ML/ml_syntax.ML";
 use "ML/ml_env.ML";
+use "Isar/runtime.ML";
 if ml_system = "polyml-experimental"
 then use "ML/ml_compiler_polyml-5.3.ML"
 else use "ML/ml_compiler.ML";
diff -r 1ba61c7b129f -r ff0ab207849a src/Pure/System/cygwin.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/cygwin.scala	Sun Jun 07 20:57:52 2009 -0700
@@ -0,0 +1,84 @@
+/*  Title:      Pure/System/cygwin.scala
+    Author:     Makarius
+
+Accessing the Cygwin installation.
+*/
+
+package isabelle
+
+import java.lang.reflect.Method
+
+
+object Cygwin
+{
+  /* registry access */
+
+  // Some black magic involving private WindowsPreferences from Sun, cf.
+  // http://www.docjar.com/html/api/java/util/prefs/WindowsPreferences.java.html
+
+  private val WindowsPreferences = Class.forName("java.util.prefs.WindowsPreferences")
+
+  private val HKEY_CURRENT_USER = 0x80000001
+  private val HKEY_LOCAL_MACHINE = 0x80000002
+  private val KEY_READ = 0x20019
+  private val NATIVE_HANDLE = 0
+  private val ERROR_CODE = 1
+
+  private def C_string(s: String): Array[Byte] =
+    (s + "\0").getBytes("US-ASCII")
+
+  private def J_string(bs: Array[Byte]): String =
+    new String(bs, 0, bs.length - 1, "US-ASCII")
+
+  private val INT = Integer.TYPE
+  private val BYTES = (new Array[Byte](0)).getClass
+
+  private def open_key(handle: Int, subkey: Array[Byte], mask: Int): Array[Int] =
+  {
+    val m = WindowsPreferences.getDeclaredMethod("WindowsRegOpenKey", INT, BYTES, INT)
+    m.setAccessible(true)
+    m.invoke(null, handle.asInstanceOf[Object], subkey.asInstanceOf[Object],
+      mask.asInstanceOf[Object]).asInstanceOf[Array[Int]]
+  }
+
+  private def close_key(handle: Int): Int =
+  {
+    val m = WindowsPreferences.getDeclaredMethod("WindowsRegCloseKey", INT)
+    m.setAccessible(true)
+    m.invoke(null, handle.asInstanceOf[Object]).asInstanceOf[Int]
+  }
+
+  private def query(handle: Int, name: Array[Byte]) =
+  {
+    val m = WindowsPreferences.getDeclaredMethod("WindowsRegQueryValueEx", INT, BYTES)
+    m.setAccessible(true)
+    m.invoke(null, handle.asInstanceOf[Object], name.asInstanceOf[Object]).
+      asInstanceOf[Array[Byte]]
+  }
+
+  def query_registry(sys: Boolean, path: String, name: String): Option[String] =
+  {
+    val handle = if (sys) HKEY_LOCAL_MACHINE else HKEY_CURRENT_USER
+    val result = open_key(handle, C_string(path), KEY_READ)
+    if (result(ERROR_CODE) != 0) None
+    else {
+      val res = query(result(NATIVE_HANDLE), C_string(name))
+      if (res == null) None
+      else Some(J_string(res))
+    }
+  }
+
+  def query_registry(path: String, name: String): Option[String] =
+    query_registry(false, path, name) orElse
+      query_registry(true, path, name)
+
+
+  /* Cygwin installation */
+
+  private val CYGWIN_MOUNTS = "Software\\Cygnus Solutions\\Cygwin\\mounts v2"
+
+  def cygdrive(): Option[String] = query_registry(CYGWIN_MOUNTS, "cygdrive prefix")
+  def root(): Option[String] = query_registry(CYGWIN_MOUNTS + "\\/", "native")
+
+}
+
diff -r 1ba61c7b129f -r ff0ab207849a src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Sun Jun 07 20:57:24 2009 -0700
+++ b/src/Pure/System/isabelle_process.scala	Sun Jun 07 20:57:52 2009 -0700
@@ -230,7 +230,7 @@
 
   private class StdinThread(out_stream: OutputStream) extends Thread("isabelle: stdin") {
     override def run() = {
-      val writer = new BufferedWriter(new OutputStreamWriter(out_stream, isabelle_system.charset))
+      val writer = new BufferedWriter(new OutputStreamWriter(out_stream, IsabelleSystem.charset))
       var finished = false
       while (!finished) {
         try {
@@ -260,7 +260,7 @@
 
   private class StdoutThread(in_stream: InputStream) extends Thread("isabelle: stdout") {
     override def run() = {
-      val reader = new BufferedReader(new InputStreamReader(in_stream, isabelle_system.charset))
+      val reader = new BufferedReader(new InputStreamReader(in_stream, IsabelleSystem.charset))
       var result = new StringBuilder(100)
 
       var finished = false
diff -r 1ba61c7b129f -r ff0ab207849a src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sun Jun 07 20:57:24 2009 -0700
+++ b/src/Pure/System/isabelle_system.scala	Sun Jun 07 20:57:52 2009 -0700
@@ -12,10 +12,43 @@
 import scala.io.Source
 
 
-class IsabelleSystem {
+object IsabelleSystem
+{
 
   val charset = "UTF-8"
 
+  val is_cygwin = System.getProperty("os.name").startsWith("Windows")
+
+
+  /* shell processes */
+
+  private def raw_execute(env: Map[String, String], redirect: Boolean, args: String*): Process =
+  {
+    val cmdline = new java.util.LinkedList[String]
+    for (s <- args) cmdline.add(s)
+
+    val proc = new ProcessBuilder(cmdline)
+    proc.environment.clear
+    for ((x, y) <- env) proc.environment.put(x, y)
+    proc.redirectErrorStream(redirect)
+
+    try { proc.start }
+    catch { case e: IOException => error(e.getMessage) }
+  }
+
+  private def process_output(proc: Process): (String, Int) =
+  {
+    proc.getOutputStream.close
+    val output = Source.fromInputStream(proc.getInputStream, charset).mkString
+    val rc = proc.waitFor
+    (output, rc)
+  }
+
+}
+
+
+class IsabelleSystem
+{
 
   /* unique ids */
 
@@ -23,47 +56,99 @@
   def id(): String = synchronized { id_count += 1; "j" + id_count }
 
 
-  /* Isabelle environment settings */
-
-  private val environment = System.getenv
+  /* Isabelle settings environment */
 
-  def getenv(name: String) = {
-    val value = environment.get(if (name == "HOME") "HOME_JVM" else name)
-    if (value != null) value else ""
+  private val (cygdrive_pattern, cygwin_root, shell_prefix) =
+  {
+    if (IsabelleSystem.is_cygwin) {
+      val cygdrive = Cygwin.cygdrive getOrElse "/cygdrive"
+      val pattern = Pattern.compile(cygdrive + "/([a-zA-Z])($|/.*)")
+      val root = Cygwin.root getOrElse "C:\\cygwin"
+      val bash = List(root + "\\bin\\bash", "-l")
+      (Some(pattern), Some(root), bash)
+    }
+    else (None, None, Nil)
   }
 
-  def getenv_strict(name: String) = {
+  private val environment: Map[String, String] =
+  {
+    import scala.collection.jcl.Conversions._
+
+    val env0 = Map(java.lang.System.getenv.toList: _*)
+
+    val isabelle =
+      env0.get("ISABELLE_TOOL") match {
+        case None | Some("") =>
+          val isabelle = java.lang.System.getProperty("isabelle.tool")
+          if (isabelle == null || isabelle == "") "isabelle"
+          else isabelle
+        case Some(isabelle) => isabelle
+      }
+
+    val dump = File.createTempFile("isabelle", null)
+    try {
+      val cmdline = shell_prefix ::: List(isabelle, "getenv", "-d", dump.toString)
+      val proc = IsabelleSystem.raw_execute(env0, true, cmdline: _*)
+      val (output, rc) = IsabelleSystem.process_output(proc)
+      if (rc != 0) error(output)
+
+      val entries =
+        for (entry <- Source.fromFile(dump).mkString split "\0" if entry != "") yield {
+          val i = entry.indexOf('=')
+          if (i <= 0) (entry -> "")
+          else (entry.substring(0, i) -> entry.substring(i + 1))
+        }
+      Map(entries: _*)
+    }
+    finally { dump.delete }
+  }
+
+  def getenv(name: String): String =
+  {
+    environment.getOrElse(if (name == "HOME") "HOME_JVM" else name, "")
+  }
+
+  def getenv_strict(name: String): String =
+  {
     val value = getenv(name)
     if (value != "") value else error("Undefined environment variable: " + name)
   }
 
-  val is_cygwin = Pattern.matches(".*-cygwin", getenv_strict("ML_PLATFORM"))
-
 
   /* file path specifications */
 
-  private val cygdrive_pattern = Pattern.compile("/cygdrive/([a-zA-Z])($|/.*)")
-
-  def platform_path(source_path: String) = {
+  def platform_path(source_path: String): String =
+  {
     val result_path = new StringBuilder
 
-    def init(path: String) = {
-      val cygdrive = cygdrive_pattern.matcher(path)
-      if (cygdrive.matches) {
-        result_path.length = 0
-        result_path.append(cygdrive.group(1))
-        result_path.append(":")
-        result_path.append(File.separator)
-        cygdrive.group(2)
-      }
-      else if (path.startsWith("/")) {
+    def init_plain(path: String): String =
+    {
+      if (path.startsWith("/")) {
         result_path.length = 0
         result_path.append(getenv_strict("ISABELLE_ROOT_JVM"))
         path.substring(1)
       }
       else path
     }
-    def append(path: String) = {
+    def init(path: String): String =
+    {
+      cygdrive_pattern match {
+        case Some(pattern) =>
+          val cygdrive = pattern.matcher(path)
+          if (cygdrive.matches) {
+            result_path.length = 0
+            result_path.append(cygdrive.group(1))
+            result_path.append(":")
+            result_path.append(File.separator)
+            cygdrive.group(2)
+          }
+          else init_plain(path)
+        case None => init_plain(path)
+      }
+    }
+
+    def append(path: String)
+    {
       for (p <- init(path).split("/")) {
         if (p != "") {
           val len = result_path.length
@@ -82,17 +167,16 @@
     result_path.toString
   }
 
-  def platform_file(path: String) =
-    new File(platform_path(path))
+  def platform_file(path: String) = new File(platform_path(path))
 
 
   /* source files */
 
   private def try_file(file: File) = if (file.isFile) Some(file) else None
 
-  def source_file(path: String): Option[File] = {
-    if (path == "ML") None
-    else if (path.startsWith("/") || path == "")
+  def source_file(path: String): Option[File] =
+  {
+    if (path.startsWith("/") || path == "")
       try_file(platform_file(path))
     else {
       val pure_file = platform_file("~~/src/Pure/" + path)
@@ -104,59 +188,52 @@
   }
 
 
-  /* shell processes */
+  /* external processes */
 
-  def execute(redirect: Boolean, args: String*): Process = {
-    val cmdline = new java.util.LinkedList[String]
-    if (is_cygwin) cmdline.add(platform_path("/bin/env"))
-    for (s <- args) cmdline.add(s)
-
-    val proc = new ProcessBuilder(cmdline)
-    proc.environment.clear
-    proc.environment.putAll(environment)
-    proc.redirectErrorStream(redirect)
-    proc.start
+  def execute(redirect: Boolean, args: String*): Process =
+  {
+    val cmdline =
+      if (IsabelleSystem.is_cygwin) List(platform_path("/bin/env")) ++ args
+      else args
+    IsabelleSystem.raw_execute(environment, redirect, cmdline: _*)
   }
 
-
-  /* Isabelle tools (non-interactive) */
-
-  def isabelle_tool(args: String*) = {
-    val proc =
-      try { execute(true, (List(getenv_strict("ISABELLE_TOOL")) ++ args): _*) }
-      catch { case e: IOException => error(e.getMessage) }
-    proc.getOutputStream.close
-    val output = Source.fromInputStream(proc.getInputStream, charset).mkString
-    val rc = proc.waitFor
-    (output, rc)
+  def isabelle_tool(args: String*): (String, Int) =
+  {
+    val proc = execute(true, (List(getenv_strict("ISABELLE_TOOL")) ++ args): _*)
+    IsabelleSystem.process_output(proc)
   }
 
 
   /* named pipes */
 
-  def mk_fifo() = {
+  def mk_fifo(): String =
+  {
     val (result, rc) = isabelle_tool("mkfifo")
     if (rc == 0) result.trim
     else error(result)
   }
 
-  def rm_fifo(fifo: String) = {
+  def rm_fifo(fifo: String)
+  {
     val (result, rc) = isabelle_tool("rmfifo", fifo)
     if (rc != 0) error(result)
   }
 
-  def fifo_reader(fifo: String) = {
+  def fifo_reader(fifo: String): BufferedReader =
+  {
     // blocks until writer is ready
     val stream =
-      if (is_cygwin) execute(false, "cat", fifo).getInputStream
+      if (IsabelleSystem.is_cygwin) execute(false, "cat", fifo).getInputStream
       else new FileInputStream(fifo)
-    new BufferedReader(new InputStreamReader(stream, charset))
+    new BufferedReader(new InputStreamReader(stream, IsabelleSystem.charset))
   }
 
 
   /* find logics */
 
-  def find_logics() = {
+  def find_logics(): List[String] =
+  {
     val ml_ident = getenv_strict("ML_IDENTIFIER")
     var logics: Set[String] = Set()
     for (dir <- getenv_strict("ISABELLE_PATH").split(":")) {
@@ -171,7 +248,8 @@
 
   /* symbols */
 
-  private def read_symbols(path: String) = {
+  private def read_symbols(path: String): Iterator[String] =
+  {
     val file = new File(platform_path(path))
     if (file.isFile) Source.fromFile(file).getLines
     else Iterator.empty
diff -r 1ba61c7b129f -r ff0ab207849a src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Sun Jun 07 20:57:24 2009 -0700
+++ b/src/Pure/System/isar.ML	Sun Jun 07 20:57:52 2009 -0700
@@ -134,7 +134,7 @@
       NONE => if secure then quit () else ()
     | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
     handle exn =>
-      (Output.error_msg (Toplevel.exn_message exn)
+      (Output.error_msg (ML_Compiler.exn_message exn)
         handle crash =>
           (CRITICAL (fn () => change crashes (cons crash));
             warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
diff -r 1ba61c7b129f -r ff0ab207849a src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Sun Jun 07 20:57:24 2009 -0700
+++ b/src/Pure/System/session.ML	Sun Jun 07 20:57:52 2009 -0700
@@ -107,6 +107,6 @@
     |> setmp_noncritical Multithreading.max_threads
       (if Multithreading.available then max_threads
        else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
-  handle exn => (Output.error_msg (Toplevel.exn_message exn); exit 1);
+  handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
 
 end;