# HG changeset patch # User wenzelm # Date 1459792134 -7200 # Node ID 1f1a2c33ccf4b9d1f2caeced3d7e7653cc340132 # Parent caaa2fc4040db04a12e6379850ee1893866983f3 clarified conditional compilation; diff -r caaa2fc4040d -r 1f1a2c33ccf4 src/HOL/ex/Cartouche_Examples.thy --- 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 \Nested ML evaluation:\ ML \ - val ML = ML_Context.eval_source ML_Compiler.flags; - ML \ML \val a = @{thm refl}\\; ML \val b = @{thm sym}\; val c = @{thm trans} diff -r caaa2fc4040d -r 1f1a2c33ccf4 src/Pure/ML/ml_antiquotation.ML --- 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; diff -r caaa2fc4040d -r 1f1a2c33ccf4 src/Pure/ML/ml_antiquotations.ML --- 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} diff -r caaa2fc4040d -r 1f1a2c33ccf4 src/Pure/ML/ml_context.ML --- 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; diff -r caaa2fc4040d -r 1f1a2c33ccf4 src/Pure/ROOT --- 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" diff -r caaa2fc4040d -r 1f1a2c33ccf4 src/Pure/ROOT.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"; diff -r caaa2fc4040d -r 1f1a2c33ccf4 src/Pure/System/bash.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 +\ +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; +\ +else ML +\ structure Bash: BASH = struct @@ -99,4 +192,4 @@ end); end; - +\; diff -r caaa2fc4040d -r 1f1a2c33ccf4 src/Pure/System/bash_windows.ML --- 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;