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,235 @@ /* 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 = { 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("decode_base64") with Scala.Fun_Single_Bytes { val here = Scala_Project.here def invoke(args: List[Bytes]): List[Bytes] = List(base64(Library.the_single(args).text)) } - object Encode_Base64 extends Scala.Fun("encode_base64") { + object Encode_Base64 extends Scala.Fun("encode_base64") with Scala.Fun_Single_Bytes { val here = Scala_Project.here def invoke(args: List[Bytes]): List[Bytes] = List(Bytes(Library.the_single(args).base64)) } /* XZ compression */ - object Compress extends Scala.Fun("compress") { + object Compress extends Scala.Fun("compress") with Scala.Fun_Single_Bytes { val here = Scala_Project.here def invoke(args: List[Bytes]): List[Bytes] = List(Library.the_single(args).compress()) } - object Uncompress extends Scala.Fun("uncompress") { + object Uncompress extends Scala.Fun("uncompress") with Scala.Fun_Single_Bytes { val here = Scala_Project.here def invoke(args: List[Bytes]): List[Bytes] = List(Library.the_single(args).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 = { val b = if (offset == 0 && length == bytes.length) bytes else Bytes(bytes, offset, length).bytes Base64.getEncoder.encodeToString(b) } def maybe_base64: (Boolean, String) = { val s = text if (this == Bytes(s)) (false, s) else (true, 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/PIDE/resources.ML b/src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML +++ b/src/Pure/PIDE/resources.ML @@ -1,446 +1,447 @@ (* 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 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 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"); +val scala_function_default = the_default ((true, false), Position.none); + (*regular resources*) fun scala_function a = - (a, the_default (false, Position.none) (Symtab.lookup (get_session_base1 #scala_functions) a)); + (a, scala_function_default (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 flags = #1 (scala_function_default (AList.lookup (op =) funs 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/scala.scala b/src/Pure/System/scala.scala --- a/src/Pure/System/scala.scala +++ b/src/Pure/System/scala.scala @@ -1,325 +1,335 @@ /* 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 Fun_Single extends Fun { override def single: Boolean = true } + trait Fun_Bytes extends Fun { override def bytes: Boolean = true } + trait Fun_Single_Bytes extends Fun_Single with Fun_Bytes + 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 Fun_Single { override def apply(args: List[String]): List[String] = List(apply(Library.the_single(args))) def apply(arg: String): String } + 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)