diff --git a/src/Pure/General/bytes.ML b/src/Pure/General/bytes.ML --- a/src/Pure/General/bytes.ML +++ b/src/Pure/General/bytes.ML @@ -1,164 +1,211 @@ (* Title: Pure/General/bytes.ML Author: Makarius Scalable byte strings, with incremental construction (add content to the end). Note: type string is implicitly limited by String.maxSize (approx. 64 MB on 64_32 architecture). *) signature BYTES = sig val chunk_size: int type T val length: T -> int val contents: T -> string list val contents_blob: T -> XML.body val content: T -> string val is_empty: T -> bool val empty: T val build: (T -> T) -> T val add_substring: substring -> T -> T val add: string -> T -> T val beginning: int -> T -> string val exists_string: (string -> bool) -> T -> bool val forall_string: (string -> bool) -> T -> bool val last_string: T -> string option val trim_line: T -> T val append: T -> T -> T val string: string -> T val newline: T val buffer: Buffer.T -> T + val space_explode: string -> T -> string list + val split_lines: T -> string list + val trim_split_lines: T -> string list + val cat_lines: string list -> T val read_block: int -> BinIO.instream -> string val read_stream: int -> BinIO.instream -> T val write_stream: BinIO.outstream -> T -> unit val read: Path.T -> T val write: Path.T -> T -> unit end; structure Bytes: BYTES = struct (* primitive operations *) val chunk_size = 1024 * 1024; abstype T = Bytes of {buffer: string list, chunks: string list, m: int (*buffer size*), n: int (*chunks size*)} with fun length (Bytes {m, n, ...}) = m + n; val compact = implode o rev; fun contents (Bytes {buffer, chunks, ...}) = rev (chunks |> not (null buffer) ? cons (compact buffer)); val contents_blob = contents #> XML.blob; val content = implode o contents; fun is_empty bytes = length bytes = 0; val empty = Bytes {buffer = [], chunks = [], m = 0, n = 0}; fun build (f: T -> T) = f empty; fun add_substring s (bytes as Bytes {buffer, chunks, m, n}) = if Substring.isEmpty s then bytes else let val l = Substring.size s in if l + m < chunk_size then Bytes {buffer = Substring.string s :: buffer, chunks = chunks, m = l + m, n = n} else let val k = chunk_size - m; val chunk = compact (Substring.string (Substring.slice (s, 0, SOME k)) :: buffer); val s' = Substring.slice (s, k, SOME (l - k)); val bytes' = Bytes {buffer = [], chunks = chunk :: chunks, m = 0, n = chunk_size + n}; in add_substring s' bytes' end end; val add = add_substring o Substring.full; fun exists_string pred (Bytes {buffer, chunks, ...}) = let val ex = (exists o Library.exists_string) pred in ex buffer orelse ex chunks end; fun forall_string pred = not o exists_string (not o pred); fun last_string (Bytes {buffer, chunks, ...}) = (case buffer of s :: _ => Library.last_string s | [] => (case chunks of s :: _ => Library.last_string s | [] => NONE)); fun trim_line (bytes as Bytes {buffer, chunks, ...}) = let val is_line = (case last_string bytes of SOME s => Symbol.is_ascii_line_terminator s | NONE => false); in if is_line then let val (last_chunk, chunks') = (case chunks of [] => ("", []) | c :: cs => (c, cs)); val trimed = Library.trim_line (last_chunk ^ compact buffer); in build (fold_rev add chunks' #> add trimed) end else bytes end; end; (* derived operations *) fun beginning n bytes = let val dots = " ..."; val m = (String.maxSize - size dots) div chunk_size; val a = implode (take m (contents bytes)); val b = String.substring (a, 0, Int.min (n, size a)); in if size b < length bytes then b ^ dots else b end; fun append bytes1 bytes2 = (*left-associative*) if is_empty bytes1 then bytes2 else if is_empty bytes2 then bytes1 else bytes1 |> fold add (contents bytes2); val string = build o add; val newline = string "\n"; val buffer = build o fold add o Buffer.contents; + +(* space_explode *) + +fun space_explode sep bytes = + if is_empty bytes then [] + else if size sep <> 1 then [content bytes] + else + let + val sep_char = String.sub (sep, 0); + + fun add_part s part = + Buffer.add (Substring.string s) (the_default Buffer.empty part); + + fun explode head tail part res = + if Substring.isEmpty head then + (case tail of + [] => + (case part of + NONE => rev res + | SOME buf => rev (Buffer.content buf :: res)) + | chunk :: chunks => explode (Substring.full chunk) chunks part res) + else + (case Substring.fields (fn c => c = sep_char) head of + [a] => explode Substring.empty tail (SOME (add_part a part)) res + | a :: rest => + let + val (bs, c) = split_last rest; + val res' = res + |> cons (Buffer.content (add_part a part)) + |> fold (cons o Substring.string) bs; + val part' = SOME (add_part c NONE); + in explode Substring.empty tail part' res' end) + in explode Substring.empty (contents bytes) NONE [] end; + +val split_lines = space_explode "\n"; + +val trim_split_lines = trim_line #> split_lines #> map Library.trim_line; + +fun cat_lines lines = build (fold add (separate "\n" lines)); + + +(* IO *) + fun read_block limit = File.input_size (if limit < 0 then chunk_size else Int.min (chunk_size, limit)); fun read_stream limit stream = let fun read bytes = (case read_block (limit - length bytes) stream of "" => bytes | s => read (add s bytes)) in read empty end; fun write_stream stream = File.outputs stream o contents; val read = File.open_input (read_stream ~1); val write = File.open_output write_stream; (* ML pretty printing *) val _ = ML_system_pp (fn _ => fn _ => fn bytes => PolyML.PrettyString ("Bytes {length = " ^ string_of_int (length bytes) ^ "}")) end; diff --git a/src/Pure/General/bytes.scala b/src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala +++ b/src/Pure/General/bytes.scala @@ -1,235 +1,231 @@ /* Title: Pure/General/bytes.scala Author: Makarius Immutable byte vectors versus UTF8 strings. */ package isabelle import java.io.{File => JFile, ByteArrayOutputStream, ByteArrayInputStream, OutputStream, InputStream, FileInputStream, FileOutputStream} import java.net.URL import java.util.Base64 import org.tukaani.xz.{XZInputStream, XZOutputStream} object Bytes { val empty: Bytes = new Bytes(Array[Byte](), 0, 0) def apply(s: CharSequence): Bytes = { val str = s.toString if (str.isEmpty) empty else { val b = UTF8.bytes(str) new Bytes(b, 0, b.length) } } def apply(a: Array[Byte]): Bytes = apply(a, 0, a.length) def apply(a: Array[Byte], offset: Int, length: Int): Bytes = if (length == 0) empty else { val b = new Array[Byte](length) System.arraycopy(a, offset, b, 0, length) new Bytes(b, 0, b.length) } val newline: Bytes = apply("\n") /* base64 */ - def base64(s: String): Bytes = { + def decode_base64(s: String): Bytes = { val a = Base64.getDecoder.decode(s) new Bytes(a, 0, a.length) } - object Decode_Base64 extends Scala.Fun("decode_base64") { + object Decode_Base64 extends Scala.Fun_Bytes("decode_base64") { val here = Scala_Project.here - def invoke(args: List[Bytes]): List[Bytes] = - List(base64(Library.the_single(args).text)) + def apply(arg: Bytes): Bytes = decode_base64(arg.text) } - object Encode_Base64 extends Scala.Fun("encode_base64") { + object Encode_Base64 extends Scala.Fun_Bytes("encode_base64") { val here = Scala_Project.here - def invoke(args: List[Bytes]): List[Bytes] = - List(Bytes(Library.the_single(args).base64)) + def apply(arg: Bytes): Bytes = Bytes(arg.encode_base64) } /* XZ compression */ - object Compress extends Scala.Fun("compress") { + object Compress extends Scala.Fun_Bytes("compress") { val here = Scala_Project.here - def invoke(args: List[Bytes]): List[Bytes] = - List(Library.the_single(args).compress()) + def apply(arg: Bytes): Bytes = arg.compress() } - object Uncompress extends Scala.Fun("uncompress") { + object Uncompress extends Scala.Fun_Bytes("uncompress") { val here = Scala_Project.here - def invoke(args: List[Bytes]): List[Bytes] = - List(Library.the_single(args).uncompress()) + def apply(arg: Bytes): Bytes = arg.uncompress() } /* read */ def read_stream(stream: InputStream, limit: Int = Integer.MAX_VALUE, hint: Int = 1024): Bytes = if (limit == 0) empty else { val out_size = (if (limit == Integer.MAX_VALUE) hint else limit) max 1024 val out = new ByteArrayOutputStream(out_size) val buf = new Array[Byte](8192) var m = 0 var cont = true while (cont) { m = stream.read(buf, 0, buf.length min (limit - out.size)) if (m != -1) out.write(buf, 0, m) cont = (m != -1 && limit > out.size) } new Bytes(out.toByteArray, 0, out.size) } def read(file: JFile): Bytes = { val length = file.length val limit = if (length < 0 || length > Integer.MAX_VALUE) Integer.MAX_VALUE else length.toInt using(new FileInputStream(file))(read_stream(_, limit = limit)) } def read(path: Path): Bytes = read(path.file) def read(url: URL): Bytes = using(url.openStream)(read_stream(_)) /* write */ def write(file: JFile, bytes: Bytes): Unit = using(new FileOutputStream(file))(bytes.write_stream(_)) def write(path: Path, bytes: Bytes): Unit = write(path.file, bytes) } final class Bytes private( protected val bytes: Array[Byte], protected val offset: Int, val length: Int) extends CharSequence { /* equality */ override def equals(that: Any): Boolean = { that match { case other: Bytes => if (this eq other) true else if (length != other.length) false else (0 until length).forall(i => bytes(offset + i) == other.bytes(other.offset + i)) case _ => false } } private lazy val hash: Int = { var h = 0 for (i <- offset until offset + length) { val b = bytes(i).asInstanceOf[Int] & 0xFF h = 31 * h + b } h } override def hashCode(): Int = hash /* content */ lazy val sha1_digest: SHA1.Digest = SHA1.digest(bytes) def is_empty: Boolean = length == 0 def iterator: Iterator[Byte] = for (i <- (offset until (offset + length)).iterator) yield bytes(i) def array: Array[Byte] = { val a = new Array[Byte](length) System.arraycopy(bytes, offset, a, 0, length) a } def text: String = UTF8.decode_permissive(this) - def base64: String = { + def encode_base64: String = { val b = if (offset == 0 && length == bytes.length) bytes else Bytes(bytes, offset, length).bytes Base64.getEncoder.encodeToString(b) } - def maybe_base64: (Boolean, String) = { + def maybe_encode_base64: (Boolean, String) = { val s = text - if (this == Bytes(s)) (false, s) else (true, base64) + if (this == Bytes(s)) (false, s) else (true, encode_base64) } override def toString: String = "Bytes(" + length + ")" def proper: Option[Bytes] = if (is_empty) None else Some(this) def proper_text: Option[String] = if (is_empty) None else Some(text) def +(other: Bytes): Bytes = if (other.is_empty) this else if (is_empty) other else { val new_bytes = new Array[Byte](length + other.length) System.arraycopy(bytes, offset, new_bytes, 0, length) System.arraycopy(other.bytes, other.offset, new_bytes, length, other.length) new Bytes(new_bytes, 0, new_bytes.length) } /* CharSequence operations */ def charAt(i: Int): Char = if (0 <= i && i < length) (bytes(offset + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char] else throw new IndexOutOfBoundsException def subSequence(i: Int, j: Int): Bytes = { if (0 <= i && i <= j && j <= length) new Bytes(bytes, offset + i, j - i) else throw new IndexOutOfBoundsException } def trim_line: Bytes = if (length >= 2 && charAt(length - 2) == 13 && charAt(length - 1) == 10) subSequence(0, length - 2) else if (length >= 1 && (charAt(length - 1) == 13 || charAt(length - 1) == 10)) subSequence(0, length - 1) else this /* streams */ def stream(): ByteArrayInputStream = new ByteArrayInputStream(bytes, offset, length) def write_stream(stream: OutputStream): Unit = stream.write(bytes, offset, length) /* XZ data compression */ def uncompress(cache: XZ.Cache = XZ.Cache()): Bytes = using(new XZInputStream(stream(), cache))(Bytes.read_stream(_, hint = length)) def compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.Cache()): Bytes = { val result = new ByteArrayOutputStream(length) using(new XZOutputStream(result, options, cache))(write_stream(_)) new Bytes(result.toByteArray, 0, result.size) } def maybe_compress( options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.Cache() ) : (Boolean, Bytes) = { val compressed = compress(options = options, cache = cache) if (compressed.length < length) (true, compressed) else (false, this) } } diff --git a/src/Pure/General/file.ML b/src/Pure/General/file.ML --- a/src/Pure/General/file.ML +++ b/src/Pure/General/file.ML @@ -1,192 +1,186 @@ (* Title: Pure/General/file.ML Author: Makarius File-system operations. *) signature FILE = sig val standard_path: Path.T -> string val platform_path: Path.T -> string val bash_path: Path.T -> string val bash_paths: Path.T list -> string val bash_platform_path: Path.T -> string val absolute_path: Path.T -> Path.T val full_path: Path.T -> Path.T -> Path.T val tmp_path: Path.T -> Path.T val exists: Path.T -> bool val rm: Path.T -> unit val is_dir: Path.T -> bool val is_file: Path.T -> bool val check_dir: Path.T -> Path.T val check_file: Path.T -> Path.T val open_dir: (OS.FileSys.dirstream -> 'a) -> Path.T -> 'a val open_input: (BinIO.instream -> 'a) -> Path.T -> 'a val open_output: (BinIO.outstream -> 'a) -> Path.T -> 'a val open_append: (BinIO.outstream -> 'a) -> Path.T -> 'a val fold_dir: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a val read_dir: Path.T -> string list val input: BinIO.instream -> string val input_size: int -> BinIO.instream -> string val input_all: BinIO.instream -> string val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a - val fold_pages: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a val read_lines: Path.T -> string list - val read_pages: Path.T -> string list val read: Path.T -> string val write: Path.T -> string -> unit val append: Path.T -> string -> unit val generate: Path.T -> string -> unit val output: BinIO.outstream -> string -> unit val outputs: BinIO.outstream -> string list -> unit val write_list: Path.T -> string list -> unit val append_list: Path.T -> string list -> unit val write_buffer: Path.T -> Buffer.T -> unit val eq: Path.T * Path.T -> bool end; structure File: FILE = struct (* system path representations *) val standard_path = Path.implode o Path.expand; val platform_path = ML_System.platform_path o standard_path; val bash_path = Bash.string o standard_path; val bash_paths = Bash.strings o map standard_path; val bash_platform_path = Bash.string o platform_path; (* full_path *) val absolute_path = Path.expand #> (fn path => if Path.is_absolute path then path else Path.explode (ML_System.standard_path (OS.FileSys.getDir ())) + path); fun full_path dir path = let val path' = Path.expand path; val _ = Path.is_current path' andalso error "Bad file specification"; in absolute_path (dir + path') end; (* tmp_path *) fun tmp_path path = Path.variable "ISABELLE_TMP" + Path.base path; (* directory entries *) val exists = can OS.FileSys.modTime o platform_path; val rm = OS.FileSys.remove o platform_path; fun test_dir path = the_default false (try OS.FileSys.isDir (platform_path path)); fun is_dir path = exists path andalso test_dir path; fun is_file path = exists path andalso not (test_dir path); fun check_dir path = if is_dir path then path else error ("No such directory: " ^ Path.print (Path.expand path)); fun check_file path = if is_file path then path else error ("No such file: " ^ Path.print (Path.expand path)); (* open streams *) local fun with_file open_file close_file f = Thread_Attributes.uninterruptible (fn restore_attributes => fn path => let val file = open_file path; val result = Exn.capture (restore_attributes f) file; in close_file file; Exn.release result end); in fun open_dir f = with_file OS.FileSys.openDir OS.FileSys.closeDir f o platform_path; fun open_input f = with_file BinIO.openIn BinIO.closeIn f o platform_path; fun open_output f = with_file BinIO.openOut BinIO.closeOut f o platform_path; fun open_append f = with_file BinIO.openAppend BinIO.closeOut f o platform_path; end; (* directory content *) fun fold_dir f path a = check_dir path |> open_dir (fn stream => let fun read x = (case OS.FileSys.readDir stream of NONE => x | SOME entry => read (f entry x)); in read a end); fun read_dir path = sort_strings (fold_dir cons path []); (* input *) val input = Byte.bytesToString o BinIO.input; fun input_size n stream = Byte.bytesToString (BinIO.inputN (stream, n)); val input_all = Byte.bytesToString o BinIO.inputAll; (* scalable iterator: . avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine . optional terminator at end-of-input *) -fun fold_chunks terminator f path a = open_input (fn file => +fun fold_lines f path a = open_input (fn file => let fun read buf x = (case input file of "" => (case Buffer.content buf of "" => x | line => f line x) | input => - (case String.fields (fn c => c = terminator) input of + (case String.fields (fn c => c = #"\n") input of [rest] => read (Buffer.add rest buf) x - | line :: more => read_lines more (f (Buffer.content (Buffer.add line buf)) x))) - and read_lines [rest] x = read (Buffer.add rest Buffer.empty) x - | read_lines (line :: more) x = read_lines more (f line x); + | line :: more => read_more more (f (Buffer.content (Buffer.add line buf)) x))) + and read_more [rest] x = read (Buffer.add rest Buffer.empty) x + | read_more (line :: more) x = read_more more (f line x); in read Buffer.empty a end) path; -fun fold_lines f = fold_chunks #"\n" f; -fun fold_pages f = fold_chunks #"\f" f; - fun read_lines path = rev (fold_lines cons path []); -fun read_pages path = rev (fold_pages cons path []); val read = open_input input_all; (* output *) fun output file txt = BinIO.output (file, Byte.stringToBytes txt); val outputs = List.app o output; fun output_list txts file = List.app (output file) txts; fun write_list path txts = open_output (output_list txts) path; fun append_list path txts = open_append (output_list txts) path; fun write path txt = write_list path [txt]; fun append path txt = append_list path [txt]; fun generate path txt = if try read path = SOME txt then () else write path txt; fun write_buffer path buf = open_output (fn file => List.app (output file) (Buffer.contents buf)) path; (* eq *) fun eq paths = (case try (apply2 (OS.FileSys.fileId o platform_path)) paths of SOME ids => is_equal (OS.FileSys.compare ids) | NONE => false); end; diff --git a/src/Pure/ML/ml_init.ML b/src/Pure/ML/ml_init.ML --- a/src/Pure/ML/ml_init.ML +++ b/src/Pure/ML/ml_init.ML @@ -1,35 +1,41 @@ (* Title: Pure/ML/ml_init.ML Author: Makarius Initial ML environment. *) val seconds = Time.fromReal; val _ = List.app ML_Name_Space.forget_val ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"]; val ord = SML90.ord; val chr = SML90.chr; val raw_explode = SML90.explode; val implode = String.concat; val pointer_eq = PolyML.pointerEq; val error_depth = PolyML.error_depth; open Thread; datatype illegal = Interrupt; structure Basic_Exn: BASIC_EXN = Exn; open Basic_Exn; structure String = struct open String; fun substring (s, i, n) = if n = 1 then String.str (String.sub (s, i)) else String.substring (s, i, n); end; + +structure Substring = +struct + open Substring; + val empty = full ""; +end; 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,188 +1,186 @@ /* Title: Pure/ML/ml_process.scala Author: Makarius The raw ML process. */ package isabelle import java.util.{Map => JMap, HashMap} 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: JMap[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 eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()") 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 eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()") // session base + val (init_session_base, eval_init_session) = + session_base match { + case None => (sessions_structure.bootstrap, Nil) + case Some(base) => (base, List("Resources.init_session_env ()")) + } val init_session = Isabelle_System.tmp_file("init_session") Isabelle_System.chmod("600", File.path(init_session)) - val eval_init_session = - session_base match { - case None => Nil - case Some(base) => - File.write(init_session, new Resources(sessions_structure, base).init_session_yxml) - List("Resources.init_session_file (Path.explode " + - ML_Syntax.print_string_bytes(File.path(init_session).implode) + ")") - } + File.write(init_session, new Resources(sessions_structure, init_session_base).init_session_yxml) // 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 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_init_session).flatMap(List("--eval", _)) ::: use_prelude.flatMap(List("--use", _)) ::: List("--eval", eval_process) ::: args val bash_env = new HashMap(env) bash_env.put("ISABELLE_PROCESS_OPTIONS", File.standard_path(isabelle_process_options)) + bash_env.put("ISABELLE_INIT_SESSION", File.standard_path(init_session)) bash_env.put("ISABELLE_TMP", File.standard_path(isabelle_tmp)) bash_env.put("POLYSTATSDIR", isabelle_tmp.getAbsolutePath) - bash_env.put("ISABELLE_SCALA_FUNCTIONS", Scala.functions.mkString(",")) Bash.process( options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ + Bash.strings(bash_args), cwd = cwd, env = bash_env, redirect = redirect, cleanup = { () => isabelle_process_options.delete init_session.delete Isabelle_System.rm_tree(isabelle_tmp) cleanup() }) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", Scala_Project.here, { 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 base_info = Sessions.base_info(options, logic, dirs = dirs).check val store = Sessions.store(options) val result = ML_Process(options, base_info.sessions_structure, store, logic = logic, args = eval_args, modes = modes, session_base = Some(base_info.base)).result( progress_stdout = Output.writeln(_, stdout = true), progress_stderr = Output.writeln(_)) sys.exit(result.rc) }) } diff --git a/src/Pure/PIDE/resources.ML b/src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML +++ b/src/Pure/PIDE/resources.ML @@ -1,446 +1,444 @@ (* Title: Pure/PIDE/resources.ML Author: Makarius Resources for theories and auxiliary files. *) signature RESOURCES = sig val default_qualifier: string val init_session: {session_positions: (string * Properties.T) list, session_directories: (string * string) list, bibtex_entries: (string * string list) list, command_timings: Properties.T list, load_commands: (string * Position.T) list, - scala_functions: (string * (bool * Position.T)) list, + scala_functions: (string * ((bool * bool) * Position.T)) list, global_theories: (string * string) list, loaded_theories: string list} -> unit val init_session_yxml: string -> unit - val init_session_file: Path.T -> unit + val init_session_env: unit -> unit val finish_session_base: unit -> unit val global_theory: string -> string option val loaded_theory: string -> bool val check_session: Proof.context -> string * Position.T -> string val last_timing: Toplevel.transition -> Time.time val check_load_command: Proof.context -> string * Position.T -> string - val scala_functions: unit -> string list - val check_scala_function: Proof.context -> string * Position.T -> string * bool + val check_scala_function: Proof.context -> string * Position.T -> string * (bool * bool) val master_directory: theory -> Path.T val imports_of: theory -> (string * Position.T) list val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory val thy_path: Path.T -> Path.T val theory_qualifier: string -> string val theory_bibtex_entries: string -> string list val find_theory_file: string -> Path.T option val import_name: string -> Path.T -> string -> {node_name: Path.T, master_dir: Path.T, theory_name: string} val check_thy: Path.T -> string -> {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T, imports: (string * Position.T) list, keywords: Thy_Header.keywords} val parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list) parser val parse_file: (theory -> Token.file) parser val provide: Path.T * SHA1.digest -> theory -> theory val provide_file: Token.file -> theory -> theory val provide_parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list * theory) parser val provide_parse_file: (theory -> Token.file * theory) parser val loaded_files_current: theory -> bool val check_path: Proof.context -> Path.T option -> Input.source -> Path.T val check_file: Proof.context -> Path.T option -> Input.source -> Path.T val check_dir: Proof.context -> Path.T option -> Input.source -> Path.T val check_session_dir: Proof.context -> Path.T option -> Input.source -> Path.T end; structure Resources: RESOURCES = struct (* command timings *) type timings = ((string * Time.time) Inttab.table) Symtab.table; (*file -> offset -> name, time*) val empty_timings: timings = Symtab.empty; fun update_timings props = (case Markup.parse_command_timing_properties props of SOME ({file, offset, name}, time) => Symtab.map_default (file, Inttab.empty) (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time))) | NONE => I); fun make_timings command_timings = fold update_timings command_timings empty_timings; fun approximative_id name pos = (case (Position.file_of pos, Position.offset_of pos) of (SOME file, SOME offset) => if name = "" then NONE else SOME {file = file, offset = offset, name = name} | _ => NONE); fun get_timings timings tr = (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of SOME {file, offset, name} => (case Symtab.lookup timings file of SOME offsets => (case Inttab.lookup offsets offset of SOME (name', time) => if name = name' then SOME time else NONE | NONE => NONE) | NONE => NONE) | NONE => NONE) |> the_default Time.zeroTime; (* session base *) val default_qualifier = "Draft"; type entry = {pos: Position.T, serial: serial}; fun make_entry props : entry = {pos = Position.of_properties props, serial = serial ()}; val empty_session_base = ({session_positions = []: (string * entry) list, session_directories = Symtab.empty: Path.T list Symtab.table, bibtex_entries = Symtab.empty: string list Symtab.table, timings = empty_timings, load_commands = []: (string * Position.T) list, - scala_functions = Symtab.empty: (bool * Position.T) Symtab.table}, + scala_functions = Symtab.empty: ((bool * bool) * Position.T) Symtab.table}, {global_theories = Symtab.empty: string Symtab.table, loaded_theories = Symtab.empty: unit Symtab.table}); val global_session_base = Synchronized.var "Sessions.base" empty_session_base; fun init_session {session_positions, session_directories, bibtex_entries, command_timings, load_commands, scala_functions, global_theories, loaded_theories} = Synchronized.change global_session_base (fn _ => ({session_positions = sort_by #1 (map (apsnd make_entry) session_positions), session_directories = Symtab.build (session_directories |> fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir))), bibtex_entries = Symtab.make bibtex_entries, timings = make_timings command_timings, load_commands = load_commands, scala_functions = Symtab.make scala_functions}, {global_theories = Symtab.make global_theories, loaded_theories = Symtab.make_set loaded_theories})); fun init_session_yxml yxml = let val (session_positions, (session_directories, (bibtex_entries, (command_timings, (load_commands, (scala_functions, (global_theories, loaded_theories))))))) = YXML.parse_body yxml |> let open XML.Decode in (pair (list (pair string properties)) (pair (list (pair string string)) (pair (list (pair string (list string))) (pair (list properties) (pair (list (pair string properties)) - (pair (list (pair string (pair bool properties))) + (pair (list (pair string (pair (pair bool bool) properties))) (pair (list (pair string string)) (list string)))))))) end; in init_session {session_positions = session_positions, session_directories = session_directories, bibtex_entries = bibtex_entries, command_timings = command_timings, load_commands = (map o apsnd) Position.of_properties load_commands, scala_functions = (map o apsnd o apsnd) Position.of_properties scala_functions, global_theories = global_theories, loaded_theories = loaded_theories} end; -fun init_session_file path = - init_session_yxml (File.read path) before File.rm path; +fun init_session_env () = + (case getenv "ISABELLE_INIT_SESSION" of + "" => () + | name => + try File.read (Path.explode name) + |> Option.app init_session_yxml); + +val _ = init_session_env (); fun finish_session_base () = Synchronized.change global_session_base (apfst (K (#1 empty_session_base))); fun get_session_base f = f (Synchronized.value global_session_base); fun get_session_base1 f = get_session_base (f o #1); fun get_session_base2 f = get_session_base (f o #2); fun global_theory a = Symtab.lookup (get_session_base2 #global_theories) a; fun loaded_theory a = Symtab.defined (get_session_base2 #loaded_theories) a; fun check_session ctxt arg = Completion.check_item "session" (fn (name, {pos, serial}) => Position.make_entity_markup {def = false} serial Markup.sessionN (name, pos)) (get_session_base1 #session_positions) ctxt arg; fun last_timing tr = get_timings (get_session_base1 #timings) tr; fun check_load_command ctxt arg = Completion.check_entity Markup.load_commandN (get_session_base1 #load_commands) ctxt arg; (* Scala functions *) -(*raw bootstrap environment*) -fun scala_functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS"); - -(*regular resources*) -fun scala_function a = - (a, the_default (false, Position.none) (Symtab.lookup (get_session_base1 #scala_functions) a)); - fun check_scala_function ctxt arg = let - val funs = scala_functions () |> sort_strings |> map scala_function; - val name = Completion.check_entity Markup.scala_functionN (map (apsnd #2) funs) ctxt arg; - val multi = - (case AList.lookup (op =) funs name of - SOME (multi, _) => multi - | NONE => false); - in (name, multi) end; + val table = get_session_base1 #scala_functions; + val funs = Symtab.fold (fn (a, (_, pos)) => cons (a, pos)) table [] |> sort_by #1; + val name = Completion.check_entity Markup.scala_functionN funs ctxt arg; + val flags = #1 (the (Symtab.lookup table name)); + in (name, flags) end; val _ = Theory.setup (Document_Output.antiquotation_verbatim_embedded \<^binding>\scala_function\ (Scan.lift Parse.embedded_position) (#1 oo check_scala_function) #> ML_Antiquotation.inline_embedded \<^binding>\scala_function\ (Args.context -- Scan.lift Parse.embedded_position >> (uncurry check_scala_function #> #1 #> ML_Syntax.print_string)) #> ML_Antiquotation.value_embedded \<^binding>\scala\ (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, arg) => let - val (name, multi) = check_scala_function ctxt arg; - val func = if multi then "Scala.function" else "Scala.function1"; + val (name, (single, bytes)) = check_scala_function ctxt arg; + val func = + (if single then "Scala.function1" else "Scala.function") ^ + (if bytes then "_bytes" else ""); in ML_Syntax.atomic (func ^ " " ^ ML_Syntax.print_string name) end))); (* manage source files *) type files = {master_dir: Path.T, (*master directory of theory source*) imports: (string * Position.T) list, (*source specification of imports*) provided: (Path.T * SHA1.digest) list}; (*source path, digest*) fun make_files (master_dir, imports, provided): files = {master_dir = master_dir, imports = imports, provided = provided}; structure Files = Theory_Data ( type T = files; val empty = make_files (Path.current, [], []); fun merge ({master_dir, imports, provided = provided1}, {provided = provided2, ...}) = let val provided' = Library.merge (op =) (provided1, provided2) in make_files (master_dir, imports, provided') end ); fun map_files f = Files.map (fn {master_dir, imports, provided} => make_files (f (master_dir, imports, provided))); val master_directory = #master_dir o Files.get; val imports_of = #imports o Files.get; fun begin_theory master_dir {name, imports, keywords} parents = let val thy = Theory.begin_theory name parents |> map_files (fn _ => (Path.explode (Path.implode_symbolic master_dir), imports, [])) |> Thy_Header.add_keywords keywords; val ctxt = Proof_Context.init_global thy; val _ = List.app (ignore o check_load_command ctxt o #load_command o #2) keywords; in thy end; (* theory files *) val thy_path = Path.ext "thy"; fun theory_qualifier theory = (case global_theory theory of SOME qualifier => qualifier | NONE => Long_Name.qualifier theory); fun theory_name qualifier theory = if Long_Name.is_qualified theory orelse is_some (global_theory theory) then theory else Long_Name.qualify qualifier theory; fun theory_bibtex_entries theory = Symtab.lookup_list (get_session_base1 #bibtex_entries) (theory_qualifier theory); fun find_theory_file thy_name = let val thy_file = thy_path (Path.basic (Long_Name.base_name thy_name)); val session = theory_qualifier thy_name; val dirs = Symtab.lookup_list (get_session_base1 #session_directories) session; in dirs |> get_first (fn dir => let val path = dir + thy_file in if File.is_file path then SOME path else NONE end) end; fun make_theory_node node_name theory = {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory}; fun loaded_theory_node theory = {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}; fun import_name qualifier dir s = let val theory = theory_name qualifier (Thy_Header.import_name s); fun theory_node () = make_theory_node (File.full_path dir (thy_path (Path.expand (Path.explode s)))) theory; in if not (Thy_Header.is_base_name s) then theory_node () else if loaded_theory theory then loaded_theory_node theory else (case find_theory_file theory of SOME node_name => make_theory_node node_name theory | NONE => if Long_Name.is_qualified s then loaded_theory_node theory else theory_node ()) end; fun check_file dir file = File.check_file (File.full_path dir file); fun check_thy dir thy_name = let val thy_base_name = Long_Name.base_name thy_name; val master_file = (case find_theory_file thy_name of SOME path => check_file Path.current path | NONE => check_file dir (thy_path (Path.basic thy_base_name))); val text = File.read master_file; val {name = (name, pos), imports, keywords} = Thy_Header.read (Path.position master_file) text; val _ = thy_base_name <> name andalso error ("Bad theory name " ^ quote name ^ " for file " ^ Path.print (Path.base master_file) ^ Position.here pos); in {master = (master_file, SHA1.digest text), text = text, theory_pos = pos, imports = imports, keywords = keywords} end; (* load files *) fun parse_files make_paths = Scan.ahead Parse.not_eof -- Parse.path_input >> (fn (tok, source) => fn thy => (case Token.get_files tok of [] => let val master_dir = master_directory thy; val name = Input.string_of source; val pos = Input.pos_of source; val delimited = Input.is_delimited source; val src_paths = make_paths (Path.explode name); in map (Command.read_file master_dir pos delimited) src_paths end | files => map Exn.release files)); val parse_file = parse_files single >> (fn f => f #> the_single); fun provide (src_path, id) = map_files (fn (master_dir, imports, provided) => if AList.defined (op =) provided src_path then error ("Duplicate use of source file: " ^ Path.print src_path) else (master_dir, imports, (src_path, id) :: provided)); fun provide_file (file: Token.file) = provide (#src_path file, #digest file); fun provide_parse_files make_paths = parse_files make_paths >> (fn files => fn thy => let val fs = files thy; val thy' = fold (fn {src_path, digest, ...} => provide (src_path, digest)) fs thy; in (fs, thy') end); val provide_parse_file = provide_parse_files single >> (fn f => f #>> the_single); fun load_file thy src_path = let val full_path = check_file (master_directory thy) src_path; val text = File.read full_path; val id = SHA1.digest text; in ((full_path, id), text) end; fun loaded_files_current thy = #provided (Files.get thy) |> forall (fn (src_path, id) => (case try (load_file thy) src_path of NONE => false | SOME ((_, id'), _) => id = id')); (* formal check *) fun formal_check check_file ctxt opt_dir source = let val name = Input.string_of source; val pos = Input.pos_of source; val delimited = Input.is_delimited source; val _ = Context_Position.report ctxt pos (Markup.language_path delimited); fun err msg = error (msg ^ Position.here pos); val dir = (case opt_dir of SOME dir => dir | NONE => master_directory (Proof_Context.theory_of ctxt)); val path = dir + Path.explode name handle ERROR msg => err msg; val _ = Path.expand path handle ERROR msg => err msg; val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path)); val _ : Path.T = check_file path handle ERROR msg => err msg; in path end; val check_path = formal_check I; val check_file = formal_check File.check_file; val check_dir = formal_check File.check_dir; fun check_session_dir ctxt opt_dir s = let val dir = Path.expand (check_dir ctxt opt_dir s); val ok = File.is_file (dir + Path.explode("ROOT")) orelse File.is_file (dir + Path.explode("ROOTS")); in if ok then dir else error ("Bad session root directory (missing ROOT or ROOTS): " ^ Path.print dir ^ Position.here (Input.pos_of s)) end; (* antiquotations *) local fun document_antiq (check: Proof.context -> Path.T option -> Input.source -> Path.T) = Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) => (check ctxt NONE source; Latex.string (Latex.output_ascii_breakable "/" (Input.string_of source)) |> Latex.macro "isatt")); fun ML_antiq check = Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) => check ctxt (SOME Path.current) source |> ML_Syntax.print_path); in val _ = Theory.setup (Document_Output.antiquotation_verbatim_embedded \<^binding>\session\ (Scan.lift Parse.embedded_position) check_session #> Document_Output.antiquotation_raw_embedded \<^binding>\path\ (document_antiq check_path) (K I) #> Document_Output.antiquotation_raw_embedded \<^binding>\file\ (document_antiq check_file) (K I) #> Document_Output.antiquotation_raw_embedded \<^binding>\dir\ (document_antiq check_dir) (K I) #> ML_Antiquotation.value_embedded \<^binding>\path\ (ML_antiq check_path) #> ML_Antiquotation.value_embedded \<^binding>\file\ (ML_antiq check_file) #> ML_Antiquotation.value_embedded \<^binding>\dir\ (ML_antiq check_dir) #> ML_Antiquotation.value_embedded \<^binding>\path_binding\ (Scan.lift (Parse.position Parse.path) >> (ML_Syntax.print_path_binding o Path.explode_binding)) #> ML_Antiquotation.value \<^binding>\master_dir\ (Args.theory >> (ML_Syntax.print_path o master_directory))); end; end; diff --git a/src/Pure/PIDE/resources.scala b/src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala +++ b/src/Pure/PIDE/resources.scala @@ -1,447 +1,447 @@ /* Title: Pure/PIDE/resources.scala Author: Makarius Resources for theories and auxiliary files. */ package isabelle import scala.util.parsing.input.Reader import java.io.{File => JFile} object Resources { def empty: Resources = new Resources(Sessions.Structure.empty, Sessions.Structure.empty.bootstrap) def file_node(file: Path, dir: String = "", theory: String = ""): Document.Node.Name = empty.file_node(file, dir = dir, theory = theory) def hidden_node(name: Document.Node.Name): Boolean = !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name) def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] = File_Format.registry.get(snapshot.node_name).flatMap(_.html_document(snapshot)) } class Resources( val sessions_structure: Sessions.Structure, val session_base: Sessions.Base, val log: Logger = No_Logger, command_timings: List[Properties.T] = Nil ) { resources => /* init session */ def init_session_yxml: String = { import XML.Encode._ YXML.string_of_body( pair(list(pair(string, properties)), pair(list(pair(string, string)), pair(list(pair(string, list(string))), pair(list(properties), pair(list(pair(string, properties)), - pair(list(pair(string, pair(bool, properties))), + pair(list(Scala.encode_fun), pair(list(pair(string, string)), list(string))))))))( (sessions_structure.session_positions, (sessions_structure.dest_session_directories, (sessions_structure.bibtex_entries, (command_timings, (Command_Span.load_commands.map(cmd => (cmd.name, cmd.position)), - (Scala.functions.map(fun => (fun.name, (fun.multi, fun.position))), + (Scala.functions, (session_base.global_theories.toList, session_base.loaded_theories.keys))))))))) } /* file formats */ def make_theory_name(name: Document.Node.Name): Option[Document.Node.Name] = File_Format.registry.get(name).flatMap(_.make_theory_name(resources, name)) def make_theory_content(thy_name: Document.Node.Name): Option[String] = File_Format.registry.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name)) /* file-system operations */ def append(dir: String, source_path: Path): String = (Path.explode(dir) + source_path).expand.implode def append(node_name: Document.Node.Name, source_path: Path): String = append(node_name.master_dir, source_path) def file_node(file: Path, dir: String = "", theory: String = ""): Document.Node.Name = { val node = append(dir, file) val master_dir = append(dir, file.dir) Document.Node.Name(node, master_dir, theory) } def loaded_theory_node(theory: String): Document.Node.Name = Document.Node.Name(theory, "", theory) /* source files of Isabelle/ML bootstrap */ def source_file(raw_name: String): Option[String] = { if (Path.is_wellformed(raw_name)) { if (Path.is_valid(raw_name)) { def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None val path = Path.explode(raw_name) val path1 = if (path.is_absolute || path.is_current) check(path) else { check(Path.explode("~~/src/Pure") + path) orElse (if (Isabelle_System.getenv("ML_SOURCES") == "") None else check(Path.explode("$ML_SOURCES") + path)) } Some(File.platform_path(path1 getOrElse path)) } else None } else Some(raw_name) } /* theory files */ def load_commands( syntax: Outer_Syntax, name: Document.Node.Name ) : () => List[Command_Span.Span] = { val (is_utf8, raw_text) = with_thy_reader(name, reader => (Scan.reader_is_utf8(reader), reader.source.toString)) () => { if (syntax.has_load_commands(raw_text)) { val text = Symbol.decode(Scan.reader_decode_utf8(is_utf8, raw_text)) syntax.parse_spans(text).filter(_.is_load_command(syntax)) } else Nil } } def loaded_files( syntax: Outer_Syntax, name: Document.Node.Name, spans: List[Command_Span.Span] ) : List[Path] = { val dir = name.master_dir_path for { span <- spans; file <- span.loaded_files(syntax).files } yield (dir + Path.explode(file)).expand } def pure_files(syntax: Outer_Syntax): List[Path] = { val pure_dir = Path.explode("~~/src/Pure") for { (name, theory) <- Thy_Header.ml_roots path = (pure_dir + Path.explode(name)).expand node_name = Document.Node.Name(path.implode, path.dir.implode, theory) file <- loaded_files(syntax, node_name, load_commands(syntax, node_name)()) } yield file } def theory_name(qualifier: String, theory: String): String = if (Long_Name.is_qualified(theory) || session_base.global_theories.isDefinedAt(theory)) theory else Long_Name.qualify(qualifier, theory) def find_theory_node(theory: String): Option[Document.Node.Name] = { val thy_file = Path.basic(Long_Name.base_name(theory)).thy val session = session_base.theory_qualifier(theory) val dirs = sessions_structure.get(session) match { case Some(info) => info.dirs case None => Nil } dirs.collectFirst({ case dir if (dir + thy_file).is_file => file_node(dir + thy_file, theory = theory) }) } def import_name(qualifier: String, dir: String, s: String): Document.Node.Name = { val theory = theory_name(qualifier, Thy_Header.import_name(s)) def theory_node = file_node(Path.explode(s).thy, dir = dir, theory = theory) if (!Thy_Header.is_base_name(s)) theory_node else if (session_base.loaded_theory(theory)) loaded_theory_node(theory) else { find_theory_node(theory) match { case Some(node_name) => node_name case None => if (Long_Name.is_qualified(s)) loaded_theory_node(theory) else theory_node } } } def import_name(name: Document.Node.Name, s: String): Document.Node.Name = import_name(session_base.theory_qualifier(name), name.master_dir, s) def import_name(info: Sessions.Info, s: String): Document.Node.Name = import_name(info.name, info.dir.implode, s) def find_theory(file: JFile): Option[Document.Node.Name] = { for { qualifier <- session_base.session_directories.get(File.canonical(file).getParentFile) theory_base <- proper_string(Thy_Header.theory_name(file.getName)) theory = theory_name(qualifier, theory_base) theory_node <- find_theory_node(theory) if File.eq(theory_node.path.file, file) } yield theory_node } def complete_import_name(context_name: Document.Node.Name, s: String): List[String] = { val context_session = session_base.theory_qualifier(context_name) val context_dir = try { Some(context_name.master_dir_path) } catch { case ERROR(_) => None } (for { (session, (info, _)) <- sessions_structure.imports_graph.iterator dir <- (if (session == context_session) context_dir.toList else info.dirs).iterator theory <- Thy_Header.try_read_dir(dir).iterator if Completion.completed(s)(theory) } yield { if (session == context_session || session_base.global_theories.isDefinedAt(theory)) theory else Long_Name.qualify(session, theory) }).toList.sorted } def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = { val path = name.path if (path.is_file) using(Scan.byte_reader(path.file))(f) else if (name.node == name.theory) error("Cannot load theory " + quote(name.theory)) else error ("Cannot load theory file " + path) } def check_thy( node_name: Document.Node.Name, reader: Reader[Char], command: Boolean = true, strict: Boolean = true ): Document.Node.Header = { if (node_name.is_theory && reader.source.length > 0) { try { val header = Thy_Header.read(node_name, reader, command = command, strict = strict) val imports = header.imports.map({ case (s, pos) => val name = import_name(node_name, s) if (Sessions.exclude_theory(name.theory_base_name)) error("Bad theory name " + quote(name.theory_base_name) + Position.here(pos)) (name, pos) }) Document.Node.Header(imports, header.keywords, header.abbrevs) } catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } } else Document.Node.no_header } /* special header */ def special_header(name: Document.Node.Name): Option[Document.Node.Header] = { val imports = if (name.theory == Sessions.root_name) List(import_name(name, Sessions.theory_import)) else if (Thy_Header.is_ml_root(name.theory)) List(import_name(name, Thy_Header.ML_BOOTSTRAP)) else if (Thy_Header.is_bootstrap(name.theory)) List(import_name(name, Thy_Header.PURE)) else Nil if (imports.isEmpty) None else Some(Document.Node.Header(imports.map((_, Position.none)))) } /* blobs */ def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] = (for { (node_name, node) <- nodes.iterator if !session_base.loaded_theory(node_name) cmd <- node.load_commands.iterator name <- cmd.blobs_undefined.iterator } yield name).toList /* document changes */ def parse_change( reparse_limit: Int, previous: Document.Version, doc_blobs: Document.Blobs, edits: List[Document.Edit_Text], consolidate: List[Document.Node.Name]): Session.Change = Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate) def commit(change: Session.Change): Unit = {} /* theory and file dependencies */ def dependencies( thys: List[(Document.Node.Name, Position.T)], progress: Progress = new Progress): Dependencies[Unit] = Dependencies.empty[Unit].require_thys((), thys, progress = progress) def session_dependencies( info: Sessions.Info, progress: Progress = new Progress ) : Dependencies[Options] = { info.theories.foldLeft(Dependencies.empty[Options]) { case (dependencies, (options, thys)) => dependencies.require_thys(options, for { (thy, pos) <- thys } yield (import_name(info, thy), pos), progress = progress) } } object Dependencies { def empty[A]: Dependencies[A] = new Dependencies[A](Nil, Map.empty) private def show_path(names: List[Document.Node.Name]): String = names.map(name => quote(name.theory)).mkString(" via ") private def cycle_msg(names: List[Document.Node.Name]): String = "Cyclic dependency of " + show_path(names) private def required_by(initiators: List[Document.Node.Name]): String = if (initiators.isEmpty) "" else "\n(required by " + show_path(initiators.reverse) + ")" } final class Dependencies[A] private( rev_entries: List[Document.Node.Entry], seen: Map[Document.Node.Name, A] ) { private def cons(entry: Document.Node.Entry): Dependencies[A] = new Dependencies[A](entry :: rev_entries, seen) def require_thy(adjunct: A, thy: (Document.Node.Name, Position.T), initiators: List[Document.Node.Name] = Nil, progress: Progress = new Progress): Dependencies[A] = { val (name, pos) = thy def message: String = "The error(s) above occurred for theory " + quote(name.theory) + Dependencies.required_by(initiators) + Position.here(pos) if (seen.isDefinedAt(name)) this else { val dependencies1 = new Dependencies[A](rev_entries, seen + (name -> adjunct)) if (session_base.loaded_theory(name)) dependencies1 else { try { if (initiators.contains(name)) error(Dependencies.cycle_msg(initiators)) progress.expose_interrupt() val header = try { with_thy_reader(name, check_thy(name, _, command = false)).cat_errors(message) } catch { case ERROR(msg) => cat_error(msg, message) } val entry = Document.Node.Entry(name, header) dependencies1.require_thys(adjunct, header.imports_pos, initiators = name :: initiators, progress = progress).cons(entry) } catch { case e: Throwable => dependencies1.cons(Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e)))) } } } } def require_thys(adjunct: A, thys: List[(Document.Node.Name, Position.T)], progress: Progress = new Progress, initiators: List[Document.Node.Name] = Nil): Dependencies[A] = thys.foldLeft(this)(_.require_thy(adjunct, _, progress = progress, initiators = initiators)) def entries: List[Document.Node.Entry] = rev_entries.reverse def theories: List[Document.Node.Name] = entries.map(_.name) def theories_adjunct: List[(Document.Node.Name, A)] = theories.map(name => (name, seen(name))) def errors: List[String] = entries.flatMap(_.header.errors) def check_errors: Dependencies[A] = errors match { case Nil => this case errs => error(cat_lines(errs)) } lazy val theory_graph: Document.Node.Name.Graph[Unit] = { val regular = theories.toSet val irregular = (for { entry <- entries.iterator imp <- entry.header.imports if !regular(imp) } yield imp).toSet Document.Node.Name.make_graph( irregular.toList.map(name => ((name, ()), Nil)) ::: entries.map(entry => ((entry.name, ()), entry.header.imports))) } lazy val loaded_theories: Graph[String, Outer_Syntax] = entries.foldLeft(session_base.loaded_theories) { case (graph, entry) => val name = entry.name.theory val imports = entry.header.imports.map(_.theory) val graph1 = (name :: imports).foldLeft(graph)(_.default_node(_, Outer_Syntax.empty)) val graph2 = imports.foldLeft(graph1)(_.add_edge(_, name)) val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node) val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header graph2.map_node(name, _ => syntax) } def get_syntax(name: Document.Node.Name): Outer_Syntax = loaded_theories.get_node(name.theory) def load_commands: List[(Document.Node.Name, List[Command_Span.Span])] = theories.zip( Par_List.map((e: () => List[Command_Span.Span]) => e(), theories.map(name => resources.load_commands(get_syntax(name), name)))) .filter(p => p._2.nonEmpty) def loaded_files( name: Document.Node.Name, spans: List[Command_Span.Span] ) : (String, List[Path]) = { val theory = name.theory val syntax = get_syntax(name) val files1 = resources.loaded_files(syntax, name, spans) val files2 = if (theory == Thy_Header.PURE) pure_files(syntax) else Nil (theory, files1 ::: files2) } def loaded_files: List[Path] = for { (name, spans) <- load_commands file <- loaded_files(name, spans)._2 } yield file def imported_files: List[Path] = { val base_theories = loaded_theories.all_preds(theories.map(_.theory)). filter(session_base.loaded_theories.defined) base_theories.map(theory => session_base.known_theories(theory).name.path) ::: base_theories.flatMap(session_base.known_loaded_files.withDefaultValue(Nil)) } lazy val overall_syntax: Outer_Syntax = Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node)) override def toString: String = entries.toString } } diff --git a/src/Pure/System/options.ML b/src/Pure/System/options.ML --- a/src/Pure/System/options.ML +++ b/src/Pure/System/options.ML @@ -1,223 +1,220 @@ (* Title: Pure/System/options.ML Author: Makarius System options with external string representation. *) signature OPTIONS = sig val boolT: string val intT: string val realT: string val stringT: string val unknownT: string type T val empty: T val dest: T -> (string * Position.T) list val typ: T -> string -> string val bool: T -> string -> bool val int: T -> string -> int val real: T -> string -> real val seconds: T -> string -> Time.time val string: T -> string -> string val put_bool: string -> bool -> T -> T val put_int: string -> int -> T -> T val put_real: string -> real -> T -> T val put_string: string -> string -> T -> T val declare: {pos: Position.T, name: string, typ: string, value: string} -> T -> T val update: string -> string -> T -> T val encode: T XML.Encode.T val decode: T XML.Decode.T val default: unit -> T val default_typ: string -> string val default_bool: string -> bool val default_int: string -> int val default_real: string -> real val default_seconds: string -> Time.time val default_string: string -> string val default_put_bool: string -> bool -> unit val default_put_int: string -> int -> unit val default_put_real: string -> real -> unit val default_put_string: string -> string -> unit val get_default: string -> string val put_default: string -> string -> unit val set_default: T -> unit val reset_default: unit -> unit val load_default: unit -> unit end; structure Options: OPTIONS = struct (* representation *) val boolT = "bool"; val intT = "int"; val realT = "real"; val stringT = "string"; val unknownT = "unknown"; datatype T = Options of {pos: Position.T, typ: string, value: string} Symtab.table; val empty = Options Symtab.empty; fun dest (Options tab) = Symtab.fold (fn (name, {pos, ...}) => cons (name, pos)) tab [] |> sort_by #1; (* check *) fun check_name (Options tab) name = let val opt = Symtab.lookup tab name in if is_some opt andalso #typ (the opt) <> unknownT then the opt else error ("Unknown system option " ^ quote name) end; fun check_type options name typ = let val opt = check_name options name in if #typ opt = typ then opt else error ("Ill-typed system option " ^ quote name ^ " : " ^ #typ opt ^ " vs. " ^ typ) end; (* typ *) fun typ options name = #typ (check_name options name); (* basic operations *) fun put T print name x (options as Options tab) = let val opt = check_type options name T in Options (Symtab.update (name, {pos = #pos opt, typ = #typ opt, value = print x}) tab) end; fun get T parse options name = let val opt = check_type options name T in (case parse (#value opt) of SOME x => x | NONE => error ("Malformed value for system option " ^ quote name ^ " : " ^ T ^ " =\n" ^ quote (#value opt))) end; (* internal lookup and update *) val bool = get boolT (try Value.parse_bool); val int = get intT (try Value.parse_int); val real = get realT (try Value.parse_real); val seconds = Time.fromReal oo real; val string = get stringT SOME; val put_bool = put boolT Value.print_bool; val put_int = put intT Value.print_int; val put_real = put realT Value.print_real; val put_string = put stringT I; (* external updates *) fun check_value options name = let val opt = check_name options name in if #typ opt = boolT then ignore (bool options name) else if #typ opt = intT then ignore (int options name) else if #typ opt = realT then ignore (real options name) else if #typ opt = stringT then ignore (string options name) else () end; fun declare {pos, name, typ, value} (Options tab) = let val options' = (case Symtab.lookup tab name of SOME other => error ("Duplicate declaration of system option " ^ quote name ^ Position.here pos ^ Position.here (#pos other)) | NONE => Options (Symtab.update (name, {pos = pos, typ = typ, value = value}) tab)); val _ = typ = boolT orelse typ = intT orelse typ = realT orelse typ = stringT orelse error ("Unknown type for system option " ^ quote name ^ " : " ^ quote typ ^ Position.here pos); val _ = check_value options' name; in options' end; fun update name value (options as Options tab) = let val opt = check_name options name; val options' = Options (Symtab.update (name, {pos = #pos opt, typ = #typ opt, value = value}) tab); val _ = check_value options' name; in options' end; (* XML data *) fun encode (Options tab) = let val opts = build (tab |> Symtab.fold (fn (name, {pos, typ, value}) => cons (Position.properties_of pos, (name, (typ, value))))); open XML.Encode; in list (pair properties (pair string (pair string string))) opts end; fun decode body = let open XML.Decode; val decode_options = list (pair properties (pair string (pair string string))) #> map (fn (props, (name, (typ, value))) => {pos = Position.of_properties props, name = name, typ = typ, value = value}); in fold declare (decode_options body) empty end; (** global default **) val global_default = Synchronized.var "Options.default" (NONE: T option); fun err_no_default () = error "Missing default for system options within Isabelle process"; fun change_default f x y = Synchronized.change global_default (fn SOME options => SOME (f x y options) | NONE => err_no_default ()); fun default () = (case Synchronized.value global_default of SOME options => options | NONE => err_no_default ()); fun default_typ name = typ (default ()) name; fun default_bool name = bool (default ()) name; fun default_int name = int (default ()) name; fun default_real name = real (default ()) name; fun default_seconds name = seconds (default ()) name; fun default_string name = string (default ()) name; val default_put_bool = change_default put_bool; val default_put_int = change_default put_int; val default_put_real = change_default put_real; val default_put_string = change_default put_string; fun get_default name = let val options = default () in get (typ options name) SOME options name end; val put_default = change_default update; fun set_default options = Synchronized.change global_default (K (SOME options)); fun reset_default () = Synchronized.change global_default (K NONE); fun load_default () = (case getenv "ISABELLE_PROCESS_OPTIONS" of "" => () | name => - let val path = Path.explode name in - (case try File.read path of - SOME s => set_default (decode (YXML.parse_body s)) - | NONE => ()) - end); + try File.read (Path.explode name) + |> Option.app (set_default o decode o YXML.parse_body)); val _ = load_default (); val _ = ML_Print_Depth.set_print_depth (default_int "ML_print_depth"); end; diff --git a/src/Pure/System/scala.scala b/src/Pure/System/scala.scala --- a/src/Pure/System/scala.scala +++ b/src/Pure/System/scala.scala @@ -1,325 +1,341 @@ /* Title: Pure/System/scala.scala Author: Makarius Support for Scala at runtime. */ package isabelle import java.io.{File => JFile, StringWriter, PrintWriter} import scala.tools.nsc.{GenericRunnerSettings, ConsoleWriter, NewLinePrintWriter} import scala.tools.nsc.interpreter.{IMain, Results} import scala.tools.nsc.interpreter.shell.ReplReporterImpl object Scala { /** registered functions **/ abstract class Fun(val name: String, val thread: Boolean = false) { override def toString: String = name - def multi: Boolean = true + def single: Boolean = false + def bytes: Boolean = false def position: Properties.T = here.position def here: Scala_Project.Here def invoke(args: List[Bytes]): List[Bytes] } + trait Single_Fun extends Fun { override def single: Boolean = true } + trait Bytes_Fun extends Fun { override def bytes: Boolean = true } + abstract class Fun_Strings(name: String, thread: Boolean = false) extends Fun(name, thread = thread) { override def invoke(args: List[Bytes]): List[Bytes] = apply(args.map(_.text)).map(Bytes.apply) def apply(args: List[String]): List[String] } abstract class Fun_String(name: String, thread: Boolean = false) - extends Fun_Strings(name, thread = thread) { - override def multi: Boolean = false + extends Fun_Strings(name, thread = thread) with Single_Fun { override def apply(args: List[String]): List[String] = List(apply(Library.the_single(args))) def apply(arg: String): String } + abstract class Fun_Bytes(name: String, thread: Boolean = false) + extends Fun(name, thread = thread) with Single_Fun with Bytes_Fun { + override def invoke(args: List[Bytes]): List[Bytes] = + List(apply(Library.the_single(args))) + def apply(arg: Bytes): Bytes + } + + val encode_fun: XML.Encode.T[Fun] = { fun => + import XML.Encode._ + pair(string, pair(pair(bool, bool), properties))( + fun.name, ((fun.single, fun.bytes), fun.position)) + } + class Functions(val functions: Fun*) extends Isabelle_System.Service lazy val functions: List[Fun] = Isabelle_System.make_services(classOf[Functions]).flatMap(_.functions) /** demo functions **/ object Echo extends Fun_String("echo") { val here = Scala_Project.here def apply(arg: String): String = arg } object Sleep extends Fun_String("sleep") { val here = Scala_Project.here def apply(seconds: String): String = { val t = seconds match { case Value.Double(s) => Time.seconds(s) case _ => error("Malformed argument: " + quote(seconds)) } val t0 = Time.now() t.sleep() val t1 = Time.now() (t1 - t0).toString } } /** compiler **/ def class_path(): List[String] = for { prop <- List("isabelle.scala.classpath", "java.class.path") elems = System.getProperty(prop, "") if elems.nonEmpty elem <- space_explode(JFile.pathSeparatorChar, elems) if elem.nonEmpty } yield elem object Compiler { def default_print_writer: PrintWriter = new NewLinePrintWriter(new ConsoleWriter, true) def context( print_writer: PrintWriter = default_print_writer, error: String => Unit = Exn.error, jar_dirs: List[JFile] = Nil, class_loader: Option[ClassLoader] = None ): Context = { def find_jars(dir: JFile): List[String] = File.find_files(dir, file => file.getName.endsWith(".jar")). map(File.absolute_name) val settings = new GenericRunnerSettings(error) settings.classpath.value = (class_path() ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator) new Context(settings, print_writer, class_loader) } class Context private [Compiler]( val settings: GenericRunnerSettings, val print_writer: PrintWriter, val class_loader: Option[ClassLoader] ) { override def toString: String = settings.toString val interp: IMain = new IMain(settings, new ReplReporterImpl(settings, print_writer)) { override def parentClassLoader: ClassLoader = class_loader getOrElse super.parentClassLoader } } def toplevel(interpret: Boolean, source: String): List[String] = { val out = new StringWriter val interp = Compiler.context(print_writer = new PrintWriter(out)).interp val marker = '\u000b' val ok = interp.withLabel(marker.toString) { if (interpret) interp.interpret(source) == Results.Success else (new interp.ReadEvalPrint).compile(source) } out.close() val Error = """(?s)^\S* error: (.*)$""".r val errors = space_explode(marker, Library.strip_ansi_color(out.toString)). collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) }) if (!ok && errors.isEmpty) List("Error") else errors } } object Toplevel extends Fun_String("scala_toplevel") { val here = Scala_Project.here def apply(arg: String): String = { val (interpret, source) = YXML.parse_body(arg) match { case Nil => (false, "") case List(XML.Text(source)) => (false, source) case body => import XML.Decode._; pair(bool, string)(body) } val errors = try { Compiler.toplevel(interpret, source) } catch { case ERROR(msg) => List(msg) } locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) } } } /** interpreter thread **/ object Interpreter { /* requests */ sealed abstract class Request case class Execute(command: Compiler.Context => Unit) extends Request case object Shutdown extends Request /* known interpreters */ private val known = Synchronized(Set.empty[Interpreter]) def add(interpreter: Interpreter): Unit = known.change(_ + interpreter) def del(interpreter: Interpreter): Unit = known.change(_ - interpreter) def get[A](which: PartialFunction[Interpreter, A]): Option[A] = known.value.collectFirst(which) } class Interpreter(context: Compiler.Context) { interpreter => private val running = Synchronized[Option[Thread]](None) def running_thread(thread: Thread): Boolean = running.value.contains(thread) def interrupt_thread(): Unit = running.change({ opt => opt.foreach(_.interrupt()); opt }) private lazy val thread: Consumer_Thread[Interpreter.Request] = Consumer_Thread.fork("Scala.Interpreter") { case Interpreter.Execute(command) => try { running.change(_ => Some(Thread.currentThread())) command(context) } finally { running.change(_ => None) Exn.Interrupt.dispose() } true case Interpreter.Shutdown => Interpreter.del(interpreter) false } def shutdown(): Unit = { thread.send(Interpreter.Shutdown) interrupt_thread() thread.shutdown() } def execute(command: Compiler.Context => Unit): Unit = thread.send(Interpreter.Execute(command)) Interpreter.add(interpreter) thread } /** invoke Scala functions from ML **/ /* invoke function */ object Tag extends Enumeration { val NULL, OK, ERROR, FAIL, INTERRUPT = Value } def function_thread(name: String): Boolean = functions.find(fun => fun.name == name) match { case Some(fun) => fun.thread case None => false } def function_body(name: String, args: List[Bytes]): (Tag.Value, List[Bytes]) = functions.find(fun => fun.name == name) match { case Some(fun) => Exn.capture { fun.invoke(args) } match { case Exn.Res(null) => (Tag.NULL, Nil) case Exn.Res(res) => (Tag.OK, res) case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, Nil) case Exn.Exn(e) => (Tag.ERROR, List(Bytes(Exn.message(e)))) } case None => (Tag.FAIL, List(Bytes("Unknown Isabelle/Scala function: " + quote(name)))) } /* protocol handler */ class Handler extends Session.Protocol_Handler { private var session: Session = null private var futures = Map.empty[String, Future[Unit]] override def init(session: Session): Unit = synchronized { this.session = session } override def exit(): Unit = synchronized { for ((id, future) <- futures) cancel(id, future) futures = Map.empty } private def result(id: String, tag: Scala.Tag.Value, res: List[Bytes]): Unit = synchronized { if (futures.isDefinedAt(id)) { session.protocol_command_raw("Scala.result", Bytes(id) :: Bytes(tag.id.toString) :: res) futures -= id } } private def cancel(id: String, future: Future[Unit]): Unit = { future.cancel() result(id, Scala.Tag.INTERRUPT, Nil) } private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized { msg.properties match { case Markup.Invoke_Scala(name, id) => def body(): Unit = { val (tag, res) = Scala.function_body(name, msg.chunks) result(id, tag, res) } val future = if (Scala.function_thread(name)) { Future.thread(name = Isabelle_Thread.make_name(base = "invoke_scala"))(body()) } else Future.fork(body()) futures += (id -> future) true case _ => false } } private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized { msg.properties match { case Markup.Cancel_Scala(id) => futures.get(id) match { case Some(future) => cancel(id, future) case None => } true case _ => false } } override val functions: Session.Protocol_Functions = List( Markup.Invoke_Scala.name -> invoke_scala, Markup.Cancel_Scala.name -> cancel_scala) } } class Scala_Functions extends Scala.Functions( Scala.Echo, Scala.Sleep, Scala.Toplevel, Bytes.Decode_Base64, Bytes.Encode_Base64, Bytes.Compress, Bytes.Uncompress, Doc.Doc_Names, Bibtex.Check_Database, Isabelle_System.Make_Directory, Isabelle_System.Copy_Dir, Isabelle_System.Copy_File, Isabelle_System.Copy_File_Base, Isabelle_System.Rm_Tree, Isabelle_System.Download, Isabelle_System.Isabelle_Id, Isabelle_Tool.Isabelle_Tools, isabelle.atp.SystemOnTPTP.List_Systems, isabelle.atp.SystemOnTPTP.Run_System) diff --git a/src/Pure/Tools/server_commands.scala b/src/Pure/Tools/server_commands.scala --- a/src/Pure/Tools/server_commands.scala +++ b/src/Pure/Tools/server_commands.scala @@ -1,334 +1,334 @@ /* Title: Pure/Tools/server_commands.scala Author: Makarius Miscellaneous Isabelle server commands. */ package isabelle object Server_Commands { def default_preferences: String = Options.read_prefs() object Help extends Server.Command("help") { override val command_body: Server.Command_Body = { case (context, ()) => context.command_list } } object Echo extends Server.Command("echo") { override val command_body: Server.Command_Body = { case (_, t) => t } } object Cancel extends Server.Command("cancel") { sealed case class Args(task: UUID.T) def unapply(json: JSON.T): Option[Args] = for { task <- JSON.uuid(json, "task") } yield Args(task) override val command_body: Server.Command_Body = { case (context, Cancel(args)) => context.cancel_task(args.task) } } object Shutdown extends Server.Command("shutdown") { override val command_body: Server.Command_Body = { case (context, ()) => context.server.shutdown() } } object Session_Build extends Server.Command("session_build") { sealed case class Args( session: String, preferences: String = default_preferences, options: List[String] = Nil, dirs: List[String] = Nil, include_sessions: List[String] = Nil, verbose: Boolean = false) def unapply(json: JSON.T): Option[Args] = for { session <- JSON.string(json, "session") preferences <- JSON.string_default(json, "preferences", default_preferences) options <- JSON.strings_default(json, "options") dirs <- JSON.strings_default(json, "dirs") include_sessions <- JSON.strings_default(json, "include_sessions") verbose <- JSON.bool_default(json, "verbose") } yield { Args(session, preferences = preferences, options = options, dirs = dirs, include_sessions = include_sessions, verbose = verbose) } def command( args: Args, progress: Progress = new Progress ) : (JSON.Object.T, Build.Results, Options, Sessions.Base_Info) = { val options = Options.init(prefs = args.preferences, opts = args.options) val dirs = args.dirs.map(Path.explode) val base_info = Sessions.base_info(options, args.session, progress = progress, dirs = dirs, include_sessions = args.include_sessions).check val results = Build.build(options, selection = Sessions.Selection.session(args.session), progress = progress, build_heap = true, dirs = dirs, infos = base_info.infos, verbose = args.verbose) val sessions_order = base_info.sessions_structure.imports_topological_order.zipWithIndex. toMap.withDefaultValue(-1) val results_json = JSON.Object( "ok" -> results.ok, "return_code" -> results.rc, "sessions" -> results.sessions.toList.sortBy(sessions_order).map { session => val result = results(session) JSON.Object( "session" -> session, "ok" -> result.ok, "return_code" -> result.rc, "timeout" -> result.timeout, "timing" -> result.timing.json) }) if (results.ok) (results_json, results, options, base_info) else { throw new Server.Error("Session build failed: " + Process_Result.RC.print(results.rc), results_json) } } override val command_body: Server.Command_Body = { case (context, Session_Build(args)) => context.make_task(task => Session_Build.command(args, progress = task.progress)._1) } } object Session_Start extends Server.Command("session_start") { sealed case class Args( build: Session_Build.Args, print_mode: List[String] = Nil) def unapply(json: JSON.T): Option[Args] = for { build <- Session_Build.unapply(json) print_mode <- JSON.strings_default(json, "print_mode") } yield Args(build = build, print_mode = print_mode) def command( args: Args, progress: Progress = new Progress, log: Logger = No_Logger ) : (JSON.Object.T, (UUID.T, Headless.Session)) = { val (_, _, options, base_info) = try { Session_Build.command(args.build, progress = progress) } catch { case exn: Server.Error => error(exn.message) } val resources = Headless.Resources(options, base_info, log = log) val session = resources.start_session(print_mode = args.print_mode, progress = progress) val id = UUID.random() val res = JSON.Object( "session_id" -> id.toString, "tmp_dir" -> File.path(session.tmp_dir).implode) (res, id -> session) } override val command_body: Server.Command_Body = { case (context, Session_Start(args)) => context.make_task { task => val (res, entry) = Session_Start.command(args, progress = task.progress, log = context.server.log) context.server.add_session(entry) res } } } object Session_Stop extends Server.Command("session_stop") { def unapply(json: JSON.T): Option[UUID.T] = JSON.uuid(json, "session_id") def command(session: Headless.Session): (JSON.Object.T, Process_Result) = { val result = session.stop() val result_json = JSON.Object("ok" -> result.ok, "return_code" -> result.rc) if (result.ok) (result_json, result) else throw new Server.Error("Session shutdown failed: " + result.print_rc, result_json) } override val command_body: Server.Command_Body = { case (context, Session_Stop(id)) => context.make_task(_ => { val session = context.server.remove_session(id) Session_Stop.command(session)._1 }) } } object Use_Theories extends Server.Command("use_theories") { sealed case class Args( session_id: UUID.T, theories: List[String], master_dir: String = "", pretty_margin: Double = Pretty.default_margin, unicode_symbols: Boolean = false, export_pattern: String = "", check_delay: Option[Time] = None, check_limit: Option[Int] = None, watchdog_timeout: Option[Time] = None, nodes_status_delay: Option[Time] = None, commit_cleanup_delay: Option[Time] = None) def unapply(json: JSON.T): Option[Args] = for { session_id <- JSON.uuid(json, "session_id") theories <- JSON.strings(json, "theories") master_dir <- JSON.string_default(json, "master_dir") pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin) unicode_symbols <- JSON.bool_default(json, "unicode_symbols") export_pattern <- JSON.string_default(json, "export_pattern") check_delay = JSON.seconds(json, "check_delay") check_limit = JSON.int(json, "check_limit") watchdog_timeout = JSON.seconds(json, "watchdog_timeout") nodes_status_delay = JSON.seconds(json, "nodes_status_delay") commit_cleanup_delay = JSON.seconds(json, "commit_cleanup_delay") } yield { Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin, unicode_symbols = unicode_symbols, export_pattern = export_pattern, check_delay = check_delay, check_limit = check_limit, watchdog_timeout = watchdog_timeout, nodes_status_delay = nodes_status_delay, commit_cleanup_delay = commit_cleanup_delay) } def command(args: Args, session: Headless.Session, id: UUID.T = UUID.random(), progress: Progress = new Progress ): (JSON.Object.T, Headless.Use_Theories_Result) = { val result = session.use_theories(args.theories, master_dir = args.master_dir, check_delay = args.check_delay.getOrElse(session.default_check_delay), check_limit = args.check_limit.getOrElse(session.default_check_limit), watchdog_timeout = args.watchdog_timeout.getOrElse(session.default_watchdog_timeout), nodes_status_delay = args.nodes_status_delay.getOrElse(session.default_nodes_status_delay), commit_cleanup_delay = args.commit_cleanup_delay.getOrElse(session.default_commit_cleanup_delay), id = id, progress = progress) def output_text(text: String): String = Symbol.output(args.unicode_symbols, text) def output_message(tree: XML.Tree, pos: Position.T): JSON.Object.T = { val position = "pos" -> Position.JSON(pos) tree match { case XML.Text(msg) => Server.Reply.message(output_text(msg)) + position case elem: XML.Elem => val msg = XML.content(Pretty.formatted(List(elem), margin = args.pretty_margin)) val kind = Markup.messages.collectFirst({ case (a, b) if b == elem.name => if (Protocol.is_legacy(elem)) Markup.WARNING else a }) getOrElse "" Server.Reply.message(output_text(msg), kind = kind) + position } } val result_json = JSON.Object( "ok" -> result.ok, "errors" -> (for { (name, status) <- result.nodes if !status.ok (tree, pos) <- result.snapshot(name).messages if Protocol.is_error(tree) } yield output_message(tree, pos)), "nodes" -> (for ((name, status) <- result.nodes) yield { val snapshot = result.snapshot(name) name.json + ("status" -> status.json) + ("messages" -> (for { (tree, pos) <- snapshot.messages if Protocol.is_exported(tree) } yield output_message(tree, pos))) + ("exports" -> (if (args.export_pattern == "") Nil else { val matcher = Export.make_matcher(args.export_pattern) for { entry <- snapshot.exports if matcher(entry.theory_name, entry.name) } yield { - val (base64, body) = entry.uncompressed.maybe_base64 + val (base64, body) = entry.uncompressed.maybe_encode_base64 JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body) } })) })) (result_json, result) } override val command_body: Server.Command_Body = { case (context, Use_Theories(args)) => context.make_task { task => val session = context.server.the_session(args.session_id) Use_Theories.command(args, session, id = task.id, progress = task.progress)._1 } } } object Purge_Theories extends Server.Command("purge_theories") { sealed case class Args( session_id: UUID.T, theories: List[String] = Nil, master_dir: String = "", all: Boolean = false) def unapply(json: JSON.T): Option[Args] = for { session_id <- JSON.uuid(json, "session_id") theories <- JSON.strings_default(json, "theories") master_dir <- JSON.string_default(json, "master_dir") all <- JSON.bool_default(json, "all") } yield { Args(session_id, theories = theories, master_dir = master_dir, all = all) } def command( args: Args, session: Headless.Session ) : (JSON.Object.T, (List[Document.Node.Name], List[Document.Node.Name])) = { val (purged, retained) = session.purge_theories( theories = args.theories, master_dir = args.master_dir, all = args.all) val result_json = JSON.Object("purged" -> purged.map(_.json), "retained" -> retained.map(_.json)) (result_json, (purged, retained)) } override val command_body: Server.Command_Body = { case (context, Purge_Theories(args)) => val session = context.server.the_session(args.session_id) command(args, session)._1 } } } class Server_Commands extends Server.Commands( Server_Commands.Help, Server_Commands.Echo, Server_Commands.Cancel, Server_Commands.Shutdown, Server_Commands.Session_Build, Server_Commands.Session_Start, Server_Commands.Session_Stop, Server_Commands.Use_Theories, Server_Commands.Purge_Theories)