diff --git a/src/HOL/Tools/ATP/system_on_tptp.scala b/src/HOL/Tools/ATP/system_on_tptp.scala --- a/src/HOL/Tools/ATP/system_on_tptp.scala +++ b/src/HOL/Tools/ATP/system_on_tptp.scala @@ -1,91 +1,91 @@ /* Title: HOL/Tools/ATP/system_on_tptp.scala Author: Makarius Support for remote ATPs via SystemOnTPTP. */ package isabelle.atp import isabelle._ import java.net.URL object SystemOnTPTP { /* requests */ def get_url(options: Options): URL = Url(options.string("SystemOnTPTP")) def post_request( url: URL, parameters: List[(String, Any)], timeout: Time = HTTP.Client.default_timeout): HTTP.Content = { try { HTTP.Client.post(url, ("NoHTML" -> 1) :: parameters, timeout = timeout, user_agent = "Sledgehammer") } catch { case ERROR(msg) => cat_error("Failed to access SystemOnTPTP server", msg) } } /* list systems */ def list_systems(url: URL): HTTP.Content = post_request(url, List("SubmitButton" -> "ListSystems", "ListStatus" -> "READY", "QuietFlag" -> "-q0")) - object List_Systems extends Scala.Fun("SystemOnTPTP.list_systems", thread = true) + object List_Systems extends Scala.Fun_String("SystemOnTPTP.list_systems", thread = true) { val here = Scala_Project.here def apply(url: String): String = list_systems(Url(url)).text } /* run system */ def run_system(url: URL, system: String, problem: String, extra: String = "", quiet: String = "01", timeout: Time = Time.seconds(60)): HTTP.Content = { val paramaters = List( "SubmitButton" -> "RunSelectedSystems", "ProblemSource" -> "FORMULAE", "FORMULAEProblem" -> problem, "ForceSystem" -> "-force", "System___" + system -> system, "TimeLimit___" + system -> timeout.seconds.ceil.toLong, "Command___" + system -> extra, "QuietFlag" -> ("-q" + quiet)) post_request(url, paramaters, timeout = timeout + Time.seconds(15)) } - object Run_System extends Scala.Fun("SystemOnTPTP.run_system", thread = true) + object Run_System extends Scala.Fun_String("SystemOnTPTP.run_system", thread = true) { val here = Scala_Project.here def apply(arg: String): String = { val List(url, system, problem_path, extra, Value.Int(timeout)) = Library.split_strings0(arg) val problem = File.read(Path.explode(problem_path)) val res = run_system(Url(url), system, problem, extra = extra, timeout = Time.ms(timeout)) val text = res.text val timing = res.elapsed_time.ms val bad_prover = "WARNING: " + system + " does not exist" if (split_lines(text).exists(_.startsWith(bad_prover))) { error("The ATP " + quote(system) + " is not available at SystemOnTPTP") } else Library.cat_strings0(List(text, timing.toString)) } } } diff --git a/src/HOL/Tools/Nitpick/kodkod.scala b/src/HOL/Tools/Nitpick/kodkod.scala --- a/src/HOL/Tools/Nitpick/kodkod.scala +++ b/src/HOL/Tools/Nitpick/kodkod.scala @@ -1,178 +1,178 @@ /* Title: HOL/Tools/Nitpick/kodkod.scala Author: Makarius Scala interface for Kodkod. */ package isabelle.nitpick import isabelle._ import java.util.concurrent.{TimeUnit, LinkedBlockingQueue, ThreadPoolExecutor} import org.antlr.runtime.{ANTLRInputStream, RecognitionException} import de.tum.in.isabelle.Kodkodi.{Context, KodkodiLexer, KodkodiParser} object Kodkod { /** result **/ sealed case class Result(rc: Int, out: String, err: String) { def ok: Boolean = rc == 0 def check: String = if (ok) out else error(if (err.isEmpty) "Error" else err) def encode: XML.Body = { import XML.Encode._ triple(int, string, string)((rc, out, err)) } } /** execute **/ def execute(source: String, solve_all: Boolean = false, prove: Boolean = false, max_solutions: Int = Integer.MAX_VALUE, cleanup_inst: Boolean = false, timeout: Time = Time.zero, max_threads: Int = 0): Result = { /* executor */ val pool_size = if (max_threads == 0) Isabelle_Thread.max_threads() else max_threads val executor: ThreadPoolExecutor = new ThreadPoolExecutor(pool_size, pool_size, 0L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable], new ThreadPoolExecutor.CallerRunsPolicy) val executor_killed = Synchronized(false) def executor_kill(): Unit = executor_killed.change(b => if (b) b else { Isabelle_Thread.fork() { executor.shutdownNow() }; true }) /* system context */ class Exit extends Exception("EXIT") class Exec_Context extends Context { private var rc = 0 private val out = new StringBuilder private val err = new StringBuilder def return_code(i: Int): Unit = synchronized { rc = rc max i} override def output(s: String): Unit = synchronized { Exn.Interrupt.expose() out ++= s out += '\n' } override def error(s: String): Unit = synchronized { Exn.Interrupt.expose() err ++= s err += '\n' } override def exit(i: Int): Unit = synchronized { return_code(i) executor_kill() throw new Exit } def result(): Result = synchronized { Result(rc, out.toString, err.toString) } } val context = new Exec_Context /* main */ try { val lexer = new KodkodiLexer(new ANTLRInputStream(Bytes(source).stream())) val parser = KodkodiParser.create(context, executor, false, solve_all, prove, max_solutions, cleanup_inst, lexer) val timeout_request = if (timeout.is_zero) None else { Some(Event_Timer.request(Time.now() + timeout) { context.error("Ran out of time") context.return_code(2) executor_kill() }) } try { parser.problems() } catch { case exn: RecognitionException => parser.reportError(exn) } timeout_request.foreach(_.cancel()) if (parser.getTokenStream.LA(1) != KodkodiParser.EOF) { context.error("Error: trailing tokens") context.exit(1) } if (lexer.getNumberOfSyntaxErrors + parser.getNumberOfSyntaxErrors > 0) { context.exit(1) } } catch { case _: Exit => case exn: Throwable => val message = exn.getMessage context.error(if (message.isEmpty) exn.toString else "Error: " + message) context.return_code(1) } executor.shutdownNow() context.result() } /** protocol handler **/ def warmup(): String = execute( "solver: \"MiniSat\"\n" + File.read(Path.explode("$KODKODI/examples/weber3.kki"))).check class Handler extends Session.Protocol_Handler { override def init(session: Session): Unit = warmup() } /** scala function **/ - object Fun extends Scala.Fun("kodkod", thread = true) + object Fun extends Scala.Fun_String("kodkod", thread = true) { val here = Scala_Project.here def apply(args: String): String = { val (timeout, (solve_all, (max_solutions, (max_threads, kki)))) = { import XML.Decode._ pair(int, pair(bool, pair(int, pair(int, string))))(YXML.parse_body(args)) } val result = execute(kki, solve_all = solve_all, max_solutions = max_solutions, timeout = Time.ms(timeout), max_threads = max_threads) YXML.string_of_body(result.encode) } } } class Scala_Functions extends Scala.Functions(Kodkod.Fun) 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,435 +1,443 @@ (* 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, session_chapters: (string * string) list, bibtex_entries: (string * string list) list, command_timings: Properties.T list, - scala_functions: (string * Position.T) list, + scala_functions: (string * (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 session_chapter: string -> string val last_timing: Toplevel.transition -> Time.time val scala_functions: unit -> string list - val check_scala_function: Proof.context -> string * Position.T -> string + val check_scala_function: Proof.context -> string * Position.T -> string * 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, session_chapters = Symtab.empty: string Symtab.table, bibtex_entries = Symtab.empty: string list Symtab.table, timings = empty_timings, - scala_functions = Symtab.empty: Position.T Symtab.table}, + scala_functions = Symtab.empty: (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, session_chapters, bibtex_entries, command_timings, 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 = fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir)) session_directories Symtab.empty, session_chapters = Symtab.make session_chapters, bibtex_entries = Symtab.make bibtex_entries, timings = make_timings command_timings, 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, (session_chapters, (bibtex_entries, (command_timings, (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 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 string)) (list string)))))))) end; in init_session {session_positions = session_positions, session_directories = session_directories, session_chapters = session_chapters, bibtex_entries = bibtex_entries, command_timings = command_timings, - scala_functions = map (apsnd Position.of_properties) scala_functions, + 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}) => Markup.entity Markup.sessionN name |> Markup.properties (Position.entity_properties_of false serial pos)) (get_session_base1 #session_positions) ctxt arg; fun session_chapter name = the_default "Unsorted" (Symtab.lookup (get_session_base1 #session_chapters) name); fun last_timing tr = get_timings (get_session_base1 #timings) tr; (* Scala functions *) (*raw bootstrap environment*) fun scala_functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS"); (*regular resources*) -fun scala_function_pos name = - (name, the_default Position.none (Symtab.lookup (get_session_base1 #scala_functions) name)); +fun scala_function a = + (a, the_default (false, Position.none) (Symtab.lookup (get_session_base1 #scala_functions) a)); fun check_scala_function ctxt arg = - Completion.check_entity Markup.scala_functionN - (scala_functions () |> sort_strings |> map scala_function_pos) 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 _ = Theory.setup (Thy_Output.antiquotation_verbatim_embedded \<^binding>\scala_function\ - (Scan.lift Parse.embedded_position) check_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 #> ML_Syntax.print_string)) #> + >> (uncurry check_scala_function #> #1 #> ML_Syntax.print_string)) #> ML_Antiquotation.value_embedded \<^binding>\scala\ (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) => - let val name = check_scala_function ctxt arg - in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end))); + let + val (name, multi) = check_scala_function ctxt arg; + val func = if multi then "Scala.function" else "Scala.function1"; + 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, [], []); val extend = I; 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 = Theory.begin_theory name parents |> map_files (fn _ => (Path.explode (Path.implode_symbolic master_dir), imports, [])) |> Thy_Header.add_keywords keywords; (* 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) => let val _ = check ctxt NONE source; val latex = Latex.string (Latex.output_ascii_breakable "/" (Input.string_of source)); in Latex.enclose_block "\\isatt{" "}" [latex] end); 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 (Thy_Output.antiquotation_verbatim_embedded \<^binding>\session\ (Scan.lift Parse.embedded_position) check_session #> Thy_Output.antiquotation_raw_embedded \<^binding>\path\ (document_antiq check_path) (K I) #> Thy_Output.antiquotation_raw_embedded \<^binding>\file\ (document_antiq check_file) (K I) #> Thy_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,451 +1,451 @@ /* 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) } 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, 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, string)), list(string))))))))( (sessions_structure.session_positions, (sessions_structure.dest_session_directories, (sessions_structure.session_chapters, (sessions_structure.bibtex_entries, (command_timings, - (Scala.functions.map(fun => (fun.name, fun.position)), + (Scala.functions.map(fun => (fun.name, (fun.multi, fun.position))), (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)) def is_hidden(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)) /* 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_name)) 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/PIDE/session.scala b/src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala +++ b/src/Pure/PIDE/session.scala @@ -1,774 +1,784 @@ /* Title: Pure/PIDE/session.scala Author: Makarius Options: :folding=explicit: PIDE editor session, potentially with running prover process. */ package isabelle import scala.collection.immutable.Queue import scala.collection.mutable import scala.annotation.tailrec object Session { /* outlets */ object Consumer { def apply[A](name: String)(consume: A => Unit): Consumer[A] = new Consumer[A](name, consume) } final class Consumer[-A] private(val name: String, val consume: A => Unit) class Outlet[A](dispatcher: Consumer_Thread[() => Unit]) { private val consumers = Synchronized[List[Consumer[A]]](Nil) def += (c: Consumer[A]): Unit = consumers.change(Library.update(c)) def -= (c: Consumer[A]): Unit = consumers.change(Library.remove(c)) def post(a: A): Unit = { for (c <- consumers.value.iterator) { dispatcher.send(() => try { c.consume(a) } catch { case exn: Throwable => Output.error_message("Consumer failed: " + quote(c.name) + "\n" + Exn.message(exn)) }) } } } /* change */ sealed case class Change( previous: Document.Version, syntax_changed: List[Document.Node.Name], deps_changed: Boolean, doc_edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name], version: Document.Version) case object Change_Flush /* events */ //{{{ case class Command_Timing(props: Properties.T) case class Theory_Timing(props: Properties.T) case class Runtime_Statistics(props: Properties.T) case class Task_Statistics(props: Properties.T) case class Global_Options(options: Options) case object Caret_Focus case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String) case class Build_Theories(id: String, master_dir: Path, theories: List[(Options, List[Path])]) case class Commands_Changed( assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command]) sealed abstract class Phase { def print: String = this match { case Terminated(result) => if (result.ok) "finished" else "failed" case _ => Word.lowercase(this.toString) } } case object Inactive extends Phase // stable case object Startup extends Phase // transient case object Ready extends Phase // metastable case object Shutdown extends Phase // transient case class Terminated(result: Process_Result) extends Phase // stable //}}} /* syslog */ private[Session] class Syslog(limit: Int) { private var queue = Queue.empty[XML.Elem] private var length = 0 def += (msg: XML.Elem): Unit = synchronized { queue = queue.enqueue(msg) length += 1 if (length > limit) queue = queue.dequeue._2 } def content: String = synchronized { cat_lines(queue.iterator.map(XML.content)) + (if (length > limit) "\n(A total of " + length + " messages...)" else "") } } /* protocol handlers */ type Protocol_Function = Prover.Protocol_Output => Boolean abstract class Protocol_Handler extends Isabelle_System.Service { def init(session: Session): Unit = {} def exit(): Unit = {} def functions: List[(String, Protocol_Function)] = Nil def prover_options(options: Options): Options = options } } class Session(_session_options: => Options, val resources: Resources) extends Document.Session { session => val cache: XML.Cache = XML.Cache.make() def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = Command.Blobs_Info.none /* global flags */ @volatile var timing: Boolean = false @volatile var verbose: Boolean = false /* dynamic session options */ def session_options: Options = _session_options def output_delay: Time = session_options.seconds("editor_output_delay") def consolidate_delay: Time = session_options.seconds("editor_consolidate_delay") def prune_delay: Time = session_options.seconds("editor_prune_delay") def prune_size: Int = session_options.int("editor_prune_size") def syslog_limit: Int = session_options.int("editor_syslog_limit") def reparse_limit: Int = session_options.int("editor_reparse_limit") /* dispatcher */ private val dispatcher = Consumer_Thread.fork[() => Unit]("Session.dispatcher", daemon = true) { case e => e(); true } def assert_dispatcher[A](body: => A): A = { assert(dispatcher.check_thread) body } def require_dispatcher[A](body: => A): A = { require(dispatcher.check_thread, "not on dispatcher thread") body } def send_dispatcher(body: => Unit): Unit = { if (dispatcher.check_thread) body else dispatcher.send(() => body) } def send_wait_dispatcher(body: => Unit): Unit = { if (dispatcher.check_thread) body else dispatcher.send_wait(() => body) } /* outlets */ val finished_theories = new Session.Outlet[Document.Snapshot](dispatcher) val command_timings = new Session.Outlet[Session.Command_Timing](dispatcher) val theory_timings = new Session.Outlet[Session.Theory_Timing](dispatcher) val runtime_statistics = new Session.Outlet[Session.Runtime_Statistics](dispatcher) val task_statistics = new Session.Outlet[Session.Task_Statistics](dispatcher) val global_options = new Session.Outlet[Session.Global_Options](dispatcher) val caret_focus = new Session.Outlet[Session.Caret_Focus.type](dispatcher) val raw_edits = new Session.Outlet[Session.Raw_Edits](dispatcher) val commands_changed = new Session.Outlet[Session.Commands_Changed](dispatcher) val phase_changed = new Session.Outlet[Session.Phase](dispatcher) val syslog_messages = new Session.Outlet[Prover.Output](dispatcher) val raw_output_messages = new Session.Outlet[Prover.Output](dispatcher) val trace_events = new Session.Outlet[Simplifier_Trace.Event.type](dispatcher) val debugger_updates = new Session.Outlet[Debugger.Update.type](dispatcher) val all_messages = new Session.Outlet[Prover.Message](dispatcher) // potential bottle-neck! /** main protocol manager **/ /* internal messages */ private case class Start(start_prover: Prover.Receiver => Prover) private case object Stop private case class Get_State(promise: Promise[Document.State]) private case class Cancel_Exec(exec_id: Document_ID.Exec) - private case class Protocol_Command(name: String, args: List[String]) + private case class Protocol_Command_Raw(name: String, args: List[Bytes]) + private case class Protocol_Command_Args(name: String, args: List[String]) private case class Update_Options(options: Options) private case object Consolidate_Execution private case object Prune_History /* phase */ private def post_phase(new_phase: Session.Phase): Session.Phase = { phase_changed.post(new_phase) new_phase } private val _phase = Synchronized[Session.Phase](Session.Inactive) private def phase_=(new_phase: Session.Phase): Unit = _phase.change(_ => post_phase(new_phase)) def phase: Session.Phase = _phase.value def is_ready: Boolean = phase == Session.Ready /* syslog */ private val syslog = new Session.Syslog(syslog_limit) def syslog_content(): String = syslog.content /* pipelined change parsing */ private case class Text_Edits( previous: Future[Document.Version], doc_blobs: Document.Blobs, text_edits: List[Document.Edit_Text], consolidate: List[Document.Node.Name], version_result: Promise[Document.Version]) private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true) { case Text_Edits(previous, doc_blobs, text_edits, consolidate, version_result) => val prev = previous.get_finished val change = Timing.timeit("parse_change", timing) { resources.parse_change(reparse_limit, prev, doc_blobs, text_edits, consolidate) } version_result.fulfill(change.version) manager.send(change) true } /* buffered changes */ private object change_buffer { private var assignment: Boolean = false private var nodes: Set[Document.Node.Name] = Set.empty private var commands: Set[Command] = Set.empty def flush(): Unit = synchronized { if (assignment || nodes.nonEmpty || commands.nonEmpty) commands_changed.post(Session.Commands_Changed(assignment, nodes, commands)) if (nodes.nonEmpty) consolidation.update(nodes) assignment = false nodes = Set.empty commands = Set.empty } private val delay_flush = Delay.first(output_delay) { flush() } def invoke(assign: Boolean, edited_nodes: List[Document.Node.Name], cmds: List[Command]): Unit = synchronized { assignment |= assign for (node <- edited_nodes) { nodes += node } for (command <- cmds) { nodes += command.node_name command.blobs_names.foreach(nodes += _) commands += command } delay_flush.invoke() } def shutdown(): Unit = { delay_flush.revoke() flush() } } /* postponed changes */ private object postponed_changes { private var postponed: List[Session.Change] = Nil def store(change: Session.Change): Unit = synchronized { postponed ::= change } def flush(state: Document.State): List[Session.Change] = synchronized { val (assigned, unassigned) = postponed.partition(change => state.is_assigned(change.previous)) postponed = unassigned assigned.reverse } } /* node consolidation */ private object consolidation { private val delay = Delay.first(consolidate_delay) { manager.send(Consolidate_Execution) } private val init_state: Option[Set[Document.Node.Name]] = Some(Set.empty) private val state = Synchronized(init_state) def exit(): Unit = { delay.revoke() state.change(_ => None) } def update(new_nodes: Set[Document.Node.Name] = Set.empty): Unit = { val active = state.change_result(st => (st.isDefined, st.map(nodes => if (nodes.isEmpty) new_nodes else nodes ++ new_nodes))) if (active) delay.invoke() } def flush(): Set[Document.Node.Name] = state.change_result(st => if (st.isDefined) (st.get, init_state) else (Set.empty, None)) } /* prover process */ private object prover { private val variable = Synchronized[Option[Prover]](None) def defined: Boolean = variable.value.isDefined def get: Prover = variable.value.get def set(p: Prover): Unit = variable.change(_ => Some(p)) def reset: Unit = variable.change(_ => None) def await_reset(): Unit = variable.guarded_access({ case None => Some((), None) case _ => None }) } /* file formats and protocol handlers */ private lazy val file_formats: File_Format.Session = File_Format.registry.start_session(session) private val protocol_handlers = Protocol_Handlers.init(session) def get_protocol_handler[C <: Session.Protocol_Handler](c: Class[C]): Option[C] = protocol_handlers.get(c.getName) match { case Some(h) if Library.is_subclass(h.getClass, c) => Some(h.asInstanceOf[C]) case _ => None } def init_protocol_handler(handler: Session.Protocol_Handler): Unit = protocol_handlers.init(handler) def prover_options(options: Options): Options = protocol_handlers.prover_options(file_formats.prover_options(options)) /* debugger */ private val debugger_handler = new Debugger.Handler(this) init_protocol_handler(debugger_handler) def debugger: Debugger = debugger_handler.debugger /* manager thread */ private val delay_prune = Delay.first(prune_delay) { manager.send(Prune_History) } private val manager: Consumer_Thread[Any] = { /* global state */ val global_state = Synchronized(Document.State.init) /* raw edits */ def handle_raw_edits( doc_blobs: Document.Blobs = Document.Blobs.empty, edits: List[Document.Edit_Text] = Nil, consolidate: List[Document.Node.Name] = Nil): Unit = //{{{ { require(prover.defined, "prover process not defined (handle_raw_edits)") if (edits.nonEmpty) prover.get.discontinue_execution() val previous = global_state.value.history.tip.version val version = Future.promise[Document.Version] global_state.change(_.continue_history(previous, edits, version)) raw_edits.post(Session.Raw_Edits(doc_blobs, edits)) change_parser.send(Text_Edits(previous, doc_blobs, edits, consolidate, version)) } //}}} /* resulting changes */ def handle_change(change: Session.Change): Unit = //{{{ { require(prover.defined, "prover process not defined (handle_change)") // define commands { val id_commands = new mutable.ListBuffer[Command] def id_command(command: Command): Unit = { for { (name, digest) <- command.blobs_defined if !global_state.value.defined_blob(digest) } { change.version.nodes(name).get_blob match { case Some(blob) => global_state.change(_.define_blob(digest)) prover.get.define_blob(digest, blob.bytes) case None => Output.error_message("Missing blob " + quote(name.toString)) } } if (!global_state.value.defined_command(command.id)) { global_state.change(_.define_command(command)) id_commands += command } } for { (_, edit) <- change.doc_edits } { edit.foreach({ case (c1, c2) => c1.foreach(id_command); c2.foreach(id_command) }) } if (id_commands.nonEmpty) { prover.get.define_commands_bulk(resources, id_commands.toList) } } val assignment = global_state.value.the_assignment(change.previous).check_finished global_state.change(_.define_version(change.version, assignment)) prover.get.update(change.previous.id, change.version.id, change.doc_edits, change.consolidate) resources.commit(change) } //}}} /* prover output */ def handle_output(output: Prover.Output): Unit = //{{{ { def bad_output(): Unit = { if (verbose) Output.warning("Ignoring bad prover output: " + output.message.toString) } def change_command(f: Document.State => (Command.State, Document.State)): Unit = { try { val st = global_state.change_result(f) if (!st.command.span.is_theory) { change_buffer.invoke(false, Nil, List(st.command)) } } catch { case _: Document.State.Fail => bad_output() } } output match { case msg: Prover.Protocol_Output => val handled = protocol_handlers.invoke(msg) if (!handled) { msg.properties match { case Protocol.Command_Timing(props, state_id, timing) if prover.defined => command_timings.post(Session.Command_Timing(props)) val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil))) change_command(_.accumulate(state_id, cache.elem(message), cache)) case Markup.Theory_Timing(props) => theory_timings.post(Session.Theory_Timing(props)) case Markup.Task_Statistics(props) => task_statistics.post(Session.Task_Statistics(props)) case Protocol.Export(args) if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined => val id = Value.Long.unapply(args.id.get).get val export = Export.make_entry("", args, msg.chunk, cache) change_command(_.add_export(id, (args.serial, export))) case Protocol.Loading_Theory(node_name, id) => val blobs_info = build_blobs_info(node_name) try { global_state.change(_.begin_theory(node_name, id, msg.text, blobs_info)) } catch { case _: Document.State.Fail => bad_output() } case List(Markup.Commands_Accepted.PROPERTY) => msg.text match { case Protocol.Commands_Accepted(ids) => ids.foreach(id => change_command(_.accumulate(id, Protocol.Commands_Accepted.message, cache))) case _ => bad_output() } case List(Markup.Assign_Update.PROPERTY) => msg.text match { case Protocol.Assign_Update(id, edited, update) => try { val (edited_nodes, cmds) = global_state.change_result(_.assign(id, edited, update)) change_buffer.invoke(true, edited_nodes, cmds) manager.send(Session.Change_Flush) } catch { case _: Document.State.Fail => bad_output() } case _ => bad_output() } delay_prune.invoke() case List(Markup.Removed_Versions.PROPERTY) => msg.text match { case Protocol.Removed(removed) => try { global_state.change(_.removed_versions(removed)) manager.send(Session.Change_Flush) } catch { case _: Document.State.Fail => bad_output() } case _ => bad_output() } case _ => bad_output() } } case _ => output.properties match { case Position.Id(state_id) => change_command(_.accumulate(state_id, output.message, cache)) case _ if output.is_init => val init_ok = try { Isabelle_System.make_services(classOf[Session.Protocol_Handler]) .foreach(init_protocol_handler) true } catch { case exn: Throwable => prover.get.protocol_command("Prover.stop", "1", Exn.message(exn)) false } if (init_ok) { prover.get.options(prover_options(session_options)) prover.get.init_session(resources) phase = Session.Ready debugger.ready() } case Markup.Process_Result(result) if output.is_exit => if (prover.defined) protocol_handlers.exit() for (id <- global_state.value.theories.keys) { val snapshot = global_state.change_result(_.end_theory(id)) finished_theories.post(snapshot) } file_formats.stop_session phase = Session.Terminated(result) prover.reset case _ => raw_output_messages.post(output) } } } //}}} /* main thread */ Consumer_Thread.fork[Any]("Session.manager", daemon = true) { case arg: Any => //{{{ arg match { case output: Prover.Output => if (output.is_syslog) { syslog += output.message syslog_messages.post(output) } if (output.is_stdout || output.is_stderr) raw_output_messages.post(output) else handle_output(output) all_messages.post(output) case input: Prover.Input => all_messages.post(input) case Start(start_prover) if !prover.defined => prover.set(start_prover(manager.send(_))) case Stop => consolidation.exit() delay_prune.revoke() if (prover.defined) { global_state.change(_ => Document.State.init) prover.get.terminate() } case Get_State(promise) => promise.fulfill(global_state.value) case Consolidate_Execution => if (prover.defined) { val state = global_state.value state.stable_tip_version match { case None => consolidation.update() case Some(version) => val consolidate = consolidation.flush().iterator.filter(name => !resources.session_base.loaded_theory(name) && !state.node_consolidated(version, name) && state.node_maybe_consolidated(version, name)).toList if (consolidate.nonEmpty) handle_raw_edits(consolidate = consolidate) } } case Prune_History => if (prover.defined) { val old_versions = global_state.change_result(_.remove_versions(prune_size)) if (old_versions.nonEmpty) prover.get.remove_versions(old_versions) } case Update_Options(options) => if (prover.defined && is_ready) { prover.get.options(prover_options(options)) handle_raw_edits() } global_options.post(Session.Global_Options(options)) case Cancel_Exec(exec_id) if prover.defined => prover.get.cancel_exec(exec_id) case Session.Raw_Edits(doc_blobs, edits) if prover.defined => handle_raw_edits(doc_blobs = doc_blobs, edits = edits) case Session.Dialog_Result(id, serial, result) if prover.defined => prover.get.dialog_result(serial, result) handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result))) - case Protocol_Command(name, args) if prover.defined => + case Protocol_Command_Raw(name, args) if prover.defined => + prover.get.protocol_command_raw(name, args) + + case Protocol_Command_Args(name, args) if prover.defined => prover.get.protocol_command_args(name, args) case change: Session.Change if prover.defined => val state = global_state.value if (!state.removing_versions && state.is_assigned(change.previous)) handle_change(change) else postponed_changes.store(change) case Session.Change_Flush if prover.defined => val state = global_state.value if (!state.removing_versions) postponed_changes.flush(state).foreach(handle_change) case bad => if (verbose) Output.warning("Ignoring bad message: " + bad.toString) } true //}}} } } /* main operations */ def get_state(): Document.State = { if (manager.is_active) { val promise = Future.promise[Document.State] manager.send_wait(Get_State(promise)) promise.join } else Document.State.init } def snapshot(name: Document.Node.Name = Document.Node.Name.empty, pending_edits: List[Text.Edit] = Nil): Document.Snapshot = get_state().snapshot(name, pending_edits) def recent_syntax(name: Document.Node.Name): Outer_Syntax = get_state().recent_finished.version.get_finished.nodes(name).syntax getOrElse resources.session_base.overall_syntax @tailrec final def await_stable_snapshot(): Document.Snapshot = { val snapshot = this.snapshot() if (snapshot.is_outdated) { output_delay.sleep await_stable_snapshot() } else snapshot } def start(start_prover: Prover.Receiver => Prover): Unit = { file_formats _phase.change( { case Session.Inactive => manager.send(Start(start_prover)) post_phase(Session.Startup) case phase => error("Cannot start prover in phase " + quote(phase.print)) }) } def stop(): Process_Result = { val was_ready = _phase.guarded_access( { case Session.Startup | Session.Shutdown => None case Session.Terminated(_) => Some((false, phase)) case Session.Inactive => Some((false, post_phase(Session.Terminated(Process_Result(0))))) case Session.Ready => Some((true, post_phase(Session.Shutdown))) }) if (was_ready) manager.send(Stop) prover.await_reset() change_parser.shutdown() change_buffer.shutdown() manager.shutdown() dispatcher.shutdown() phase match { case Session.Terminated(result) => result case phase => error("Bad session phase after shutdown: " + quote(phase.print)) } } + def protocol_command_raw(name: String, args: List[Bytes]): Unit = + manager.send(Protocol_Command_Raw(name, args)) + + def protocol_command_args(name: String, args: List[String]): Unit = + manager.send(Protocol_Command_Args(name, args)) + def protocol_command(name: String, args: String*): Unit = - manager.send(Protocol_Command(name, args.toList)) + protocol_command_args(name, args.toList) def cancel_exec(exec_id: Document_ID.Exec): Unit = manager.send(Cancel_Exec(exec_id)) def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]): Unit = if (edits.nonEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits)) def update_options(options: Options): Unit = manager.send_wait(Update_Options(options)) def dialog_result(id: Document_ID.Generic, serial: Long, result: String): Unit = manager.send(Session.Dialog_Result(id, serial, result)) } diff --git a/src/Pure/System/bash.scala b/src/Pure/System/bash.scala --- a/src/Pure/System/bash.scala +++ b/src/Pure/System/bash.scala @@ -1,235 +1,234 @@ /* Title: Pure/System/bash.scala Author: Makarius GNU bash processes, with propagation of interrupts. */ package isabelle import java.io.{File => JFile, BufferedReader, InputStreamReader, BufferedWriter, OutputStreamWriter} import scala.annotation.tailrec object Bash { /* concrete syntax */ private def bash_chr(c: Byte): String = { val ch = c.toChar ch match { case '\t' => "$'\\t'" case '\n' => "$'\\n'" case '\f' => "$'\\f'" case '\r' => "$'\\r'" case _ => if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "+,-./:_".contains(ch)) Symbol.ascii(ch) else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'" else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'" else if (c < 32 || c >= 127) "$'\\x" + Integer.toHexString(c) + "'" else "\\" + ch } } def string(s: String): String = if (s == "") "\"\"" else UTF8.bytes(s).iterator.map(bash_chr).mkString def strings(ss: List[String]): String = ss.iterator.map(Bash.string).mkString(" ") /* process and result */ type Watchdog = (Time, Process => Boolean) def process(script: String, cwd: JFile = null, env: Map[String, String] = Isabelle_System.settings(), redirect: Boolean = false, cleanup: () => Unit = () => ()): Process = new Process(script, cwd, env, redirect, cleanup) class Process private[Bash]( script: String, cwd: JFile, env: Map[String, String], redirect: Boolean, cleanup: () => Unit) { private val timing_file = Isabelle_System.tmp_file("bash_timing") private val timing = Synchronized[Option[Timing]](None) def get_timing: Timing = timing.value getOrElse Timing.zero private val script_file = Isabelle_System.tmp_file("bash_script") File.write(script_file, script) private val proc = Isabelle_System.process( List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-", File.standard_path(timing_file), "bash", File.standard_path(script_file)), cwd = cwd, env = env, redirect = redirect) // channels val stdin: BufferedWriter = new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset)) val stdout: BufferedReader = new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset)) val stderr: BufferedReader = new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset)) // signals private val pid = stdout.readLine @tailrec private def kill(signal: String, count: Int = 1): Boolean = { count <= 0 || { Isabelle_System.kill(signal, pid) val running = Isabelle_System.kill("0", pid)._2 == 0 if (running) { Time.seconds(0.1).sleep kill(signal, count - 1) } else false } } def terminate(): Unit = Isabelle_Thread.try_uninterruptible { kill("INT", count = 7) && kill("TERM", count = 3) && kill("KILL") proc.destroy() do_cleanup() } def interrupt(): Unit = Isabelle_Thread.try_uninterruptible { Isabelle_System.kill("INT", pid) } // JVM shutdown hook private val shutdown_hook = Isabelle_Thread.create(() => terminate()) try { Runtime.getRuntime.addShutdownHook(shutdown_hook) } catch { case _: IllegalStateException => } // cleanup private def do_cleanup(): Unit = { try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) } catch { case _: IllegalStateException => } script_file.delete timing.change { case None => if (timing_file.isFile) { val t = Word.explode(File.read(timing_file)) match { case List(Value.Long(elapsed), Value.Long(cpu)) => Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero) case _ => Timing.zero } timing_file.delete Some(t) } else Some(Timing.zero) case some => some } cleanup() } // join def join: Int = { val rc = proc.waitFor do_cleanup() rc } // result def result( progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), watchdog: Option[Watchdog] = None, strict: Boolean = true): Process_Result = { stdin.close() val out_lines = Future.thread("bash_stdout") { File.read_lines(stdout, progress_stdout) } val err_lines = Future.thread("bash_stderr") { File.read_lines(stderr, progress_stderr) } val watchdog_thread = for ((time, check) <- watchdog) yield { Future.thread("bash_watchdog") { while (proc.isAlive) { time.sleep if (check(this)) interrupt() } } } val rc = try { join } catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code } watchdog_thread.foreach(_.cancel()) if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt() Process_Result(rc, out_lines.join, err_lines.join, get_timing) } } /* Scala function */ - object Process extends Scala.Fun("bash_process", thread = true) + object Process extends Scala.Fun_Strings("bash_process", thread = true) { val here = Scala_Project.here - def apply(script: String): String = + def apply(args: List[String]): List[String] = { - val result = Exn.capture { Isabelle_System.bash(script) } + val result = Exn.capture { Isabelle_System.bash(cat_lines(args)) } val is_interrupt = result match { case Exn.Res(res) => res.rc == Exn.Interrupt.return_code case Exn.Exn(exn) => Exn.is_interrupt(exn) } result match { - case _ if is_interrupt => "" - case Exn.Exn(exn) => Exn.message(exn) + case _ if is_interrupt => Nil + case Exn.Exn(exn) => List(Exn.message(exn)) case Exn.Res(res) => - Library.cat_strings0( - res.rc.toString :: - res.timing.elapsed.ms.toString :: - res.timing.cpu.ms.toString :: - res.out_lines.length.toString :: - res.out_lines ::: res.err_lines) + res.rc.toString :: + res.timing.elapsed.ms.toString :: + res.timing.cpu.ms.toString :: + res.out_lines.length.toString :: + res.out_lines ::: res.err_lines } } } } diff --git a/src/Pure/System/isabelle_system.ML b/src/Pure/System/isabelle_system.ML --- a/src/Pure/System/isabelle_system.ML +++ b/src/Pure/System/isabelle_system.ML @@ -1,139 +1,138 @@ (* Title: Pure/System/isabelle_system.ML Author: Makarius Isabelle system support. *) signature ISABELLE_SYSTEM = sig val bash_process: string -> Process_Result.T val bash_output: string -> string * int val bash: string -> int val bash_functions: unit -> string list val check_bash_function: Proof.context -> string * Position.T -> string val absolute_path: Path.T -> string val make_directory: Path.T -> Path.T val copy_dir: Path.T -> Path.T -> unit val copy_file: Path.T -> Path.T -> unit val copy_file_base: Path.T * Path.T -> Path.T -> unit val create_tmp_path: string -> string -> Path.T val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a val rm_tree: Path.T -> unit val with_tmp_dir: string -> (Path.T -> 'a) -> 'a val download: string -> Path.T -> unit val isabelle_id: unit -> string val isabelle_identifier: unit -> string option val isabelle_heading: unit -> string val isabelle_name: unit -> string val identification: unit -> string end; structure Isabelle_System: ISABELLE_SYSTEM = struct (* bash *) fun bash_process script = Scala.function "bash_process" - ("export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP") ^ "\n" ^ script) - |> split_strings0 + ["export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP"), script] |> (fn [] => raise Exn.Interrupt | [err] => error err | a :: b :: c :: d :: lines => let val rc = Value.parse_int a; val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c); val (out_lines, err_lines) = chop (Value.parse_int d) lines; in Process_Result.make {rc = rc, out_lines = out_lines, err_lines = err_lines, timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}} end | _ => raise Fail "Malformed Isabelle/Scala result"); val bash = bash_process #> Process_Result.print #> Process_Result.rc; fun bash_output s = let val res = bash_process s; val _ = warning (Process_Result.err res); in (Process_Result.out res, Process_Result.rc res) end; (* bash functions *) fun bash_functions () = bash_process "declare -Fx" |> Process_Result.check |> Process_Result.out_lines |> map_filter (space_explode " " #> try List.last); fun check_bash_function ctxt arg = Completion.check_entity Markup.bash_functionN (bash_functions () |> map (rpair Position.none)) ctxt arg; (* directory and file operations *) val absolute_path = Path.implode o File.absolute_path; -fun scala_function0 name = ignore o Scala.function name o cat_strings0; +fun scala_function0 name = ignore o Scala.function1 name o cat_strings0; fun scala_function name = scala_function0 name o map absolute_path; fun make_directory path = (scala_function "make_directory" [path]; path); fun copy_dir src dst = scala_function "copy_dir" [src, dst]; fun copy_file src dst = scala_function "copy_file" [src, dst]; fun copy_file_base (base_dir, src) target_dir = scala_function0 "copy_file_base" [absolute_path base_dir, Path.implode src, absolute_path target_dir]; (* tmp files *) fun create_tmp_path name ext = let val path = File.tmp_path (Path.basic (name ^ serial_string ()) |> Path.ext ext); val _ = File.exists path andalso raise Fail ("Temporary file already exists: " ^ Path.print path); in path end; fun with_tmp_file name ext f = let val path = create_tmp_path name ext in Exn.release (Exn.capture f path before ignore (try File.rm path)) end; (* tmp dirs *) fun rm_tree path = scala_function "rm_tree" [path]; fun with_tmp_dir name f = let val path = create_tmp_path name "" in Exn.release (Exn.capture f (make_directory path) before ignore (try rm_tree path)) end; (* download file *) fun download url file = - ignore (Scala.function "download" (cat_strings0 [url, absolute_path file])); + ignore (Scala.function "download" [url, absolute_path file]); (* Isabelle distribution identification *) -fun isabelle_id () = Scala.function "isabelle_id" ""; +fun isabelle_id () = Scala.function1 "isabelle_id" ""; fun isabelle_identifier () = try getenv_strict "ISABELLE_IDENTIFIER"; fun isabelle_heading () = (case isabelle_identifier () of NONE => "" | SOME version => " (" ^ version ^ ")"); fun isabelle_name () = getenv_strict "ISABELLE_NAME"; fun identification () = "Isabelle/" ^ isabelle_id () ^ isabelle_heading (); end; diff --git a/src/Pure/System/isabelle_system.scala b/src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala +++ b/src/Pure/System/isabelle_system.scala @@ -1,615 +1,615 @@ /* Title: Pure/System/isabelle_system.scala Author: Makarius Fundamental Isabelle system environment: quasi-static module with optional init operation. */ package isabelle import java.io.{File => JFile, IOException} import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult, StandardCopyOption, FileSystemException} import java.nio.file.attribute.BasicFileAttributes object Isabelle_System { /** bootstrap information **/ def jdk_home(): String = { val java_home = System.getProperty("java.home", "") val home = new JFile(java_home) val parent = home.getParent if (home.getName == "jre" && parent != null && (new JFile(new JFile(parent, "bin"), "javac")).exists) parent else java_home } def bootstrap_directory( preference: String, envar: String, property: String, description: String): String = { val value = proper_string(preference) orElse // explicit argument proper_string(System.getenv(envar)) orElse // e.g. inherited from running isabelle tool proper_string(System.getProperty(property)) getOrElse // e.g. via JVM application boot process error("Unknown " + description + " directory") if ((new JFile(value)).isDirectory) value else error("Bad " + description + " directory " + quote(value)) } /** implicit settings environment **/ abstract class Service @volatile private var _settings: Option[Map[String, String]] = None @volatile private var _services: Option[List[Class[Service]]] = None def settings(): Map[String, String] = { if (_settings.isEmpty) init() // unsynchronized check _settings.get } def services(): List[Class[Service]] = { if (_services.isEmpty) init() // unsynchronized check _services.get } def make_services[C](c: Class[C]): List[C] = for { c1 <- services() if Library.is_subclass(c1, c) } yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C] def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized { if (_settings.isEmpty || _services.isEmpty) { val isabelle_root1 = bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root") val cygwin_root1 = if (Platform.is_windows) bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root") else "" if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1) def set_cygwin_root(): Unit = { if (Platform.is_windows) _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1)) } set_cygwin_root() def default(env: Map[String, String], entry: (String, String)): Map[String, String] = if (env.isDefinedAt(entry._1) || entry._2 == "") env else env + entry val env = { val temp_windows = { val temp = if (Platform.is_windows) System.getenv("TEMP") else null if (temp != null && temp.contains('\\')) temp else "" } val user_home = System.getProperty("user.home", "") val isabelle_app = System.getProperty("isabelle.app", "") default( default( default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())), "TEMP_WINDOWS" -> temp_windows), "HOME" -> user_home), "ISABELLE_APP" -> "true") } val settings = { val dump = JFile.createTempFile("settings", null) dump.deleteOnExit try { val cmd1 = if (Platform.is_windows) List(cygwin_root1 + "\\bin\\bash", "-l", File.standard_path(isabelle_root1 + "\\bin\\isabelle")) else List(isabelle_root1 + "/bin/isabelle") val cmd = cmd1 ::: List("getenv", "-d", dump.toString) val (output, rc) = process_output(process(cmd, env = env, redirect = true)) if (rc != 0) error(output) val entries = (for (entry <- Library.split_strings0(File.read(dump)) if entry != "") yield { val i = entry.indexOf('=') if (i <= 0) entry -> "" else entry.substring(0, i) -> entry.substring(i + 1) }).toMap entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM" } finally { dump.delete } } _settings = Some(settings) set_cygwin_root() val variable = "ISABELLE_SCALA_SERVICES" val services = for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable)))) yield { def err(msg: String): Nothing = error("Bad entry " + quote(name) + " in " + variable + "\n" + msg) try { Class.forName(name).asInstanceOf[Class[Service]] } catch { case _: ClassNotFoundException => err("Class not found") case exn: Throwable => err(Exn.message(exn)) } } _services = Some(services) } } /* getenv -- dynamic process environment */ private def getenv_error(name: String): Nothing = error("Undefined Isabelle environment variable: " + quote(name)) def getenv(name: String, env: Map[String, String] = settings()): String = env.getOrElse(name, "") def getenv_strict(name: String, env: Map[String, String] = settings()): String = proper_string(getenv(name, env)) getOrElse error("Undefined Isabelle environment variable: " + quote(name)) def cygwin_root(): String = getenv_strict("CYGWIN_ROOT") /* getetc -- static distribution parameters */ def getetc(name: String, root: Path = Path.ISABELLE_HOME): Option[String] = { val path = root + Path.basic("etc") + Path.basic(name) if (path.is_file) { Library.trim_split_lines(File.read(path)) match { case Nil => None case List(s) => Some(s) case _ => error("Single line expected in " + path.absolute) } } else None } /* Isabelle distribution identification */ def isabelle_id(root: Path = Path.ISABELLE_HOME): String = getetc("ISABELLE_ID", root = root) orElse Mercurial.archive_id(root) getOrElse { if (Mercurial.is_repository(root)) Mercurial.repository(root).parent() else error("Failed to identify Isabelle distribution " + root) } - object Isabelle_Id extends Scala.Fun("isabelle_id") + object Isabelle_Id extends Scala.Fun_String("isabelle_id") { val here = Scala_Project.here def apply(arg: String): String = isabelle_id() } def isabelle_tags(root: Path = Path.ISABELLE_HOME): String = getetc("ISABELLE_TAGS", root = root) orElse Mercurial.archive_tags(root) getOrElse { if (Mercurial.is_repository(root)) { val hg = Mercurial.repository(root) hg.tags(rev = hg.parent()) } else "" } def isabelle_identifier(): Option[String] = proper_string(getenv("ISABELLE_IDENTIFIER")) def isabelle_heading(): String = isabelle_identifier() match { case None => "" case Some(version) => " (" + version + ")" } def isabelle_name(): String = getenv_strict("ISABELLE_NAME") def identification(): String = "Isabelle/" + isabelle_id() + isabelle_heading() /** file-system operations **/ /* scala functions */ private def apply_paths(arg: String, fun: List[Path] => Unit): String = { fun(Library.split_strings0(arg).map(Path.explode)); "" } private def apply_paths1(arg: String, fun: Path => Unit): String = apply_paths(arg, { case List(path) => fun(path) }) private def apply_paths2(arg: String, fun: (Path, Path) => Unit): String = apply_paths(arg, { case List(path1, path2) => fun(path1, path2) }) private def apply_paths3(arg: String, fun: (Path, Path, Path) => Unit): String = apply_paths(arg, { case List(path1, path2, path3) => fun(path1, path2, path3) }) /* permissions */ def chmod(arg: String, path: Path): Unit = bash("chmod " + arg + " " + File.bash_path(path)).check def chown(arg: String, path: Path): Unit = bash("chown " + arg + " " + File.bash_path(path)).check /* directories */ def make_directory(path: Path): Path = { if (!path.is_dir) { try { Files.createDirectories(path.file.toPath) } catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) } } path } def new_directory(path: Path): Path = if (path.is_dir) error("Directory already exists: " + path.absolute) else make_directory(path) def copy_dir(dir1: Path, dir2: Path): Unit = { val res = bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)) if (!res.ok) { cat_error("Failed to copy directory " + dir1.absolute + " to " + dir2.absolute, res.err) } } - object Make_Directory extends Scala.Fun("make_directory") + object Make_Directory extends Scala.Fun_String("make_directory") { val here = Scala_Project.here def apply(arg: String): String = apply_paths1(arg, make_directory) } - object Copy_Dir extends Scala.Fun("copy_dir") + object Copy_Dir extends Scala.Fun_String("copy_dir") { val here = Scala_Project.here def apply(arg: String): String = apply_paths2(arg, copy_dir) } /* copy files */ def copy_file(src: JFile, dst: JFile): Unit = { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!File.eq(src, target)) { try { Files.copy(src.toPath, target.toPath, StandardCopyOption.COPY_ATTRIBUTES, StandardCopyOption.REPLACE_EXISTING) } catch { case ERROR(msg) => cat_error("Failed top copy file " + File.path(src).absolute + " to " + File.path(dst).absolute, msg) } } } def copy_file(src: Path, dst: Path): Unit = copy_file(src.file, dst.file) def copy_file_base(base_dir: Path, src: Path, target_dir: Path): Unit = { val src1 = src.expand val src1_dir = src1.dir if (!src1.starts_basic) error("Illegal path specification " + src1 + " beyond base directory") copy_file(base_dir + src1, Isabelle_System.make_directory(target_dir + src1_dir)) } - object Copy_File extends Scala.Fun("copy_file") + object Copy_File extends Scala.Fun_String("copy_file") { val here = Scala_Project.here def apply(arg: String): String = apply_paths2(arg, copy_file) } - object Copy_File_Base extends Scala.Fun("copy_file_base") + object Copy_File_Base extends Scala.Fun_String("copy_file_base") { val here = Scala_Project.here def apply(arg: String): String = apply_paths3(arg, copy_file_base) } /* move files */ def move_file(src: JFile, dst: JFile): Unit = { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!File.eq(src, target)) Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING) } def move_file(src: Path, dst: Path): Unit = move_file(src.file, dst.file) /* symbolic link */ def symlink(src: Path, dst: Path, force: Boolean = false): Unit = { val src_file = src.file val dst_file = dst.file val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file if (force) target.delete try { Files.createSymbolicLink(target.toPath, src_file.toPath) } catch { case _: UnsupportedOperationException if Platform.is_windows => Cygwin.link(File.standard_path(src), target) case _: FileSystemException if Platform.is_windows => Cygwin.link(File.standard_path(src), target) } } /* tmp files */ def isabelle_tmp_prefix(): JFile = { val path = Path.explode("$ISABELLE_TMP_PREFIX") path.file.mkdirs // low-level mkdirs to avoid recursion via Isabelle environment File.platform_file(path) } def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile = { val suffix = if (ext == "") "" else "." + ext val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile file.deleteOnExit file } def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A = { val file = tmp_file(name, ext) try { body(File.path(file)) } finally { file.delete } } /* tmp dirs */ def rm_tree(root: JFile): Unit = { root.delete if (root.isDirectory) { Files.walkFileTree(root.toPath, new SimpleFileVisitor[JPath] { override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult = { try { Files.deleteIfExists(file) } catch { case _: IOException => } FileVisitResult.CONTINUE } override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult = { if (e == null) { try { Files.deleteIfExists(dir) } catch { case _: IOException => } FileVisitResult.CONTINUE } else throw e } } ) } } def rm_tree(root: Path): Unit = rm_tree(root.file) - object Rm_Tree extends Scala.Fun("rm_tree") + object Rm_Tree extends Scala.Fun_String("rm_tree") { val here = Scala_Project.here def apply(arg: String): String = apply_paths1(arg, rm_tree) } def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile = { val dir = Files.createTempDirectory(base_dir.toPath, name).toFile dir.deleteOnExit dir } def with_tmp_dir[A](name: String)(body: Path => A): A = { val dir = tmp_dir(name) try { body(File.path(dir)) } finally { rm_tree(dir) } } /* quasi-atomic update of directory */ def update_directory(dir: Path, f: Path => Unit): Unit = { val new_dir = dir.ext("new") val old_dir = dir.ext("old") rm_tree(new_dir) rm_tree(old_dir) f(new_dir) if (dir.is_dir) move_file(dir, old_dir) move_file(new_dir, dir) rm_tree(old_dir) } /** external processes **/ /* raw process */ def process(command_line: List[String], cwd: JFile = null, env: Map[String, String] = settings(), redirect: Boolean = false): Process = { val proc = new ProcessBuilder proc.command(command_line:_*) // fragile on Windows if (cwd != null) proc.directory(cwd) if (env != null) { proc.environment.clear() for ((x, y) <- env) proc.environment.put(x, y) } proc.redirectErrorStream(redirect) proc.start } def process_output(proc: Process): (String, Int) = { proc.getOutputStream.close() val output = File.read_stream(proc.getInputStream) val rc = try { proc.waitFor } finally { proc.getInputStream.close() proc.getErrorStream.close() proc.destroy() Exn.Interrupt.dispose() } (output, rc) } def kill(signal: String, group_pid: String): (String, Int) = { val bash = if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe") else List("/usr/bin/env", "bash") process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid))) } /* GNU bash */ def bash(script: String, cwd: JFile = null, env: Map[String, String] = settings(), redirect: Boolean = false, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), watchdog: Option[Bash.Watchdog] = None, strict: Boolean = true, cleanup: () => Unit = () => ()): Process_Result = { Bash.process(script, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup). result(progress_stdout = progress_stdout, progress_stderr = progress_stderr, watchdog = watchdog, strict = strict) } private lazy val gnutar_check: Boolean = try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") } catch { case ERROR(_) => false } def gnutar( args: String, dir: Path = Path.current, original_owner: Boolean = false, redirect: Boolean = false): Process_Result = { val options = (if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") + (if (original_owner) "" else "--owner=root --group=staff ") if (gnutar_check) bash("tar " + options + args, redirect = redirect) else error("Expected to find GNU tar executable") } def require_command(cmds: String*): Unit = { for (cmd <- cmds) { if (!bash(Bash.string(cmd) + " --version").ok) error("Missing system command: " + quote(cmd)) } } def hostname(): String = bash("hostname -s").check.out def open(arg: String): Unit = bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &") def pdf_viewer(arg: Path): Unit = bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &") def open_external_file(name: String): Boolean = { val ext = Library.take_suffix((c: Char) => c != '.', name.toList)._2.mkString val external = ext.nonEmpty && Library.space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext) if (external) { if (ext == "pdf" && Path.is_wellformed(name)) pdf_viewer(Path.explode(name)) else open(name) } external } def export_isabelle_identifier(isabelle_identifier: String): String = if (isabelle_identifier == "") "" else "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n" /** Isabelle resources **/ /* repository clone with Admin */ def admin(): Boolean = Path.explode("~~/Admin").is_dir /* components */ def components(): List[Path] = Path.split(getenv_strict("ISABELLE_COMPONENTS")) /* default logic */ def default_logic(args: String*): String = { args.find(_ != "") match { case Some(logic) => logic case None => getenv_strict("ISABELLE_LOGIC") } } /* download file */ def download(url_name: String, file: Path, progress: Progress = new Progress): Unit = { val url = Url(url_name) progress.echo("Getting " + quote(url_name)) val content = try { HTTP.Client.get(url) } catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) } Bytes.write(file, content.bytes) } - object Download extends Scala.Fun("download", thread = true) + object Download extends Scala.Fun_Strings("download", thread = true) { val here = Scala_Project.here - def apply(arg: String): String = - Library.split_strings0(arg) match { - case List(url, file) => download(url, Path.explode(file)); "" + override def apply(args: List[String]): List[String] = + args match { + case List(url, file) => download(url, Path.explode(file)); Nil } } } diff --git a/src/Pure/System/isabelle_tool.scala b/src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala +++ b/src/Pure/System/isabelle_tool.scala @@ -1,233 +1,233 @@ /* Title: Pure/System/isabelle_tool.scala Author: Makarius Author: Lars Hupel Isabelle system tools: external executables or internal Scala functions. */ package isabelle import java.net.URLClassLoader import scala.reflect.runtime.universe import scala.tools.reflect.{ToolBox, ToolBoxError} object Isabelle_Tool { /* Scala source tools */ abstract class Body extends Function[List[String], Unit] private def compile(path: Path): Body = { def err(msg: String): Nothing = cat_error(msg, "The error(s) above occurred in Isabelle/Scala tool " + path) val source = File.read(path) val class_loader = new URLClassLoader(Array(), getClass.getClassLoader) val tool_box = universe.runtimeMirror(class_loader).mkToolBox() try { val tree = tool_box.parse(source) val module = try { tree.asInstanceOf[universe.ModuleDef] } catch { case _: java.lang.ClassCastException => err("Source does not describe a module (Scala object)") } tool_box.compile(universe.Ident(tool_box.define(module)))() match { case body: Body => body case _ => err("Ill-typed source: Isabelle_Tool.Body expected") } } catch { case e: ToolBoxError => if (tool_box.frontEnd.hasErrors) { val infos = tool_box.frontEnd.infos.toList val msgs = infos.map(info => "Error in line " + info.pos.line + ":\n" + info.msg) err(msgs.mkString("\n")) } else err(e.toString) } } /* external tools */ private def dirs(): List[Path] = Path.split(Isabelle_System.getenv_strict("ISABELLE_TOOLS")) private def is_external(dir: Path, file_name: String): Boolean = { val file = (dir + Path.explode(file_name)).file try { file.isFile && file.canRead && (file_name.endsWith(".scala") || file.canExecute) && !file_name.endsWith("~") && !file_name.endsWith(".orig") } catch { case _: SecurityException => false } } private def find_external(name: String): Option[List[String] => Unit] = dirs().collectFirst({ case dir if is_external(dir, name + ".scala") => compile(dir + Path.explode(name + ".scala")) case dir if is_external(dir, name) => (args: List[String]) => { val tool = dir + Path.explode(name) val result = Isabelle_System.bash(File.bash_path(tool) + " " + Bash.strings(args)) sys.exit(result.print_stdout.rc) } }) /* internal tools */ private lazy val internal_tools: List[Isabelle_Tool] = Isabelle_System.make_services(classOf[Isabelle_Scala_Tools]).flatMap(_.tools) private def find_internal(name: String): Option[List[String] => Unit] = internal_tools.collectFirst({ case tool if tool.name == name => args => Command_Line.tool { tool.body(args) } }) /* list tools */ abstract class Entry { def name: String def position: Properties.T def description: String def print: String = description match { case "" => name case descr => name + " - " + descr } } sealed case class External(name: String, path: Path) extends Entry { def position: Properties.T = Position.File(path.absolute.implode) def description: String = { val Pattern = """.*\bDESCRIPTION: *(.*)""".r split_lines(File.read(path)).collectFirst({ case Pattern(s) => s }) getOrElse "" } } def external_tools(): List[External] = { for { dir <- dirs() if dir.is_dir file_name <- File.read_dir(dir) if is_external(dir, file_name) } yield { val path = dir + Path.explode(file_name) val name = Library.perhaps_unsuffix(".scala", file_name) External(name, path) } } def isabelle_tools(): List[Entry] = (external_tools() ::: internal_tools).sortBy(_.name) - object Isabelle_Tools extends Scala.Fun("isabelle_tools") + object Isabelle_Tools extends Scala.Fun_String("isabelle_tools") { val here = Scala_Project.here def apply(arg: String): String = if (arg.nonEmpty) error("Bad argument: " + quote(arg)) else { val result = isabelle_tools().map(entry => (entry.name, entry.position)) val body = { import XML.Encode._; list(pair(string, properties))(result) } YXML.string_of_body(body) } } /* command line entry point */ def main(args: Array[String]): Unit = { Command_Line.tool { args.toList match { case Nil | List("-?") => val tool_descriptions = isabelle_tools().map(_.print) Getopts(""" Usage: isabelle TOOL [ARGS ...] Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help. Available tools:""" + tool_descriptions.mkString("\n ", "\n ", "\n")).usage() case tool_name :: tool_args => find_external(tool_name) orElse find_internal(tool_name) match { case Some(tool) => tool(tool_args) case None => error("Unknown Isabelle tool: " + quote(tool_name)) } } } } } sealed case class Isabelle_Tool( name: String, description: String, here: Scala_Project.Here, body: List[String] => Unit) extends Isabelle_Tool.Entry { def position: Position.T = here.position } class Isabelle_Scala_Tools(val tools: Isabelle_Tool*) extends Isabelle_System.Service class Tools extends Isabelle_Scala_Tools( Build.isabelle_tool, Build_Docker.isabelle_tool, Build_Job.isabelle_tool, Doc.isabelle_tool, Dump.isabelle_tool, Export.isabelle_tool, ML_Process.isabelle_tool, Mercurial.isabelle_tool, Mkroot.isabelle_tool, Logo.isabelle_tool, Options.isabelle_tool, Phabricator.isabelle_tool1, Phabricator.isabelle_tool2, Phabricator.isabelle_tool3, Phabricator.isabelle_tool4, Presentation.isabelle_tool, Profiling_Report.isabelle_tool, Server.isabelle_tool, Sessions.isabelle_tool, Scala_Project.isabelle_tool, Update.isabelle_tool, Update_Cartouches.isabelle_tool, Update_Comments.isabelle_tool, Update_Header.isabelle_tool, Update_Then.isabelle_tool, Update_Theorems.isabelle_tool, isabelle.vscode.TextMate_Grammar.isabelle_tool, isabelle.vscode.Language_Server.isabelle_tool) class Admin_Tools extends Isabelle_Scala_Tools( Build_CSDP.isabelle_tool, Build_Cygwin.isabelle_tool, Build_Doc.isabelle_tool, Build_E.isabelle_tool, Build_Fonts.isabelle_tool, Build_JCEF.isabelle_tool, Build_JDK.isabelle_tool, Build_PolyML.isabelle_tool1, Build_PolyML.isabelle_tool2, Build_SPASS.isabelle_tool, Build_SQLite.isabelle_tool, Build_Status.isabelle_tool, Build_Vampire.isabelle_tool, Build_VeriT.isabelle_tool, Build_Zipperposition.isabelle_tool, Check_Sources.isabelle_tool, Components.isabelle_tool, isabelle.vscode.Build_VSCode.isabelle_tool) diff --git a/src/Pure/System/scala.ML b/src/Pure/System/scala.ML --- a/src/Pure/System/scala.ML +++ b/src/Pure/System/scala.ML @@ -1,66 +1,69 @@ (* Title: Pure/System/scala.ML Author: Makarius Invoke Scala functions from the ML runtime. *) signature SCALA = sig exception Null - val function: string -> string -> string + val function: string -> string list -> string list + val function1: string -> string -> string end; structure Scala: SCALA = struct exception Null; local val new_id = string_of_int o Counter.make (); val results = - Synchronized.var "Scala.results" (Symtab.empty: string Exn.result Symtab.table); + Synchronized.var "Scala.results" (Symtab.empty: string list Exn.result Symtab.table); val _ = Protocol_Command.define "Scala.result" - (fn [id, tag, res] => + (fn id :: args => let val result = - (case tag of - "0" => Exn.Exn Null - | "1" => Exn.Res res - | "2" => Exn.Exn (ERROR res) - | "3" => Exn.Exn (Fail res) - | "4" => Exn.Exn Exn.Interrupt - | _ => raise Fail ("Bad tag: " ^ tag)); + (case args of + ["0"] => Exn.Exn Null + | "1" :: rest => Exn.Res rest + | ["2", msg] => Exn.Exn (ERROR msg) + | ["3", msg] => Exn.Exn (Fail msg) + | ["4"] => Exn.Exn Exn.Interrupt + | _ => raise Fail "Malformed Scala.result"); in Synchronized.change results (Symtab.map_entry id (K result)) end); in -fun function name arg = +fun function name args = Thread_Attributes.uninterruptible (fn restore_attributes => fn () => let val id = new_id (); fun invoke () = (Synchronized.change results (Symtab.update (id, Exn.Exn Match)); - Output.protocol_message (Markup.invoke_scala name id) [[XML.Text arg]]); + Output.protocol_message (Markup.invoke_scala name id) (map (single o XML.Text) args)); fun cancel () = (Synchronized.change results (Symtab.delete_safe id); Output.protocol_message (Markup.cancel_scala id) []); fun await_result () = Synchronized.guarded_access results (fn tab => (case Symtab.lookup tab id of SOME (Exn.Exn Match) => NONE | SOME result => SOME (result, Symtab.delete id tab) | NONE => SOME (Exn.Exn Exn.Interrupt, tab))); in invoke (); Exn.release (restore_attributes await_result ()) handle exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn) end) (); +val function1 = singleton o function; + end; 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,265 +1,285 @@ /* 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) - extends Function[String, String] { override def toString: String = name + def multi: Boolean = true def position: Properties.T = here.position def here: Scala_Project.Here + def invoke(args: List[Bytes]): List[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 + override def apply(args: List[String]): List[String] = + args match { + case List(arg) => List(apply(arg)) + case _ => error("Expected single argument for Scala function " + quote(name)) + } def apply(arg: String): String } 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("echo") + object Echo extends Fun_String("echo") { val here = Scala_Project.here def apply(arg: String): String = arg } - object Sleep extends Fun("sleep") + 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 **/ object Compiler { def context( error: String => Unit = Exn.error, jar_dirs: List[JFile] = Nil): Context = { def find_jars(dir: JFile): List[String] = File.find_files(dir, file => file.getName.endsWith(".jar")). map(File.absolute_name) val class_path = for { prop <- List("isabelle.scala.classpath", "java.class.path") path = System.getProperty(prop, "") if path != "\"\"" elem <- space_explode(JFile.pathSeparatorChar, path) } yield elem val settings = new GenericRunnerSettings(error) settings.classpath.value = (class_path ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator) new Context(settings) } def default_print_writer: PrintWriter = new NewLinePrintWriter(new ConsoleWriter, true) class Context private [Compiler](val settings: GenericRunnerSettings) { override def toString: String = settings.toString def interpreter( print_writer: PrintWriter = default_print_writer, class_loader: ClassLoader = null): IMain = { new IMain(settings, new ReplReporterImpl(settings, print_writer)) { override def parentClassLoader: ClassLoader = if (class_loader == null) super.parentClassLoader else class_loader } } def toplevel(interpret: Boolean, source: String): List[String] = { val out = new StringWriter val interp = interpreter(new PrintWriter(out)) 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("scala_toplevel") + 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.context().toplevel(interpret, source) } catch { case ERROR(msg) => List(msg) } locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) } } } /** 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, arg: String): (Tag.Value, String) = + 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(arg) } match { - case Exn.Res(null) => (Tag.NULL, "") + 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, "") - case Exn.Exn(e) => (Tag.ERROR, Exn.message(e)) + case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, Nil) + case Exn.Exn(e) => (Tag.ERROR, List(Bytes(Exn.message(e)))) } - case None => (Tag.FAIL, "Unknown Isabelle/Scala function: " + quote(name)) + 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: String): Unit = + private def result(id: String, tag: Scala.Tag.Value, res: List[Bytes]): Unit = synchronized { if (futures.isDefinedAt(id)) { - session.protocol_command("Scala.result", id, tag.id.toString, res) + 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, "") + 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.text) + 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 = 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, Doc.Doc_Names, Bash.Process, 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/Thy/bibtex.scala b/src/Pure/Thy/bibtex.scala --- a/src/Pure/Thy/bibtex.scala +++ b/src/Pure/Thy/bibtex.scala @@ -1,704 +1,704 @@ /* Title: Pure/Thy/bibtex.scala Author: Makarius BibTeX support. */ package isabelle import java.io.{File => JFile} import scala.collection.mutable import scala.util.parsing.combinator.RegexParsers import scala.util.parsing.input.Reader object Bibtex { /** file format **/ def is_bibtex(name: String): Boolean = name.endsWith(".bib") class File_Format extends isabelle.File_Format { val format_name: String = "bibtex" val file_ext: String = "bib" override def theory_suffix: String = "bibtex_file" override def theory_content(name: String): String = """theory "bib" imports Pure begin bibtex_file """ + Outer_Syntax.quote_string(name) + """ end""" override def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] = { val name = snapshot.node_name if (detect(name.node)) { val title = "Bibliography " + quote(snapshot.node_name.path.file_name) val content = Isabelle_System.with_tmp_file("bib", "bib") { bib => File.write(bib, snapshot.node.source) Bibtex.html_output(List(bib), style = "unsort", title = title) } Some(Presentation.HTML_Document(title, content)) } else None } } /** bibtex errors **/ def bibtex_errors(dir: Path, root_name: String): List[String] = { val log_path = dir + Path.explode(root_name).ext("blg") if (log_path.is_file) { val Error1 = """^(I couldn't open database file .+)$""".r val Error2 = """^(.+)---line (\d+) of file (.+)""".r Line.logical_lines(File.read(log_path)).flatMap(line => line match { case Error1(msg) => Some("Bibtex error: " + msg) case Error2(msg, Value.Int(l), file) => val path = File.standard_path(file) if (Path.is_wellformed(path)) { val pos = Position.Line_File(l, (dir + Path.explode(path)).canonical.implode) Some("Bibtex error" + Position.here(pos) + ":\n " + msg) } else None case _ => None }) } else Nil } /** check database **/ def check_database(database: String): (List[(String, Position.T)], List[(String, Position.T)]) = { val chunks = parse(Line.normalize(database)) var chunk_pos = Map.empty[String, Position.T] val tokens = new mutable.ListBuffer[(Token, Position.T)] var line = 1 var offset = 1 def make_pos(length: Int): Position.T = Position.Offset(offset) ::: Position.End_Offset(offset + length) ::: Position.Line(line) def advance_pos(tok: Token): Unit = { for (s <- Symbol.iterator(tok.source)) { if (Symbol.is_newline(s)) line += 1 offset += 1 } } def get_line_pos(l: Int): Position.T = if (0 < l && l <= tokens.length) tokens(l - 1)._2 else Position.none for (chunk <- chunks) { val name = chunk.name if (name != "" && !chunk_pos.isDefinedAt(name)) { chunk_pos += (name -> make_pos(chunk.heading_length)) } for (tok <- chunk.tokens) { tokens += (tok.copy(source = tok.source.replace("\n", " ")) -> make_pos(tok.source.length)) advance_pos(tok) } } Isabelle_System.with_tmp_dir("bibtex")(tmp_dir => { File.write(tmp_dir + Path.explode("root.bib"), tokens.iterator.map(p => p._1.source).mkString("", "\n", "\n")) File.write(tmp_dir + Path.explode("root.aux"), "\\bibstyle{plain}\n\\bibdata{root}\n\\citation{*}") Isabelle_System.bash("\"$ISABELLE_BIBTEX\" root", cwd = tmp_dir.file) val Error = """^(.*)---line (\d+) of file root.bib$""".r val Warning = """^Warning--(.+)$""".r val Warning_Line = """--line (\d+) of file root.bib$""".r val Warning_in_Chunk = """^Warning--(.+) in (.+)$""".r val log_file = tmp_dir + Path.explode("root.blg") val lines = if (log_file.is_file) Line.logical_lines(File.read(log_file)) else Nil val (errors, warnings) = if (lines.isEmpty) (Nil, Nil) else { lines.zip(lines.tail ::: List("")).flatMap( { case (Error(msg, Value.Int(l)), _) => Some((true, (msg, get_line_pos(l)))) case (Warning_in_Chunk(msg, name), _) if chunk_pos.isDefinedAt(name) => Some((false, (Word.capitalize(msg + " in entry " + quote(name)), chunk_pos(name)))) case (Warning(msg), Warning_Line(Value.Int(l))) => Some((false, (Word.capitalize(msg), get_line_pos(l)))) case (Warning(msg), _) => Some((false, (Word.capitalize(msg), Position.none))) case _ => None } ).partition(_._1) } (errors.map(_._2), warnings.map(_._2)) }) } - object Check_Database extends Scala.Fun("bibtex_check_database") + object Check_Database extends Scala.Fun_String("bibtex_check_database") { val here = Scala_Project.here def apply(database: String): String = { import XML.Encode._ YXML.string_of_body(pair(list(pair(string, properties)), list(pair(string, properties)))( check_database(database))) } } /** document model **/ /* entries */ def entries(text: String): List[Text.Info[String]] = { val result = new mutable.ListBuffer[Text.Info[String]] var offset = 0 for (chunk <- Bibtex.parse(text)) { val end_offset = offset + chunk.source.length if (chunk.name != "" && !chunk.is_command) result += Text.Info(Text.Range(offset, end_offset), chunk.name) offset = end_offset } result.toList } def entries_iterator[A, B <: Document.Model](models: Map[A, B]) : Iterator[Text.Info[(String, B)]] = { for { (_, model) <- models.iterator info <- model.bibtex_entries.iterator } yield info.map((_, model)) } /* completion */ def completion[A, B <: Document.Model]( history: Completion.History, rendering: Rendering, caret: Text.Offset, models: Map[A, B]): Option[Completion.Result] = { for { Text.Info(r, name) <- rendering.citations(rendering.before_caret_range(caret)).headOption name1 <- Completion.clean_name(name) original <- rendering.get_text(r) original1 <- Completion.clean_name(Library.perhaps_unquote(original)) entries = (for { Text.Info(_, (entry, _)) <- entries_iterator(models) if entry.toLowerCase.containsSlice(name1.toLowerCase) && entry != original1 } yield entry).toList if entries.nonEmpty items = entries.sorted.map({ case entry => val full_name = Long_Name.qualify(Markup.CITATION, entry) val description = List(entry, "(BibTeX entry)") val replacement = quote(entry) Completion.Item(r, original, full_name, description, replacement, 0, false) }).sorted(history.ordering).take(rendering.options.int("completion_limit")) } yield Completion.Result(r, original, false, items) } /** content **/ private val months = List( "jan", "feb", "mar", "apr", "may", "jun", "jul", "aug", "sep", "oct", "nov", "dec") def is_month(s: String): Boolean = months.contains(s.toLowerCase) private val commands = List("preamble", "string") def is_command(s: String): Boolean = commands.contains(s.toLowerCase) sealed case class Entry( kind: String, required: List[String], optional_crossref: List[String], optional_other: List[String]) { val optional_standard: List[String] = List("url", "doi", "ee") def is_required(s: String): Boolean = required.contains(s.toLowerCase) def is_optional(s: String): Boolean = optional_crossref.contains(s.toLowerCase) || optional_other.contains(s.toLowerCase) || optional_standard.contains(s.toLowerCase) def fields: List[String] = required ::: optional_crossref ::: optional_other ::: optional_standard def template: String = "@" + kind + "{,\n" + fields.map(x => " " + x + " = {},\n").mkString + "}\n" } val known_entries: List[Entry] = List( Entry("Article", List("author", "title"), List("journal", "year"), List("volume", "number", "pages", "month", "note")), Entry("InProceedings", List("author", "title"), List("booktitle", "year"), List("editor", "volume", "number", "series", "pages", "month", "address", "organization", "publisher", "note")), Entry("InCollection", List("author", "title", "booktitle"), List("publisher", "year"), List("editor", "volume", "number", "series", "type", "chapter", "pages", "edition", "month", "address", "note")), Entry("InBook", List("author", "editor", "title", "chapter"), List("publisher", "year"), List("volume", "number", "series", "type", "address", "edition", "month", "pages", "note")), Entry("Proceedings", List("title", "year"), List(), List("booktitle", "editor", "volume", "number", "series", "address", "month", "organization", "publisher", "note")), Entry("Book", List("author", "editor", "title"), List("publisher", "year"), List("volume", "number", "series", "address", "edition", "month", "note")), Entry("Booklet", List("title"), List(), List("author", "howpublished", "address", "month", "year", "note")), Entry("PhdThesis", List("author", "title", "school", "year"), List(), List("type", "address", "month", "note")), Entry("MastersThesis", List("author", "title", "school", "year"), List(), List("type", "address", "month", "note")), Entry("TechReport", List("author", "title", "institution", "year"), List(), List("type", "number", "address", "month", "note")), Entry("Manual", List("title"), List(), List("author", "organization", "address", "edition", "month", "year", "note")), Entry("Unpublished", List("author", "title", "note"), List(), List("month", "year")), Entry("Misc", List(), List(), List("author", "title", "howpublished", "month", "year", "note"))) def get_entry(kind: String): Option[Entry] = known_entries.find(entry => entry.kind.toLowerCase == kind.toLowerCase) def is_entry(kind: String): Boolean = get_entry(kind).isDefined /** tokens and chunks **/ object Token { object Kind extends Enumeration { val COMMAND = Value("command") val ENTRY = Value("entry") val KEYWORD = Value("keyword") val NAT = Value("natural number") val STRING = Value("string") val NAME = Value("name") val IDENT = Value("identifier") val SPACE = Value("white space") val COMMENT = Value("ignored text") val ERROR = Value("bad input") } } sealed case class Token(kind: Token.Kind.Value, source: String) { def is_kind: Boolean = kind == Token.Kind.COMMAND || kind == Token.Kind.ENTRY || kind == Token.Kind.IDENT def is_name: Boolean = kind == Token.Kind.NAME || kind == Token.Kind.IDENT def is_ignored: Boolean = kind == Token.Kind.SPACE || kind == Token.Kind.COMMENT def is_malformed: Boolean = kind == Token.Kind.ERROR def is_open: Boolean = kind == Token.Kind.KEYWORD && (source == "{" || source == "(") } case class Chunk(kind: String, tokens: List[Token]) { val source = tokens.map(_.source).mkString private val content: Option[List[Token]] = tokens match { case Token(Token.Kind.KEYWORD, "@") :: body if body.nonEmpty => (body.init.filterNot(_.is_ignored), body.last) match { case (tok :: Token(Token.Kind.KEYWORD, "{") :: toks, Token(Token.Kind.KEYWORD, "}")) if tok.is_kind => Some(toks) case (tok :: Token(Token.Kind.KEYWORD, "(") :: toks, Token(Token.Kind.KEYWORD, ")")) if tok.is_kind => Some(toks) case _ => None } case _ => None } def name: String = content match { case Some(tok :: _) if tok.is_name => tok.source case _ => "" } def heading_length: Int = if (name == "") 1 else { tokens.takeWhile(tok => !tok.is_open).foldLeft(0) { case (n, tok) => n + tok.source.length } } def is_ignored: Boolean = kind == "" && tokens.forall(_.is_ignored) def is_malformed: Boolean = kind == "" || tokens.exists(_.is_malformed) def is_command: Boolean = Bibtex.is_command(kind) && name != "" && content.isDefined def is_entry: Boolean = Bibtex.is_entry(kind) && name != "" && content.isDefined } /** parsing **/ // context of partial line-oriented scans abstract class Line_Context case object Ignored extends Line_Context case object At extends Line_Context case class Item_Start(kind: String) extends Line_Context case class Item_Open(kind: String, end: String) extends Line_Context case class Item(kind: String, end: String, delim: Delimited) extends Line_Context case class Delimited(quoted: Boolean, depth: Int) val Closed = Delimited(false, 0) private def token(kind: Token.Kind.Value)(source: String): Token = Token(kind, source) private def keyword(source: String): Token = Token(Token.Kind.KEYWORD, source) // See also https://ctan.org/tex-archive/biblio/bibtex/base/bibtex.web // module @. object Parsers extends RegexParsers { /* white space and comments */ override val whiteSpace = "".r private val space = """[ \t\n\r]+""".r ^^ token(Token.Kind.SPACE) private val spaces = rep(space) /* ignored text */ private val ignored: Parser[Chunk] = rep1("""(?i)([^@]+|@[ \t]*comment)""".r) ^^ { case ss => Chunk("", List(Token(Token.Kind.COMMENT, ss.mkString))) } private def ignored_line: Parser[(Chunk, Line_Context)] = ignored ^^ { case a => (a, Ignored) } /* delimited string: outermost "..." or {...} and body with balanced {...} */ // see also bibtex.web: scan_a_field_token_and_eat_white, scan_balanced_braces private def delimited_depth(delim: Delimited): Parser[(String, Delimited)] = new Parser[(String, Delimited)] { require(if (delim.quoted) delim.depth > 0 else delim.depth >= 0, "bad delimiter depth") def apply(in: Input) = { val start = in.offset val end = in.source.length var i = start var q = delim.quoted var d = delim.depth var finished = false while (!finished && i < end) { val c = in.source.charAt(i) if (c == '"' && d == 0) { i += 1; d = 1; q = true } else if (c == '"' && d == 1 && q) { i += 1; d = 0; q = false; finished = true } else if (c == '{') { i += 1; d += 1 } else if (c == '}') { if (d == 1 && !q || d > 1) { i += 1; d -= 1; if (d == 0) finished = true } else {i = start; finished = true } } else if (d > 0) i += 1 else finished = true } if (i == start) Failure("bad input", in) else { val s = in.source.subSequence(start, i).toString Success((s, Delimited(q, d)), in.drop(i - start)) } } }.named("delimited_depth") private def delimited: Parser[Token] = delimited_depth(Closed) ^? { case (s, delim) if delim == Closed => Token(Token.Kind.STRING, s) } private def recover_delimited: Parser[Token] = """["{][^@]*""".r ^^ token(Token.Kind.ERROR) def delimited_line(ctxt: Item): Parser[(Chunk, Line_Context)] = delimited_depth(ctxt.delim) ^^ { case (s, delim1) => (Chunk(ctxt.kind, List(Token(Token.Kind.STRING, s))), ctxt.copy(delim = delim1)) } | recover_delimited ^^ { case a => (Chunk(ctxt.kind, List(a)), Ignored) } /* other tokens */ private val at = "@" ^^ keyword private val nat = "[0-9]+".r ^^ token(Token.Kind.NAT) private val name = """[\x21-\x7f&&[^"#%'(),={}]]+""".r ^^ token(Token.Kind.NAME) private val identifier = """[\x21-\x7f&&[^"#%'(),={}0-9]][\x21-\x7f&&[^"#%'(),={}]]*""".r private val ident = identifier ^^ token(Token.Kind.IDENT) val other_token = "[=#,]".r ^^ keyword | (nat | (ident | space)) /* body */ private val body = delimited | (recover_delimited | other_token) private def body_line(ctxt: Item) = if (ctxt.delim.depth > 0) delimited_line(ctxt) else delimited_line(ctxt) | other_token ^^ { case a => (Chunk(ctxt.kind, List(a)), ctxt) } | ctxt.end ^^ { case a => (Chunk(ctxt.kind, List(keyword(a))), Ignored) } /* items: command or entry */ private val item_kind = identifier ^^ { case a => val kind = if (is_command(a)) Token.Kind.COMMAND else if (is_entry(a)) Token.Kind.ENTRY else Token.Kind.IDENT Token(kind, a) } private val item_begin = "{" ^^ { case a => ("}", keyword(a)) } | "(" ^^ { case a => (")", keyword(a)) } private def item_name(kind: String) = kind.toLowerCase match { case "preamble" => failure("") case "string" => identifier ^^ token(Token.Kind.NAME) case _ => name } private val item_start = at ~ spaces ~ item_kind ~ spaces ^^ { case a ~ b ~ c ~ d => (c.source, List(a) ::: b ::: List(c) ::: d) } private val item: Parser[Chunk] = (item_start ~ item_begin ~ spaces) into { case (kind, a) ~ ((end, b)) ~ c => opt(item_name(kind)) ~ rep(body) ~ opt(end ^^ keyword) ^^ { case d ~ e ~ f => Chunk(kind, a ::: List(b) ::: c ::: d.toList ::: e ::: f.toList) } } private val recover_item: Parser[Chunk] = at ~ "[^@]*".r ^^ { case a ~ b => Chunk("", List(a, Token(Token.Kind.ERROR, b))) } /* chunks */ val chunk: Parser[Chunk] = ignored | (item | recover_item) def chunk_line(ctxt: Line_Context): Parser[(Chunk, Line_Context)] = { ctxt match { case Ignored => ignored_line | at ^^ { case a => (Chunk("", List(a)), At) } case At => space ^^ { case a => (Chunk("", List(a)), ctxt) } | item_kind ^^ { case a => (Chunk(a.source, List(a)), Item_Start(a.source)) } | recover_item ^^ { case a => (a, Ignored) } | ignored_line case Item_Start(kind) => space ^^ { case a => (Chunk(kind, List(a)), ctxt) } | item_begin ^^ { case (end, a) => (Chunk(kind, List(a)), Item_Open(kind, end)) } | recover_item ^^ { case a => (a, Ignored) } | ignored_line case Item_Open(kind, end) => space ^^ { case a => (Chunk(kind, List(a)), ctxt) } | item_name(kind) ^^ { case a => (Chunk(kind, List(a)), Item(kind, end, Closed)) } | body_line(Item(kind, end, Closed)) | ignored_line case item_ctxt: Item => body_line(item_ctxt) | ignored_line case _ => failure("") } } } /* parse */ def parse(input: CharSequence): List[Chunk] = Parsers.parseAll(Parsers.rep(Parsers.chunk), Scan.char_reader(input)) match { case Parsers.Success(result, _) => result case _ => error("Unexpected failure to parse input:\n" + input.toString) } def parse_line(input: CharSequence, context: Line_Context): (List[Chunk], Line_Context) = { var in: Reader[Char] = Scan.char_reader(input) val chunks = new mutable.ListBuffer[Chunk] var ctxt = context while (!in.atEnd) { Parsers.parse(Parsers.chunk_line(ctxt), in) match { case Parsers.Success((x, c), rest) => chunks += x; ctxt = c; in = rest case Parsers.NoSuccess(_, rest) => error("Unepected failure to parse input:\n" + rest.source.toString) } } (chunks.toList, ctxt) } /** HTML output **/ private val output_styles = List( "" -> "html-n", "plain" -> "html-n", "alpha" -> "html-a", "named" -> "html-n", "paragraph" -> "html-n", "unsort" -> "html-u", "unsortlist" -> "html-u") def html_output(bib: List[Path], title: String = "Bibliography", body: Boolean = false, citations: List[String] = List("*"), style: String = "", chronological: Boolean = false): String = { Isabelle_System.with_tmp_dir("bibtex")(tmp_dir => { /* database files */ val bib_files = bib.map(_.drop_ext) val bib_names = { val names0 = bib_files.map(_.file_name) if (Library.duplicates(names0).isEmpty) names0 else names0.zipWithIndex.map({ case (name, i) => (i + 1).toString + "-" + name }) } for ((a, b) <- bib_files zip bib_names) { Isabelle_System.copy_file(a.ext("bib"), tmp_dir + Path.basic(b).ext("bib")) } /* style file */ val bst = output_styles.toMap.get(style) match { case Some(base) => base + (if (chronological) "c" else "") + ".bst" case None => error("Bad style for bibtex HTML output: " + quote(style) + "\n(expected: " + commas_quote(output_styles.map(_._1)) + ")") } Isabelle_System.copy_file(Path.explode("$BIB2XHTML_HOME/bst") + Path.explode(bst), tmp_dir) /* result */ val in_file = Path.explode("bib.aux") val out_file = Path.explode("bib.html") File.write(tmp_dir + in_file, bib_names.mkString("\\bibdata{", ",", "}\n") + citations.map(cite => "\\citation{" + cite + "}\n").mkString) Isabelle_System.bash( "\"$BIB2XHTML_HOME/main/bib2xhtml.pl\" -B \"$ISABELLE_BIBTEX\"" + " -u -s " + Bash.string(proper_string(style) getOrElse "empty") + (if (chronological) " -c" else "") + (if (title != "") " -h " + Bash.string(title) + " " else "") + " " + File.bash_path(in_file) + " " + File.bash_path(out_file), cwd = tmp_dir.file).check val html = File.read(tmp_dir + out_file) if (body) { cat_lines( split_lines(html). dropWhile(line => !line.startsWith("