--- a/src/HOL/ex/Cartouche_Examples.thy Mon Apr 04 17:25:53 2016 +0200
+++ b/src/HOL/ex/Cartouche_Examples.thy Mon Apr 04 19:48:54 2016 +0200
@@ -274,8 +274,6 @@
text \<open>Nested ML evaluation:\<close>
ML \<open>
- val ML = ML_Context.eval_source ML_Compiler.flags;
-
ML \<open>ML \<open>val a = @{thm refl}\<close>\<close>;
ML \<open>val b = @{thm sym}\<close>;
val c = @{thm trans}
--- a/src/Pure/ML/ml_antiquotation.ML Mon Apr 04 17:25:53 2016 +0200
+++ b/src/Pure/ML/ml_antiquotation.ML Mon Apr 04 19:48:54 2016 +0200
@@ -42,6 +42,11 @@
(Args.context >> (ML_Pretty.make_string_fn o ML_Context.struct_name)) #>
value (Binding.make ("binding", @{here}))
- (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding));
+ (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
+
+ value (Binding.make ("cartouche", @{here}))
+ (Scan.lift Args.cartouche_input >> (fn source =>
+ "Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^
+ ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))));
end;
--- a/src/Pure/ML/ml_antiquotations.ML Mon Apr 04 17:25:53 2016 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML Mon Apr 04 19:48:54 2016 +0200
@@ -10,12 +10,7 @@
(* ML support *)
val _ = Theory.setup
- (ML_Antiquotation.value @{binding cartouche}
- (Scan.lift Args.cartouche_input >> (fn source =>
- "Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^
- ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))) #>
-
- ML_Antiquotation.inline @{binding undefined}
+ (ML_Antiquotation.inline @{binding undefined}
(Scan.succeed "(raise General.Match)") #>
ML_Antiquotation.inline @{binding assert}
--- a/src/Pure/ML/ml_context.ML Mon Apr 04 17:25:53 2016 +0200
+++ b/src/Pure/ML/ml_context.ML Mon Apr 04 19:48:54 2016 +0200
@@ -237,3 +237,4 @@
end;
+val ML = ML_Context.eval_source ML_Compiler.flags;
--- a/src/Pure/ROOT Mon Apr 04 17:25:53 2016 +0200
+++ b/src/Pure/ROOT Mon Apr 04 19:48:54 2016 +0200
@@ -155,7 +155,6 @@
"Syntax/term_position.ML"
"Syntax/type_annotation.ML"
"System/bash.ML"
- "System/bash_windows.ML"
"System/command_line.ML"
"System/distribution.ML"
"System/invoke_scala.ML"
--- a/src/Pure/ROOT.ML Mon Apr 04 17:25:53 2016 +0200
+++ b/src/Pure/ROOT.ML Mon Apr 04 19:48:54 2016 +0200
@@ -280,9 +280,7 @@
use "Proof/extraction.ML";
(*Isabelle system*)
-if ML_System.platform_is_windows
-then use "System/bash_windows.ML"
-else use "System/bash.ML";
+use "System/bash.ML";
use "System/isabelle_system.ML";
--- a/src/Pure/System/bash.ML Mon Apr 04 17:25:53 2016 +0200
+++ b/src/Pure/System/bash.ML Mon Apr 04 19:48:54 2016 +0200
@@ -1,7 +1,7 @@
(* Title: Pure/System/bash.ML
Author: Makarius
-GNU bash processes, with propagation of interrupts -- POSIX version.
+GNU bash processes, with propagation of interrupts.
*)
signature BASH =
@@ -9,6 +9,99 @@
val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
end;
+if ML_System.platform_is_windows then ML
+\<open>
+structure Bash: BASH =
+struct
+
+val process = uninterruptible (fn restore_attributes => fn script =>
+ let
+ datatype result = Wait | Signal | Result of int;
+ val result = Synchronized.var "bash_result" Wait;
+
+ val id = serial_string ();
+ val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
+ val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
+ val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
+ val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
+
+ fun cleanup_files () =
+ (try File.rm script_path;
+ try File.rm out_path;
+ try File.rm err_path;
+ try File.rm pid_path);
+ val _ = cleanup_files ();
+
+ val system_thread =
+ Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
+ Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
+ let
+ val _ = File.write script_path script;
+ val bash_script =
+ "bash " ^ File.bash_path script_path ^
+ " > " ^ File.bash_path out_path ^
+ " 2> " ^ File.bash_path err_path;
+ val bash_process = getenv_strict "ISABELLE_BASH_PROCESS";
+ val rc =
+ Windows.simpleExecute ("",
+ quote (ML_System.platform_path bash_process) ^ " " ^
+ quote (File.platform_path pid_path) ^ " \"\" bash -c " ^ quote bash_script)
+ |> Windows.fromStatus |> SysWord.toInt;
+ val res = if rc = 130 orelse rc = 512 then Signal else Result rc;
+ in Synchronized.change result (K res) end
+ handle exn =>
+ (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
+
+ fun read_pid 0 = NONE
+ | read_pid count =
+ (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
+ NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
+ | some => some);
+
+ fun terminate NONE = ()
+ | terminate (SOME pid) =
+ let
+ fun kill s =
+ let
+ val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe";
+ val arg = "kill -" ^ s ^ " -" ^ string_of_int pid;
+ in
+ OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg))
+ handle OS.SysErr _ => false
+ end;
+
+ fun multi_kill count s =
+ count = 0 orelse
+ (kill s; kill "0") andalso
+ (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
+ val _ =
+ multi_kill 10 "INT" andalso
+ multi_kill 10 "TERM" andalso
+ multi_kill 10 "KILL";
+ in () end;
+
+ fun cleanup () =
+ (Standard_Thread.interrupt_unsynchronized system_thread;
+ cleanup_files ());
+ in
+ let
+ val _ =
+ restore_attributes (fn () =>
+ Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
+
+ val out = the_default "" (try File.read out_path);
+ val err = the_default "" (try File.read err_path);
+ val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
+ val pid = read_pid 1;
+ val _ = cleanup ();
+ in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
+ handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
+ end);
+
+end;
+\<close>
+else ML
+\<open>
structure Bash: BASH =
struct
@@ -99,4 +192,4 @@
end);
end;
-
+\<close>;
--- a/src/Pure/System/bash_windows.ML Mon Apr 04 17:25:53 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,99 +0,0 @@
-(* Title: Pure/System/bash_windows.ML
- Author: Makarius
-
-GNU bash processes, with propagation of interrupts -- Windows version.
-*)
-
-signature BASH =
-sig
- val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
-end;
-
-structure Bash: BASH =
-struct
-
-val process = uninterruptible (fn restore_attributes => fn script =>
- let
- datatype result = Wait | Signal | Result of int;
- val result = Synchronized.var "bash_result" Wait;
-
- val id = serial_string ();
- val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
- val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
- val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
- val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
-
- fun cleanup_files () =
- (try File.rm script_path;
- try File.rm out_path;
- try File.rm err_path;
- try File.rm pid_path);
- val _ = cleanup_files ();
-
- val system_thread =
- Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
- Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
- let
- val _ = File.write script_path script;
- val bash_script =
- "bash " ^ File.bash_path script_path ^
- " > " ^ File.bash_path out_path ^
- " 2> " ^ File.bash_path err_path;
- val bash_process = getenv_strict "ISABELLE_BASH_PROCESS";
- val rc =
- Windows.simpleExecute ("",
- quote (ML_System.platform_path bash_process) ^ " " ^
- quote (File.platform_path pid_path) ^ " \"\" bash -c " ^ quote bash_script)
- |> Windows.fromStatus |> SysWord.toInt;
- val res = if rc = 130 orelse rc = 512 then Signal else Result rc;
- in Synchronized.change result (K res) end
- handle exn =>
- (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
-
- fun read_pid 0 = NONE
- | read_pid count =
- (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
- NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
- | some => some);
-
- fun terminate NONE = ()
- | terminate (SOME pid) =
- let
- fun kill s =
- let
- val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe";
- val arg = "kill -" ^ s ^ " -" ^ string_of_int pid;
- in
- OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg))
- handle OS.SysErr _ => false
- end;
-
- fun multi_kill count s =
- count = 0 orelse
- (kill s; kill "0") andalso
- (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
- val _ =
- multi_kill 10 "INT" andalso
- multi_kill 10 "TERM" andalso
- multi_kill 10 "KILL";
- in () end;
-
- fun cleanup () =
- (Standard_Thread.interrupt_unsynchronized system_thread;
- cleanup_files ());
- in
- let
- val _ =
- restore_attributes (fn () =>
- Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
-
- val out = the_default "" (try File.read out_path);
- val err = the_default "" (try File.read err_path);
- val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
- val pid = read_pid 1;
- val _ = cleanup ();
- in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
- handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
- end);
-
-end;