--- 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=""
--- 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.
*}
--- 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%
%
--- 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
+
--- 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;
--- 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);
--- 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";
--- 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"
--- 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;
--- 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
--- /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;
+
--- 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;
--- 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;
--- 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 =
--- 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 =
--- 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
--- 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;
--- 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 =
--- 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
--- 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
--- 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";
--- /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")
+
+}
+
--- 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
--- 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
--- 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");
--- 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;