# HG changeset patch # User wenzelm # Date 1457600843 -3600 # Node ID a522a569283220dfb4e7cafe79417da11fa60b57 # Parent 5d4ed917450d180f53f96ba26e4ccb73e3b4f7fd clarified modules; diff -r 5d4ed917450d -r a522a5692832 bin/isabelle_process --- a/bin/isabelle_process Thu Mar 10 09:56:29 2016 +0100 +++ b/bin/isabelle_process Thu Mar 10 10:07:23 2016 +0100 @@ -15,4 +15,4 @@ isabelle_admin_build jars || exit $? -"$ISABELLE_TOOL" java isabelle.Isabelle_Process "$@" +"$ISABELLE_TOOL" java isabelle.ML_Process "$@" diff -r 5d4ed917450d -r a522a5692832 src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Thu Mar 10 09:56:29 2016 +0100 +++ b/src/Pure/System/isabelle_process.scala Thu Mar 10 10:07:23 2016 +0100 @@ -28,46 +28,6 @@ new Isabelle_Process(receiver, channel, process) } - - - /* command line entry point */ - - def main(args: Array[String]) - { - Command_Line.tool { - var eval_args: List[String] = Nil - var modes: List[String] = Nil - var options = Options.init() - - val getopts = Getopts(""" -Usage: isabelle_process [OPTIONS] [HEAP] - - Options are: - -e ML_EXPR evaluate ML expression on startup - -f ML_FILE evaluate ML file on startup - -m MODE add print mode for output - -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) - - If HEAP is a plain name (default $ISABELLE_LOGIC), it is searched in - $ISABELLE_PATH; if it contains a slash, it is taken as literal file; - if it is RAW_ML_SYSTEM, the initial ML heap is used. -""", - "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)), - "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)), - "m:" -> (arg => modes = arg :: modes), - "o:" -> (arg => options = options + arg)) - - val heap = - getopts(args) match { - case Nil => "" - case List(heap) => heap - case _ => getopts.usage() - } - - ML_Process(options, heap = heap, args = eval_args ::: args.toList, modes = modes). - result().print_stdout.rc - } - } } class Isabelle_Process private( diff -r 5d4ed917450d -r a522a5692832 src/Pure/System/ml_process.scala --- a/src/Pure/System/ml_process.scala Thu Mar 10 09:56:29 2016 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,115 +0,0 @@ -/* Title: Pure/System/ml_process.scala - Author: Makarius - -The underlying ML process. -*/ - -package isabelle - - -import java.io.{File => JFile} - - -object ML_Process -{ - def apply(options: Options, - heap: String = "", - args: List[String] = Nil, - modes: List[String] = Nil, - secure: Boolean = false, - cwd: JFile = null, - env: Map[String, String] = Map.empty, - redirect: Boolean = false, - channel: Option[System_Channel] = None): Bash.Process = - { - val load_heaps = - { - if (heap == "RAW_ML_SYSTEM") Nil - else if (heap.iterator.contains('/')) { - val heap_path = Path.explode(heap) - if (!heap_path.is_file) error("Bad heap file: " + heap_path) - List(heap_path) - } - else { - val dirs = Isabelle_System.find_logics_dirs() - val heap_name = if (heap == "") Isabelle_System.getenv_strict("ISABELLE_LOGIC") else heap - dirs.map(_ + Path.basic(heap_name)).find(_.is_file) match { - case Some(heap_path) => List(heap_path) - case None => - error("Unknown logic " + quote(heap) + " -- no heap file found in:\n" + - cat_lines(dirs.map(dir => " " + dir.implode))) - } - } - } - - val eval_heaps = - load_heaps.map(load_heap => - "(PolyML.SaveState.loadState " + ML_Syntax.print_string_raw(File.platform_path(load_heap)) + - "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " + - ML_Syntax.print_string_raw(": " + load_heap.toString + "\n") + - "); OS.Process.exit OS.Process.failure)") - - val eval_initial = - if (load_heaps.isEmpty) { - List( - if (Platform.is_windows) - "fun exit 0 = OS.Process.exit OS.Process.success" + - " | exit 1 = OS.Process.exit OS.Process.failure" + - " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))" - else - "fun exit rc = Posix.Process.exit (Word8.fromInt rc)", - "PolyML.Compiler.prompt1 := \"ML> \"", - "PolyML.Compiler.prompt2 := \"ML# \"") - } - else Nil - - val eval_modes = - if (modes.isEmpty) Nil - else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_raw _)(modes)) - - // options - val isabelle_process_options = Isabelle_System.tmp_file("options") - File.write(isabelle_process_options, YXML.string_of_body(options.encode)) - val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options)) - val eval_options = if (load_heaps.isEmpty) Nil else List("Options.load_default ()") - - val eval_secure = if (secure) List("Secure.set_secure ()") else Nil - - val eval_process = - if (load_heaps.isEmpty) - List("PolyML.print_depth 10") - else - channel match { - case None => - List("(default_print_depth 10; Isabelle_Process.init_options ())") - case Some(ch) => - List("(default_print_depth 10; Isabelle_Process.init_protocol " + - ML_Syntax.print_string_raw(ch.server_name) + ")") - } - - // bash - val bash_args = - Word.explode(Isabelle_System.getenv("ML_OPTIONS")) ::: - (eval_heaps ::: eval_initial ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process). - map(eval => List("--eval", eval)).flatten ::: args - - Bash.process( - """ - [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle - - export ISABELLE_PID="$$" - export ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID" - mkdir -p "$ISABELLE_TMP" - chmod $(umask -S) "$ISABELLE_TMP" - - librarypath "$ML_HOME" - "$ML_HOME/poly" -q """ + File.bash_args(bash_args) + """ - RC="$?" - - rm -f "$ISABELLE_PROCESS_OPTIONS" - rmdir "$ISABELLE_TMP" - - exit "$RC" - """, cwd = cwd, env = env ++ env_options, redirect = redirect) - } -} diff -r 5d4ed917450d -r a522a5692832 src/Pure/Tools/ml_console.scala --- a/src/Pure/Tools/ml_console.scala Thu Mar 10 09:56:29 2016 +0100 +++ b/src/Pure/Tools/ml_console.scala Thu Mar 10 10:07:23 2016 +0100 @@ -1,7 +1,7 @@ /* Title: Pure/Tools/ml_console.scala Author: Makarius -Run Isabelle process with raw ML console and line editor. +The raw ML process with interaction (line editor). */ package isabelle diff -r 5d4ed917450d -r a522a5692832 src/Pure/Tools/ml_process.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/ml_process.scala Thu Mar 10 10:07:23 2016 +0100 @@ -0,0 +1,155 @@ +/* Title: Pure/Tools/ml_process.scala + Author: Makarius + +The raw ML process. +*/ + +package isabelle + + +import java.io.{File => JFile} + + +object ML_Process +{ + def apply(options: Options, + heap: String = "", + args: List[String] = Nil, + modes: List[String] = Nil, + secure: Boolean = false, + cwd: JFile = null, + env: Map[String, String] = Map.empty, + redirect: Boolean = false, + channel: Option[System_Channel] = None): Bash.Process = + { + val load_heaps = + { + if (heap == "RAW_ML_SYSTEM") Nil + else if (heap.iterator.contains('/')) { + val heap_path = Path.explode(heap) + if (!heap_path.is_file) error("Bad heap file: " + heap_path) + List(heap_path) + } + else { + val dirs = Isabelle_System.find_logics_dirs() + val heap_name = if (heap == "") Isabelle_System.getenv_strict("ISABELLE_LOGIC") else heap + dirs.map(_ + Path.basic(heap_name)).find(_.is_file) match { + case Some(heap_path) => List(heap_path) + case None => + error("Unknown logic " + quote(heap) + " -- no heap file found in:\n" + + cat_lines(dirs.map(dir => " " + dir.implode))) + } + } + } + + val eval_heaps = + load_heaps.map(load_heap => + "(PolyML.SaveState.loadState " + ML_Syntax.print_string_raw(File.platform_path(load_heap)) + + "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " + + ML_Syntax.print_string_raw(": " + load_heap.toString + "\n") + + "); OS.Process.exit OS.Process.failure)") + + val eval_initial = + if (load_heaps.isEmpty) { + List( + if (Platform.is_windows) + "fun exit 0 = OS.Process.exit OS.Process.success" + + " | exit 1 = OS.Process.exit OS.Process.failure" + + " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))" + else + "fun exit rc = Posix.Process.exit (Word8.fromInt rc)", + "PolyML.Compiler.prompt1 := \"ML> \"", + "PolyML.Compiler.prompt2 := \"ML# \"") + } + else Nil + + val eval_modes = + if (modes.isEmpty) Nil + else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_raw _)(modes)) + + // options + val isabelle_process_options = Isabelle_System.tmp_file("options") + File.write(isabelle_process_options, YXML.string_of_body(options.encode)) + val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options)) + val eval_options = if (load_heaps.isEmpty) Nil else List("Options.load_default ()") + + val eval_secure = if (secure) List("Secure.set_secure ()") else Nil + + val eval_process = + if (load_heaps.isEmpty) + List("PolyML.print_depth 10") + else + channel match { + case None => + List("(default_print_depth 10; Isabelle_Process.init_options ())") + case Some(ch) => + List("(default_print_depth 10; Isabelle_Process.init_protocol " + + ML_Syntax.print_string_raw(ch.server_name) + ")") + } + + // bash + val bash_args = + Word.explode(Isabelle_System.getenv("ML_OPTIONS")) ::: + (eval_heaps ::: eval_initial ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process). + map(eval => List("--eval", eval)).flatten ::: args + + Bash.process( + """ + [ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle + + export ISABELLE_PID="$$" + export ISABELLE_TMP="$ISABELLE_TMP_PREFIX$ISABELLE_PID" + mkdir -p "$ISABELLE_TMP" + chmod $(umask -S) "$ISABELLE_TMP" + + librarypath "$ML_HOME" + "$ML_HOME/poly" -q """ + File.bash_args(bash_args) + """ + RC="$?" + + rm -f "$ISABELLE_PROCESS_OPTIONS" + rmdir "$ISABELLE_TMP" + + exit "$RC" + """, cwd = cwd, env = env ++ env_options, redirect = redirect) + } + + + /* command line entry point */ + + def main(args: Array[String]) + { + Command_Line.tool { + var eval_args: List[String] = Nil + var modes: List[String] = Nil + var options = Options.init() + + val getopts = Getopts(""" +Usage: isabelle_process [OPTIONS] [HEAP] + + Options are: + -e ML_EXPR evaluate ML expression on startup + -f ML_FILE evaluate ML file on startup + -m MODE add print mode for output + -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + + If HEAP is a plain name (default $ISABELLE_LOGIC), it is searched in + $ISABELLE_PATH; if it contains a slash, it is taken as literal file; + if it is RAW_ML_SYSTEM, the initial ML heap is used. +""", + "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)), + "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)), + "m:" -> (arg => modes = arg :: modes), + "o:" -> (arg => options = options + arg)) + + val heap = + getopts(args) match { + case Nil => "" + case List(heap) => heap + case _ => getopts.usage() + } + + ML_Process(options, heap = heap, args = eval_args ::: args.toList, modes = modes). + result().print_stdout.rc + } + } +} diff -r 5d4ed917450d -r a522a5692832 src/Pure/build-jars --- a/src/Pure/build-jars Thu Mar 10 09:56:29 2016 +0100 +++ b/src/Pure/build-jars Thu Mar 10 10:07:23 2016 +0100 @@ -81,7 +81,6 @@ System/isabelle_charset.scala System/isabelle_process.scala System/isabelle_system.scala - System/ml_process.scala System/options.scala System/platform.scala System/posix_interrupt.scala @@ -103,6 +102,7 @@ Tools/doc.scala Tools/main.scala Tools/ml_console.scala + Tools/ml_process.scala Tools/ml_statistics.scala Tools/news.scala Tools/print_operation.scala