# HG changeset patch # User wenzelm # Date 1613858495 -3600 # Node ID 440546ea20e61f784461b59e62fbe047abee5415 # Parent ad60214bef094fdadab92e90952aaca6b23261d6 clarified modules; diff -r ad60214bef09 -r 440546ea20e6 src/HOL/Tools/Nunchaku/nunchaku_tool.ML --- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Sat Feb 20 22:09:16 2021 +0100 +++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML Sat Feb 20 23:01:35 2021 +0100 @@ -74,11 +74,6 @@ | CVC4_Not_Found | Unknown_Error of int * string; -fun bash_output_error s = - let val {out, err, rc, ...} = Bash.process s in - ((out, err), rc) - end; - val nunchaku_home_env_var = "NUNCHAKU_HOME"; val unknown_solver = "unknown"; @@ -108,7 +103,7 @@ [bash_cmd, "This file was generated by Isabelle (most likely Nunchaku)", timestamp ()]; val prob_str = cat_lines (map (prefix "# ") comments) ^ "\n\n" ^ str_of_nun_problem problem; val _ = File.write prob_path prob_str; - val ((output, error), code) = bash_output_error bash_cmd; + val {out = output, err = error, rc = code, ...} = Isabelle_System.bash_process bash_cmd; val backend = (case map_filter (try (unprefix "{backend:")) (split_lines output) of diff -r ad60214bef09 -r 440546ea20e6 src/Pure/General/file.ML --- a/src/Pure/General/file.ML Sat Feb 20 22:09:16 2021 +0100 +++ b/src/Pure/General/file.ML Sat Feb 20 23:01:35 2021 +0100 @@ -48,10 +48,10 @@ val standard_path = Path.implode o Path.expand; val platform_path = ML_System.platform_path o standard_path; -val bash_path = Bash_Syntax.string o standard_path; -val bash_paths = Bash_Syntax.strings o map standard_path; +val bash_path = Bash.string o standard_path; +val bash_paths = Bash.strings o map standard_path; -val bash_platform_path = Bash_Syntax.string o platform_path; +val bash_platform_path = Bash.string o platform_path; (* full_path *) diff -r ad60214bef09 -r 440546ea20e6 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sat Feb 20 22:09:16 2021 +0100 +++ b/src/Pure/ROOT.ML Sat Feb 20 23:01:35 2021 +0100 @@ -79,7 +79,7 @@ ML_file "PIDE/xml.ML"; ML_file "General/path.ML"; ML_file "General/url.ML"; -ML_file "System/bash_syntax.ML"; +ML_file "System/bash.ML"; ML_file "General/file.ML"; ML_file "General/long_name.ML"; ML_file "General/binding.ML"; @@ -294,7 +294,6 @@ (*Isabelle system*) ML_file "PIDE/protocol_command.ML"; ML_file "System/scala.ML"; -ML_file "System/bash.ML"; ML_file "System/isabelle_system.ML"; diff -r ad60214bef09 -r 440546ea20e6 src/Pure/System/bash.ML --- a/src/Pure/System/bash.ML Sat Feb 20 22:09:16 2021 +0100 +++ b/src/Pure/System/bash.ML Sat Feb 20 23:01:35 2021 +0100 @@ -1,36 +1,35 @@ (* Title: Pure/System/bash.ML Author: Makarius -GNU bash processes, with propagation of interrupts -- POSIX version. +Syntax for GNU bash. *) signature BASH = sig val string: string -> string val strings: string list -> string - val process: string -> {out: string, err: string, rc: int} end; structure Bash: BASH = struct -val string = Bash_Syntax.string; -val strings = Bash_Syntax.strings; +fun string "" = "\"\"" + | string str = + str |> translate_string (fn ch => + let val c = ord ch in + (case ch of + "\t" => "$'\\t'" + | "\n" => "$'\\n'" + | "\f" => "$'\\f'" + | "\r" => "$'\\r'" + | _ => + if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse + exists_string (fn c => c = ch) "+,-./:_" then ch + else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'" + else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'" + else "\\" ^ ch) + end); -fun process script = - Scala.function_thread "bash_process" - ("export ISABELLE_TMP=" ^ string (getenv "ISABELLE_TMP") ^ "\n" ^ script) - |> YXML.parse_body - |> - let open XML.Decode in - variant - [fn ([], []) => raise Exn.Interrupt, - fn ([], a) => error (YXML.string_of_body a), - fn ([a], c) => - let - val rc = int_atom a; - val (out, err) = pair I I c |> apply2 YXML.string_of_body; - in {out = out, err = err, rc = rc} end] - end; +val strings = space_implode " " o map string; end; diff -r ad60214bef09 -r 440546ea20e6 src/Pure/System/bash_syntax.ML --- a/src/Pure/System/bash_syntax.ML Sat Feb 20 22:09:16 2021 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,35 +0,0 @@ -(* Title: Pure/System/bash_syntax.ML - Author: Makarius - -Syntax for GNU bash (see also Pure/System/bash.ML). -*) - -signature BASH_SYNTAX = -sig - val string: string -> string - val strings: string list -> string -end; - -structure Bash_Syntax: BASH_SYNTAX = -struct - -fun string "" = "\"\"" - | string str = - str |> translate_string (fn ch => - let val c = ord ch in - (case ch of - "\t" => "$'\\t'" - | "\n" => "$'\\n'" - | "\f" => "$'\\f'" - | "\r" => "$'\\r'" - | _ => - if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse - exists_string (fn c => c = ch) "+,-./:_" then ch - else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'" - else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'" - else "\\" ^ ch) - end); - -val strings = space_implode " " o map string; - -end; diff -r ad60214bef09 -r 440546ea20e6 src/Pure/System/isabelle_system.ML --- a/src/Pure/System/isabelle_system.ML Sat Feb 20 22:09:16 2021 +0100 +++ b/src/Pure/System/isabelle_system.ML Sat Feb 20 23:01:35 2021 +0100 @@ -6,6 +6,7 @@ signature ISABELLE_SYSTEM = sig + val bash_process: string -> {out: string, err: string, rc: int} val bash_output_check: string -> string val bash_output: string -> string * int val bash: string -> int @@ -28,14 +29,30 @@ (* bash *) +fun bash_process script = + Scala.function_thread "bash_process" + ("export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP") ^ "\n" ^ script) + |> YXML.parse_body + |> + let open XML.Decode in + variant + [fn ([], []) => raise Exn.Interrupt, + fn ([], a) => error (YXML.string_of_body a), + fn ([a], c) => + let + val rc = int_atom a; + val (out, err) = pair I I c |> apply2 YXML.string_of_body; + in {out = out, err = err, rc = rc} end] + end; + fun bash_output_check s = - (case Bash.process s of + (case bash_process s of {rc = 0, out, ...} => trim_line out | {err, ...} => error (trim_line err)); fun bash_output s = let - val {out, err, rc, ...} = Bash.process s; + val {out, err, rc, ...} = bash_process s; val _ = warning (trim_line err); in (out, rc) end; @@ -127,7 +144,7 @@ fun download url = with_tmp_file "download" "" (fn path => ("curl --fail --silent --location " ^ Bash.string url ^ " > " ^ File.bash_path path) - |> Bash.process + |> bash_process |> (fn {rc = 0, ...} => File.read path | {err, ...} => cat_error ("Failed to download " ^ quote url) err)); diff -r ad60214bef09 -r 440546ea20e6 src/Pure/Tools/ghc.ML --- a/src/Pure/Tools/ghc.ML Sat Feb 20 22:09:16 2021 +0100 +++ b/src/Pure/Tools/ghc.ML Sat Feb 20 23:01:35 2021 +0100 @@ -84,8 +84,9 @@ val template_path = dir + (Path.basic name |> Path.ext "hsfiles"); val _ = File.write template_path (project_template {depends = depends, modules = modules}); val {rc, err, ...} = - Bash.process ("cd " ^ File.bash_path dir ^ "; isabelle ghc_stack new " ^ Bash.string name ^ - " --bare " ^ File.bash_platform_path template_path); + Isabelle_System.bash_process + ("cd " ^ File.bash_path dir ^ "; isabelle ghc_stack new " ^ Bash.string name ^ + " --bare " ^ File.bash_platform_path template_path); in if rc = 0 then () else error err end; end;