diff --git a/src/Pure/ML/ml_process.scala b/src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala +++ b/src/Pure/ML/ml_process.scala @@ -1,204 +1,204 @@ /* Title: Pure/ML/ml_process.scala Author: Makarius The raw ML process. */ package isabelle import java.io.{File => JFile} object ML_Process { def apply(options: Options, sessions_structure: Sessions.Structure, store: Sessions.Store, logic: String = "", raw_ml_system: Boolean = false, use_prelude: List[String] = Nil, eval_main: String = "", args: List[String] = Nil, modes: List[String] = Nil, cwd: JFile = null, env: Map[String, String] = Isabelle_System.settings(), redirect: Boolean = false, cleanup: () => Unit = () => (), session_base: Option[Sessions.Base] = None): Bash.Process = { val logic_name = Isabelle_System.default_logic(logic) val heaps: List[String] = if (raw_ml_system) Nil else { sessions_structure.selection(logic_name). build_requirements(List(logic_name)). map(a => File.platform_path(store.the_heap(a))) } val eval_init = if (heaps.isEmpty) { List( """ fun chapter (_: string) = (); fun section (_: string) = (); fun subsection (_: string) = (); fun subsubsection (_: string) = (); fun paragraph (_: string) = (); fun subparagraph (_: string) = (); val ML_file = PolyML.use; """, 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 := \"Poly/ML> \"", "PolyML.Compiler.prompt2 := \"Poly/ML# \"") } else List( "(PolyML.SaveState.loadHierarchy " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) + "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " + ML_Syntax.print_string_bytes(": " + logic_name + "\n") + "); OS.Process.exit OS.Process.failure)") val eval_modes = if (modes.isEmpty) Nil else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(modes)) // options val isabelle_process_options = Isabelle_System.tmp_file("options") Isabelle_System.chmod("600", File.path(isabelle_process_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 (heaps.isEmpty) Nil else List("Options.load_default ()") // session base val eval_session_base = session_base match { case None => Nil case Some(base) => def print_table(table: List[(String, String)]): String = ML_Syntax.print_list( ML_Syntax.print_pair( ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))(table) - def print_list(list: List[String]): String = - ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list) - def print_sessions(list: List[(String, Position.T)]): String = + def print_list: List[String] => String = + ML_Syntax.print_list(ML_Syntax.print_string_bytes) + def print_sessions: List[(String, Position.T)] => String = ML_Syntax.print_list( - ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list) - def print_bibtex_entries(list: List[(String, List[String])]): String = + ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties)) + def print_bibtex_entries: List[(String, List[String])] => String = ML_Syntax.print_list( ML_Syntax.print_pair(ML_Syntax.print_string_bytes, - ML_Syntax.print_list(ML_Syntax.print_string_bytes)))(list) + ML_Syntax.print_list(ML_Syntax.print_string_bytes))) List("Resources.init_session" + "{session_positions = " + print_sessions(sessions_structure.session_positions) + ", session_directories = " + print_table(sessions_structure.dest_session_directories) + ", bibtex_entries = " + print_bibtex_entries(sessions_structure.bibtex_entries) + ", docs = " + print_list(base.doc_names) + ", global_theories = " + print_table(base.global_theories.toList) + ", loaded_theories = " + print_list(base.loaded_theories.keys) + "}") } // process val eval_process = proper_string(eval_main).getOrElse( if (heaps.isEmpty) { "PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")) } else "Isabelle_Process.init ()") // ISABELLE_TMP val isabelle_tmp = Isabelle_System.tmp_dir("process") val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp), "POLYSTATSDIR" -> isabelle_tmp.getAbsolutePath) val env_functions = Map("ISABELLE_SCALA_FUNCTIONS" -> Scala.functions.mkString(",")) val ml_runtime_options = { val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS")) val ml_options1 = if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options else ml_options ::: List("--gcthreads", options.int("threads").toString) val ml_options2 = if (!Platform.is_windows || ml_options.exists(_.containsSlice("codepage"))) ml_options1 else ml_options1 ::: List("--codepage", "utf8") ml_options2 ::: List("--exportstats") } // bash val bash_args = ml_runtime_options ::: (eval_init ::: eval_modes ::: eval_options ::: eval_session_base).flatMap(List("--eval", _)) ::: use_prelude.flatMap(List("--use", _)) ::: List("--eval", eval_process) ::: args Bash.process( "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ + Bash.strings(bash_args), cwd = cwd, env = env ++ env_options ++ env_tmp ++ env_functions, redirect = redirect, cleanup = () => { isabelle_process_options.delete Isabelle_System.rm_tree(isabelle_tmp) cleanup() }) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args => { var dirs: List[Path] = Nil var eval_args: List[String] = Nil var logic = Isabelle_System.getenv("ISABELLE_LOGIC") var modes: List[String] = Nil var options = Options.init() val getopts = Getopts(""" Usage: isabelle process [OPTIONS] Options are: -T THEORY load theory -d DIR include session directory -e ML_EXPR evaluate ML expression on startup -f ML_FILE evaluate ML file on startup -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) -m MODE add print mode for output -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) Run the raw Isabelle ML process in batch mode. """, "T:" -> (arg => eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string_bytes(arg))), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)), "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)), "l:" -> (arg => logic = arg), "m:" -> (arg => modes = arg :: modes), "o:" -> (arg => options = options + arg)) val more_args = getopts(args) if (args.isEmpty || more_args.nonEmpty) getopts.usage() val sessions_structure = Sessions.load_structure(options, dirs = dirs) val store = Sessions.store(options) val result = ML_Process(options, sessions_structure, store, logic = logic, args = eval_args, modes = modes) .result( progress_stdout = Output.writeln(_, stdout = true), progress_stderr = Output.writeln(_)) sys.exit(result.rc) }) } diff --git a/src/Pure/PIDE/protocol.scala b/src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala +++ b/src/Pure/PIDE/protocol.scala @@ -1,446 +1,433 @@ /* Title: Pure/PIDE/protocol.scala Author: Makarius Protocol message formats for interactive proof documents. */ package isabelle object Protocol { /* markers for inlined messages */ val Loading_Theory_Marker = Protocol_Message.Marker("loading_theory") val Meta_Info_Marker = Protocol_Message.Marker("meta_info") val Command_Timing_Marker = Protocol_Message.Marker("command_timing") val Theory_Timing_Marker = Protocol_Message.Marker("theory_timing") val Session_Timing_Marker = Protocol_Message.Marker("session_timing") val ML_Statistics_Marker = Protocol_Message.Marker("ML_statistics") val Task_Statistics_Marker = Protocol_Message.Marker("task_statistics") val Error_Message_Marker = Protocol_Message.Marker("error_message") /* document editing */ object Commands_Accepted { def unapply(text: String): Option[List[Document_ID.Command]] = try { Some(space_explode(',', text).map(Value.Long.parse)) } catch { case ERROR(_) => None } val message: XML.Elem = XML.elem(Markup.STATUS, List(XML.elem(Markup.ACCEPTED))) } object Assign_Update { def unapply(text: String) : Option[(Document_ID.Version, List[String], Document.Assign_Update)] = { try { import XML.Decode._ def decode_upd(body: XML.Body): (Long, List[Long]) = space_explode(',', string(body)).map(Value.Long.parse) match { case a :: bs => (a, bs) case _ => throw new XML.XML_Body(body) } Some(triple(long, list(string), list(decode_upd))(Symbol.decode_yxml(text))) } catch { case ERROR(_) => None case _: XML.Error => None } } } object Removed { def unapply(text: String): Option[List[Document_ID.Version]] = try { import XML.Decode._ Some(list(long)(Symbol.decode_yxml(text))) } catch { case ERROR(_) => None case _: XML.Error => None } } /* command timing */ object Command_Timing { def unapply(props: Properties.T): Option[(Properties.T, Document_ID.Generic, isabelle.Timing)] = props match { case Markup.Command_Timing(args) => (args, args) match { case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((args, id, timing)) case _ => None } case _ => None } } /* theory timing */ object Theory_Timing { def unapply(props: Properties.T): Option[(String, isabelle.Timing)] = props match { case Markup.Theory_Timing(args) => (args, args) match { case (Markup.Name(name), Markup.Timing_Properties(timing)) => Some((name, timing)) case _ => None } case _ => None } } /* result messages */ def is_message(pred: XML.Elem => Boolean, body: XML.Body): Boolean = body match { case List(elem: XML.Elem) => pred(elem) case _ => false } def is_result(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.RESULT, _), _) => true case _ => false } def is_tracing(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.TRACING, _), _) => true case XML.Elem(Markup(Markup.TRACING_MESSAGE, _), _) => true case _ => false } def is_state(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.STATE, _), _) => true case XML.Elem(Markup(Markup.STATE_MESSAGE, _), _) => true case _ => false } def is_information(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.INFORMATION, _), _) => true case XML.Elem(Markup(Markup.INFORMATION_MESSAGE, _), _) => true case _ => false } def is_writeln(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.WRITELN, _), _) => true case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _), _) => true case _ => false } def is_warning(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.WARNING, _), _) => true case XML.Elem(Markup(Markup.WARNING_MESSAGE, _), _) => true case _ => false } def is_legacy(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.LEGACY, _), _) => true case XML.Elem(Markup(Markup.LEGACY_MESSAGE, _), _) => true case _ => false } def is_error(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.ERROR, _), _) => true case XML.Elem(Markup(Markup.ERROR_MESSAGE, _), _) => true case _ => false } def is_inlined(msg: XML.Tree): Boolean = !(is_result(msg) || is_tracing(msg) || is_state(msg)) def is_exported(msg: XML.Tree): Boolean = is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg) def message_text(body: XML.Body, margin: Double = Pretty.default_margin, breakgain: Double = Pretty.default_breakgain, metric: Pretty.Metric = Pretty.Default_Metric): String = { val text = Pretty.string_of(Protocol_Message.expose_no_reports(body), margin = margin, breakgain = breakgain, metric = metric) if (is_message(is_warning, body) || is_message(is_legacy, body)) Output.warning_prefix(text) else if (is_message(is_error, body)) Output.error_prefix(text) else text } /* export */ object Export { sealed case class Args( id: Option[String], serial: Long, theory_name: String, name: String, executable: Boolean, compress: Boolean, strict: Boolean) { def compound_name: String = isabelle.Export.compound_name(theory_name, name) } def unapply(props: Properties.T): Option[Args] = props match { case List( (Markup.FUNCTION, Markup.EXPORT), (Markup.ID, id), (Markup.SERIAL, Value.Long(serial)), (Markup.THEORY_NAME, theory_name), (Markup.NAME, name), (Markup.EXECUTABLE, Value.Boolean(executable)), (Markup.COMPRESS, Value.Boolean(compress)), (Markup.STRICT, Value.Boolean(strict))) => Some(Args(proper_string(id), serial, theory_name, name, executable, compress, strict)) case _ => None } } /* breakpoints */ object ML_Breakpoint { def unapply(tree: XML.Tree): Option[Long] = tree match { case XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(breakpoint)), _) => Some(breakpoint) case _ => None } } /* dialogs */ object Dialog_Args { def unapply(props: Properties.T): Option[(Document_ID.Generic, Long, String)] = (props, props, props) match { case (Position.Id(id), Markup.Serial(serial), Markup.Result(result)) => Some((id, serial, result)) case _ => None } } object Dialog { def unapply(tree: XML.Tree): Option[(Document_ID.Generic, Long, String)] = tree match { case XML.Elem(Markup(Markup.DIALOG, Dialog_Args(id, serial, result)), _) => Some((id, serial, result)) case _ => None } } object Dialog_Result { def apply(id: Document_ID.Generic, serial: Long, result: String): XML.Elem = { val props = Position.Id(id) ::: Markup.Serial(serial) XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result))) } def unapply(tree: XML.Tree): Option[String] = tree match { case XML.Elem(Markup(Markup.RESULT, _), List(XML.Text(result))) => Some(result) case _ => None } } } trait Protocol { /* protocol commands */ def protocol_command_raw(name: String, args: List[Bytes]): Unit def protocol_command_args(name: String, args: List[String]) def protocol_command(name: String, args: String*): Unit /* options */ def options(opts: Options): Unit = protocol_command("Prover.options", Symbol.encode_yxml(opts.encode)) /* session base */ - private def encode_table(table: List[(String, String)]): String = - { - import XML.Encode._ - Symbol.encode_yxml(list(pair(string, string))(table)) - } - - private def encode_list(lst: List[String]): String = + def init_session(resources: Resources) { import XML.Encode._ - Symbol.encode_yxml(list(string)(lst)) - } - private def encode_sessions(lst: List[(String, Position.T)]): String = - { - import XML.Encode._ - Symbol.encode_yxml(list(pair(string, properties))(lst)) - } + def encode_table(arg: List[(String, String)]): String = + Symbol.encode_yxml(list(pair(string, string))(arg)) + def encode_list(arg: List[String]): String = + Symbol.encode_yxml(list(string)(arg)) + def encode_sessions(arg: List[(String, Position.T)]): String = + Symbol.encode_yxml(list(pair(string, properties))(arg)) + def encode_bibtex_entries(arg: List[(String, List[String])]): String = + Symbol.encode_yxml(list(pair(string, list(string)))(arg)) - private def encode_bibtex_entries(lst: List[(String, List[String])]): String = - { - import XML.Encode._ - Symbol.encode_yxml(list(pair(string, list(string)))(lst)) - } - - def init_session(resources: Resources) - { protocol_command("Prover.init_session", encode_sessions(resources.sessions_structure.session_positions), encode_table(resources.sessions_structure.dest_session_directories), encode_bibtex_entries(resources.sessions_structure.bibtex_entries), encode_list(resources.session_base.doc_names), encode_table(resources.session_base.global_theories.toList), encode_list(resources.session_base.loaded_theories.keys)) } /* interned items */ def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit = protocol_command_raw("Document.define_blob", List(Bytes(digest.toString), bytes)) private def encode_command(command: Command): (String, String, String, String, List[String]) = { import XML.Encode._ val blobs_yxml = { val encode_blob: T[Command.Blob] = variant(List( { case Exn.Res((a, b)) => (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) }, { case Exn.Exn(e) => (Nil, string(Exn.message(e))) })) Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index)) } val toks_yxml = { val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source)))) Symbol.encode_yxml(list(encode_tok)(command.span.content)) } val toks_sources = command.span.content.map(tok => Symbol.encode(tok.source)) (Document_ID(command.id), Symbol.encode(command.span.name), blobs_yxml, toks_yxml, toks_sources) } def define_command(command: Command) { val (command_id, name, blobs_yxml, toks_yxml, toks_sources) = encode_command(command) protocol_command_args( "Document.define_command", command_id :: name :: blobs_yxml :: toks_yxml :: toks_sources) } def define_commands(commands: List[Command]) { protocol_command_args("Document.define_commands", commands.map(command => { import XML.Encode._ val (command_id, name, blobs_yxml, toks_yxml, toks_sources) = encode_command(command) val body = pair(string, pair(string, pair(string, pair(string, list(string)))))( command_id, (name, (blobs_yxml, (toks_yxml, toks_sources)))) YXML.string_of_body(body) })) } def define_commands_bulk(commands: List[Command]) { val (irregular, regular) = commands.partition(command => YXML.detect(command.source)) irregular.foreach(define_command) regular match { case Nil => case List(command) => define_command(command) case _ => define_commands(regular) } } /* execution */ def discontinue_execution(): Unit = protocol_command("Document.discontinue_execution") def cancel_exec(id: Document_ID.Exec): Unit = protocol_command("Document.cancel_exec", Document_ID(id)) /* document versions */ def update(old_id: Document_ID.Version, new_id: Document_ID.Version, edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name]) { val consolidate_yxml = { import XML.Encode._ Symbol.encode_yxml(list(string)(consolidate.map(_.node))) } val edits_yxml = { import XML.Encode._ def id: T[Command] = (cmd => long(cmd.id)) def encode_edit(name: Document.Node.Name) : T[Document.Node.Edit[Command.Edit, Command.Perspective]] = variant(List( { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, { case Document.Node.Deps(header) => val master_dir = File.standard_url(name.master_dir) val imports = header.imports.map(_.node) val keywords = header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) }) (Nil, pair(string, pair(string, pair(list(string), pair(list(pair(string, pair(pair(string, list(string)), list(string)))), list(string)))))( (master_dir, (name.theory, (imports, (keywords, header.errors)))))) }, { case Document.Node.Perspective(a, b, c) => (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)), list(pair(id, pair(string, list(string))))(c.dest)) })) edits.map({ case (name, edit) => Symbol.encode_yxml(pair(string, encode_edit(name))(name.node, edit)) }) } protocol_command_args("Document.update", Document_ID(old_id) :: Document_ID(new_id) :: consolidate_yxml :: edits_yxml) } def remove_versions(versions: List[Document.Version]) { val versions_yxml = { import XML.Encode._ Symbol.encode_yxml(list(long)(versions.map(_.id))) } protocol_command("Document.remove_versions", versions_yxml) } /* dialog via document content */ def dialog_result(serial: Long, result: String): Unit = protocol_command("Document.dialog_result", Value.Long(serial), result) }