diff --git a/src/Pure/ML/ml_console.scala b/src/Pure/ML/ml_console.scala --- a/src/Pure/ML/ml_console.scala +++ b/src/Pure/ML/ml_console.scala @@ -1,84 +1,84 @@ /* Title: Pure/ML/ml_console.scala Author: Makarius The raw ML process in interactive mode. */ package isabelle object ML_Console { /* command line entry point */ def main(args: Array[String]) { Command_Line.tool { var dirs: List[Path] = Nil var include_sessions: List[String] = Nil var logic = Isabelle_System.getenv("ISABELLE_LOGIC") var modes: List[String] = Nil var no_build = false var options = Options.init() var raw_ml_system = false val getopts = Getopts(""" Usage: isabelle console [OPTIONS] Options are: -d DIR include session directory -i NAME include session in name-space of theories -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) -m MODE add print mode for output -n no build of session image on startup -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -r bootstrap from raw Poly/ML Build a logic session image and run the raw Isabelle ML process in interactive mode, with line editor ISABELLE_LINE_EDITOR=""" + quote(Isabelle_System.getenv("ISABELLE_LINE_EDITOR")) + """. """, "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "i:" -> (arg => include_sessions = include_sessions ::: List(arg)), "l:" -> (arg => logic = arg), "m:" -> (arg => modes = arg :: modes), "n" -> (_ => no_build = true), "o:" -> (arg => options = options + arg), "r" -> (_ => raw_ml_system = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val sessions_structure = Sessions.load_structure(options, dirs = dirs) val store = Sessions.store(options) // build logic if (!no_build && !raw_ml_system) { val progress = new Console_Progress() val rc = progress.interrupt_handler { Build.build_logic(options, logic, build_heap = true, progress = progress, dirs = dirs) } if (rc != 0) sys.exit(rc) } // process loop val process = ML_Process(options, sessions_structure, store, logic = logic, args = List("-i"), redirect = true, modes = if (raw_ml_system) Nil else modes ::: List("ASCII"), raw_ml_system = raw_ml_system, session_base = if (raw_ml_system) None else Some(Sessions.base_info( - options, logic, dirs = dirs, include_sessions = include_sessions).check_base)) + options, logic, dirs = dirs, include_sessions = include_sessions).check.base)) POSIX_Interrupt.handler { process.interrupt } { new TTY_Loop(process.stdin, process.stdout).join val rc = process.join if (rc != 0) sys.exit(rc) } } } } diff --git a/src/Pure/PIDE/headless.scala b/src/Pure/PIDE/headless.scala --- a/src/Pure/PIDE/headless.scala +++ b/src/Pure/PIDE/headless.scala @@ -1,661 +1,661 @@ /* Title: Pure/PIDE/headless.scala Author: Makarius Headless PIDE session and resources from file-system. */ package isabelle import java.io.{File => JFile} import scala.annotation.tailrec import scala.collection.mutable object Headless { /** session **/ private def stable_snapshot( state: Document.State, version: Document.Version, name: Document.Node.Name): Document.Snapshot = { val snapshot = state.snapshot(name) assert(version.id == snapshot.version.id) snapshot } class Use_Theories_Result private[Headless]( val state: Document.State, val version: Document.Version, val nodes: List[(Document.Node.Name, Document_Status.Node_Status)], val nodes_committed: List[(Document.Node.Name, Document_Status.Node_Status)]) { def nodes_pending: List[(Document.Node.Name, Document_Status.Node_Status)] = { val committed = nodes_committed.iterator.map(_._1).toSet nodes.filter(p => !committed(p._1)) } def snapshot(name: Document.Node.Name): Document.Snapshot = stable_snapshot(state, version, name) def ok: Boolean = (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok }) } class Session private[Headless]( session_name: String, _session_options: => Options, override val resources: Resources) extends isabelle.Session(_session_options, resources) { session => private def loaded_theory(name: Document.Node.Name): Boolean = resources.session_base.loaded_theory(name.theory) /* options */ override def consolidate_delay: Time = session_options.seconds("headless_consolidate_delay") override def prune_delay: Time = session_options.seconds("headless_prune_delay") def default_check_delay: Time = session_options.seconds("headless_check_delay") def default_check_limit: Int = session_options.int("headless_check_limit") def default_nodes_status_delay: Time = session_options.seconds("headless_nodes_status_delay") def default_watchdog_timeout: Time = session_options.seconds("headless_watchdog_timeout") def default_commit_cleanup_delay: Time = session_options.seconds("headless_commit_cleanup_delay") /* temporary directory */ val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session") val tmp_dir_name: String = File.path(tmp_dir).implode def master_directory(master_dir: String): String = proper_string(master_dir) getOrElse tmp_dir_name override def toString: String = session_name override def stop(): Process_Result = { try { super.stop() } finally { Isabelle_System.rm_tree(tmp_dir) } } /* theories */ private object Load_State { def finished: Load_State = Load_State(Nil, Nil, 0) def count_file(name: Document.Node.Name): Long = if (loaded_theory(name)) 0 else name.path.file.length } private case class Load_State( pending: List[Document.Node.Name], rest: List[Document.Node.Name], load_limit: Long) { def next( dep_graph: Document.Node.Name.Graph[Unit], finished: Document.Node.Name => Boolean): (List[Document.Node.Name], Load_State) = { def load_requirements(pending1: List[Document.Node.Name], rest1: List[Document.Node.Name]) : (List[Document.Node.Name], Load_State) = { val load_theories = dep_graph.all_preds_rev(pending1).filterNot(finished) (load_theories, Load_State(pending1, rest1, load_limit)) } if (!pending.forall(finished)) (Nil, this) else if (rest.isEmpty) (Nil, Load_State.finished) else if (load_limit == 0) load_requirements(rest, Nil) else { val reachable = dep_graph.reachable_limit(load_limit, Load_State.count_file, dep_graph.imm_preds, rest) val (pending1, rest1) = rest.partition(reachable) load_requirements(pending1, rest1) } } } private sealed case class Use_Theories_State( dep_graph: Document.Node.Name.Graph[Unit], load_state: Load_State, watchdog_timeout: Time, commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit], last_update: Time = Time.now(), nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty, already_committed: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty, result: Option[Exn.Result[Use_Theories_Result]] = None) { def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State = copy(last_update = Time.now(), nodes_status = new_nodes_status) def watchdog: Boolean = watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout def finished_result: Boolean = result.isDefined def join_result: Option[(Exn.Result[Use_Theories_Result], Use_Theories_State)] = if (finished_result) Some((result.get, this)) else None def cancel_result: Use_Theories_State = if (finished_result) this else copy(result = Some(Exn.Exn(Exn.Interrupt()))) def clean_theories: (List[Document.Node.Name], Use_Theories_State) = { @tailrec def frontier(base: List[Document.Node.Name], front: Set[Document.Node.Name]) : Set[Document.Node.Name] = { val add = base.filter(name => dep_graph.imm_succs(name).forall(front)) if (add.isEmpty) front else { val preds = add.map(dep_graph.imm_preds) val base1 = (preds.head /: preds.tail)(_ ++ _).toList.filter(already_committed.keySet) frontier(base1, front ++ add) } } if (already_committed.isEmpty) (Nil, this) else { val base = (for { (name, (_, (_, succs))) <- dep_graph.iterator if succs.isEmpty && already_committed.isDefinedAt(name) } yield name).toList val clean = frontier(base, Set.empty) if (clean.isEmpty) (Nil, this) else { (dep_graph.topological_order.filter(clean), copy(dep_graph = dep_graph.exclude(clean))) } } } def check(state: Document.State, version: Document.Version, beyond_limit: Boolean) : (List[Document.Node.Name], Use_Theories_State) = { val already_committed1 = commit match { case None => already_committed case Some(commit_fn) => (already_committed /: dep_graph.topological_order)( { case (committed, name) => def parents_committed: Boolean = version.nodes(name).header.imports.forall(parent => loaded_theory(parent) || committed.isDefinedAt(parent)) if (!committed.isDefinedAt(name) && parents_committed && state.node_consolidated(version, name)) { val snapshot = stable_snapshot(state, version, name) val status = Document_Status.Node_Status.make(state, version, name) commit_fn(snapshot, status) committed + (name -> status) } else committed }) } def finished_theory(name: Document.Node.Name): Boolean = loaded_theory(name) || (if (commit.isDefined) already_committed1.isDefinedAt(name) else state.node_consolidated(version, name)) val result1 = if (!finished_result && (beyond_limit || watchdog || dep_graph.keys_iterator.forall(name => finished_theory(name) || nodes_status.quasi_consolidated(name)))) { val nodes = (for { name <- dep_graph.keys_iterator if !loaded_theory(name) } yield { (name -> Document_Status.Node_Status.make(state, version, name)) }).toList val nodes_committed = (for { name <- dep_graph.keys_iterator status <- already_committed1.get(name) } yield (name -> status)).toList Some(Exn.Res(new Use_Theories_Result(state, version, nodes, nodes_committed))) } else result val (load_theories, load_state1) = load_state.next(dep_graph, finished_theory) (load_theories, copy(already_committed = already_committed1, result = result1, load_state = load_state1)) } } def use_theories( theories: List[String], qualifier: String = Sessions.DRAFT, master_dir: String = "", unicode_symbols: Boolean = false, check_delay: Time = default_check_delay, check_limit: Int = default_check_limit, watchdog_timeout: Time = default_watchdog_timeout, nodes_status_delay: Time = default_nodes_status_delay, id: UUID.T = UUID.random(), // commit: must not block, must not fail commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None, commit_cleanup_delay: Time = default_commit_cleanup_delay, progress: Progress = new Progress): Use_Theories_Result = { val dependencies = { val import_names = theories.map(thy => resources.import_name(qualifier, master_directory(master_dir), thy) -> Position.none) resources.dependencies(import_names, progress = progress).check_errors } val dep_theories = dependencies.theories val dep_theories_set = dep_theories.toSet val dep_files = dependencies.loaded_files(false).flatMap(_._2). map(path => Document.Node.Name(resources.append("", path))) val use_theories_state = { val dep_graph = dependencies.theory_graph val maximals = dep_graph.maximals val rest = if (maximals.isEmpty || maximals.tail.isEmpty) maximals else { val depth = dep_graph.node_depth(Load_State.count_file) maximals.sortBy(node => - depth(node)) } val load_limit = if (commit.isDefined) (session_options.real("headless_load_limit") * 1024 * 1024).round else 0 val load_state = Load_State(Nil, rest, load_limit) Synchronized(Use_Theories_State(dep_graph, load_state, watchdog_timeout, commit)) } def check_state(beyond_limit: Boolean = false) { val state = session.get_state() for { version <- state.stable_tip_version load_theories = use_theories_state.change_result(_.check(state, version, beyond_limit)) if load_theories.nonEmpty } resources.load_theories(session, id, load_theories, dep_files, unicode_symbols, progress) } val check_progress = { var check_count = 0 Event_Timer.request(Time.now(), repeat = Some(check_delay)) { if (progress.stopped) use_theories_state.change(_.cancel_result) else { check_count += 1 check_state(check_limit > 0 && check_count > check_limit) } } } val consumer = { val delay_nodes_status = Delay.first(nodes_status_delay max Time.zero) { progress.nodes_status(use_theories_state.value.nodes_status) } val delay_commit_clean = Delay.first(commit_cleanup_delay max Time.zero) { val clean_theories = use_theories_state.change_result(_.clean_theories) if (clean_theories.nonEmpty) { progress.echo("Removing " + clean_theories.length + " theories ...") resources.clean_theories(session, id, clean_theories) } } Session.Consumer[Session.Commands_Changed](getClass.getName) { case changed => if (changed.nodes.exists(dep_theories_set)) { val snapshot = session.snapshot() val state = snapshot.state val version = snapshot.version val theory_progress = use_theories_state.change_result(st => { val domain = if (st.nodes_status.is_empty) dep_theories_set else changed.nodes.iterator.filter(dep_theories_set).toSet val (nodes_status_changed, nodes_status1) = st.nodes_status.update(resources, state, version, domain = Some(domain), trim = changed.assignment) if (nodes_status_delay >= Time.zero && nodes_status_changed) { delay_nodes_status.invoke } val theory_progress = (for { (name, node_status) <- nodes_status1.present.iterator if changed.nodes.contains(name) && !st.already_committed.isDefinedAt(name) p1 = node_status.percentage if p1 > 0 && Some(p1) != st.nodes_status.get(name).map(_.percentage) } yield Progress.Theory(name.theory, percentage = Some(p1))).toList (theory_progress, st.update(nodes_status1)) }) theory_progress.foreach(progress.theory) check_state() if (commit.isDefined && commit_cleanup_delay > Time.zero) { if (use_theories_state.value.finished_result) delay_commit_clean.revoke else delay_commit_clean.invoke } } } } try { session.commands_changed += consumer check_state() use_theories_state.guarded_access(_.join_result) check_progress.cancel } finally { session.commands_changed -= consumer resources.unload_theories(session, id, dep_theories) } Exn.release(use_theories_state.guarded_access(_.join_result)) } def purge_theories( theories: List[String], qualifier: String = Sessions.DRAFT, master_dir: String = "", all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) = { val nodes = if (all) None else Some(theories.map(resources.import_name(qualifier, master_directory(master_dir), _))) resources.purge_theories(session, nodes) } } /** resources **/ object Resources { def apply(options: Options, base_info: Sessions.Base_Info, log: Logger = No_Logger): Resources = new Resources(options, base_info, log = log) def make( options: Options, session_name: String, session_dirs: List[Path] = Nil, include_sessions: List[String] = Nil, progress: Progress = new Progress, log: Logger = No_Logger): Resources = { val base_info = Sessions.base_info(options, session_name, dirs = session_dirs, include_sessions = include_sessions, progress = progress) apply(options, base_info, log = log) } final class Theory private[Headless]( val node_name: Document.Node.Name, val node_header: Document.Node.Header, val text: String, val node_required: Boolean) { override def toString: String = node_name.toString def node_perspective: Document.Node.Perspective_Text = Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty) def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] = List(node_name -> Document.Node.Deps(node_header), node_name -> Document.Node.Edits(text_edits), node_name -> node_perspective) def node_edits(old: Option[Theory]): List[Document.Edit_Text] = { val (text_edits, old_required) = if (old.isEmpty) (Text.Edit.inserts(0, text), false) else (Text.Edit.replace(0, old.get.text, text), old.get.node_required) if (text_edits.isEmpty && node_required == old_required) Nil else make_edits(text_edits) } def purge_edits: List[Document.Edit_Text] = make_edits(Text.Edit.removes(0, text)) def required(required: Boolean): Theory = if (required == node_required) this else new Theory(node_name, node_header, text, required) } sealed case class State( blobs: Map[Document.Node.Name, Document.Blob] = Map.empty, theories: Map[Document.Node.Name, Theory] = Map.empty, required: Multi_Map[Document.Node.Name, UUID.T] = Multi_Map.empty) { /* blobs */ def doc_blobs: Document.Blobs = Document.Blobs(blobs) def update_blobs(names: List[Document.Node.Name]): (Document.Blobs, State) = { val new_blobs = names.flatMap(name => { val bytes = Bytes.read(name.path) def new_blob: Document.Blob = { val text = bytes.text Document.Blob(bytes, text, Symbol.Text_Chunk(text), changed = true) } blobs.get(name) match { case Some(blob) => if (blob.bytes == bytes) None else Some(name -> new_blob) case None => Some(name -> new_blob) } }) val blobs1 = (blobs /: new_blobs)(_ + _) val blobs2 = (blobs /: new_blobs)({ case (map, (a, b)) => map + (a -> b.unchanged) }) (Document.Blobs(blobs1), copy(blobs = blobs2)) } def blob_edits(name: Document.Node.Name, old_blob: Option[Document.Blob]) : List[Document.Edit_Text] = { val blob = blobs.getOrElse(name, error("Missing blob " + quote(name.toString))) val text_edits = old_blob match { case None => List(Text.Edit.insert(0, blob.source)) case Some(blob0) => Text.Edit.replace(0, blob0.source, blob.source) } if (text_edits.isEmpty) Nil else List(name -> Document.Node.Blob(blob), name -> Document.Node.Edits(text_edits)) } /* theories */ lazy val theory_graph: Document.Node.Name.Graph[Unit] = Document.Node.Name.make_graph( for ((name, theory) <- theories.toList) yield ((name, ()), theory.node_header.imports.filter(theories.isDefinedAt))) def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name) def insert_required(id: UUID.T, names: List[Document.Node.Name]): State = copy(required = (required /: names)(_.insert(_, id))) def remove_required(id: UUID.T, names: List[Document.Node.Name]): State = copy(required = (required /: names)(_.remove(_, id))) def update_theories(update: List[(Document.Node.Name, Theory)]): State = copy(theories = (theories /: update)({ case (thys, (name, thy)) => thys.get(name) match { case Some(thy1) if thy1 == thy => thys case _ => thys + (name -> thy) } })) def remove_theories(remove: List[Document.Node.Name]): State = { require(remove.forall(name => !is_required(name))) copy(theories = theories -- remove) } def unload_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]) : (List[Document.Edit_Text], State) = { val st1 = remove_required(id, theories) val theory_edits = for { node_name <- theories theory <- st1.theories.get(node_name) } yield { val theory1 = theory.required(st1.is_required(node_name)) val edits = theory1.node_edits(Some(theory)) (edits, (node_name, theory1)) } (theory_edits.flatMap(_._1), st1.update_theories(theory_edits.map(_._2))) } def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]]) : ((List[Document.Node.Name], List[Document.Node.Name], List[Document.Edit_Text]), State) = { val all_nodes = theory_graph.topological_order val purge = nodes.getOrElse(all_nodes).filterNot(is_required).toSet val retain = theory_graph.all_preds(all_nodes.filterNot(purge)).toSet val (retained, purged) = all_nodes.partition(retain) val purge_edits = purged.flatMap(name => theories(name).purge_edits) ((purged, retained, purge_edits), remove_theories(purged)) } } } class Resources private[Headless]( val options: Options, val session_base_info: Sessions.Base_Info, log: Logger = No_Logger) extends isabelle.Resources( - session_base_info.sessions_structure, session_base_info.check_base, log = log) + session_base_info.sessions_structure, session_base_info.check.base, log = log) { resources => val store: Sessions.Store = Sessions.store(options) /* session */ def start_session(print_mode: List[String] = Nil, progress: Progress = new Progress): Session = { val session = new Session(session_base_info.session, options, resources) progress.echo("Starting session " + session_base_info.session + " ...") Isabelle_Process(session, options, session_base_info.sessions_structure, store, logic = session_base_info.session, modes = print_mode).await_startup session } /* theories */ private val state = Synchronized(Resources.State()) def load_theories( session: Session, id: UUID.T, theories: List[Document.Node.Name], files: List[Document.Node.Name], unicode_symbols: Boolean, progress: Progress) { val loaded_theories = for (node_name <- theories) yield { val path = node_name.path if (!node_name.is_theory) error("Not a theory file: " + path) progress.expose_interrupt() val text0 = File.read(path) val text = if (unicode_symbols) Symbol.decode(text0) else text0 val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text)) new Resources.Theory(node_name, node_header, text, true) } val loaded = loaded_theories.length if (loaded > 1) progress.echo("Loading " + loaded + " theories ...") state.change(st => { val (doc_blobs1, st1) = st.insert_required(id, theories).update_blobs(files) val theory_edits = for (theory <- loaded_theories) yield { val node_name = theory.node_name val theory1 = theory.required(st1.is_required(node_name)) val edits = theory1.node_edits(st1.theories.get(node_name)) (edits, (node_name, theory1)) } val file_edits = for { node_name <- files if doc_blobs1.changed(node_name) } yield st1.blob_edits(node_name, st.blobs.get(node_name)) session.update(doc_blobs1, theory_edits.flatMap(_._1) ::: file_edits.flatten) st1.update_theories(theory_edits.map(_._2)) }) } def unload_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]) { state.change(st => { val (edits, st1) = st.unload_theories(session, id, theories) session.update(st.doc_blobs, edits) st1 }) } def clean_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]) { state.change(st => { val (edits1, st1) = st.unload_theories(session, id, theories) val ((_, _, edits2), st2) = st1.purge_theories(session, None) session.update(st.doc_blobs, edits1 ::: edits2) st2 }) } def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]]) : (List[Document.Node.Name], List[Document.Node.Name]) = { state.change_result(st => { val ((purged, retained, _), st1) = st.purge_theories(session, nodes) ((purged, retained), st1) }) } } } diff --git a/src/Pure/Thy/sessions.scala b/src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala +++ b/src/Pure/Thy/sessions.scala @@ -1,1397 +1,1397 @@ /* Title: Pure/Thy/sessions.scala Author: Makarius Cumulative session information. */ package isabelle import java.io.{File => JFile} import java.nio.ByteBuffer import java.nio.channels.FileChannel import java.nio.file.StandardOpenOption import scala.collection.{SortedSet, SortedMap} import scala.collection.mutable object Sessions { /* session and theory names */ val root_name: String = "ROOT" val theory_name: String = "Pure.Sessions" val UNSORTED = "Unsorted" val DRAFT = "Draft" def is_pure(name: String): Boolean = name == Thy_Header.PURE def exclude_session(name: String): Boolean = name == "" || name == DRAFT def exclude_theory(name: String): Boolean = name == root_name || name == "README" || name == "index" || name == "bib" /* base info and source dependencies */ object Base { def bootstrap( session_directories: Map[JFile, String], global_theories: Map[String, String]): Base = Base( session_directories = session_directories, global_theories = global_theories, overall_syntax = Thy_Header.bootstrap_syntax) } sealed case class Base( pos: Position.T = Position.none, doc_names: List[String] = Nil, session_directories: Map[JFile, String] = Map.empty, global_theories: Map[String, String] = Map.empty, session_theories: List[Document.Node.Name] = Nil, document_theories: List[Document.Node.Name] = Nil, loaded_theories: Graph[String, Outer_Syntax] = Graph.string, used_theories: List[(Document.Node.Name, Options)] = Nil, known_theories: Map[String, Document.Node.Entry] = Map.empty, known_loaded_files: Map[String, List[Path]] = Map.empty, overall_syntax: Outer_Syntax = Outer_Syntax.empty, imported_sources: List[(Path, SHA1.Digest)] = Nil, sources: List[(Path, SHA1.Digest)] = Nil, session_graph_display: Graph_Display.Graph = Graph_Display.empty_graph, errors: List[String] = Nil) { override def toString: String = "Sessions.Base(loaded_theories = " + loaded_theories.size + ", used_theories = " + used_theories.length + ")" def theory_qualifier(name: String): String = global_theories.getOrElse(name, Long_Name.qualifier(name)) def theory_qualifier(name: Document.Node.Name): String = theory_qualifier(name.theory) def loaded_theory(name: String): Boolean = loaded_theories.defined(name) def loaded_theory(name: Document.Node.Name): Boolean = loaded_theory(name.theory) def loaded_theory_syntax(name: String): Option[Outer_Syntax] = if (loaded_theory(name)) Some(loaded_theories.get_node(name)) else None def loaded_theory_syntax(name: Document.Node.Name): Option[Outer_Syntax] = loaded_theory_syntax(name.theory) def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax = nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax } sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base]) { override def toString: String = "Sessions.Deps(" + sessions_structure + ")" def is_empty: Boolean = session_bases.isEmpty def apply(name: String): Base = session_bases(name) def get(name: String): Option[Base] = session_bases.get(name) def imported_sources(name: String): List[SHA1.Digest] = session_bases(name).imported_sources.map(_._2) def sources(name: String): List[SHA1.Digest] = session_bases(name).sources.map(_._2) def errors: List[String] = (for { (name, base) <- session_bases.iterator if base.errors.nonEmpty } yield cat_lines(base.errors) + "\nThe error(s) above occurred in session " + quote(name) + Position.here(base.pos) ).toList def check_errors: Deps = errors match { case Nil => this case errs => error(cat_lines(errs)) } } def deps(sessions_structure: Structure, progress: Progress = new Progress, inlined_files: Boolean = false, verbose: Boolean = false, list_files: Boolean = false, check_keywords: Set[String] = Set.empty): Deps = { var cache_sources = Map.empty[JFile, SHA1.Digest] def check_sources(paths: List[Path]): List[(Path, SHA1.Digest)] = { for { path <- paths file = path.file if cache_sources.isDefinedAt(file) || file.isFile } yield { cache_sources.get(file) match { case Some(digest) => (path, digest) case None => val digest = SHA1.digest(file) cache_sources = cache_sources + (file -> digest) (path, digest) } } } val doc_names = Doc.doc_names() val bootstrap = Sessions.Base.bootstrap( sessions_structure.session_directories, sessions_structure.global_theories) val session_bases = (Map("" -> bootstrap) /: sessions_structure.imports_topological_order)({ case (session_bases, session_name) => progress.expose_interrupt() val info = sessions_structure(session_name) try { val deps_base = info.deps_base(session_bases) val resources = new Resources(sessions_structure, deps_base) if (verbose || list_files) { val groups = if (info.groups.isEmpty) "" else info.groups.mkString(" (", " ", ")") progress.echo("Session " + info.chapter + "/" + info.name + groups) } val dependencies = resources.session_dependencies(info) val overall_syntax = dependencies.overall_syntax val session_theories = dependencies.theories.filter(name => deps_base.theory_qualifier(name) == session_name) val theory_files = dependencies.theories.map(_.path) val (loaded_files, loaded_files_errors) = try { if (inlined_files) (dependencies.loaded_files(Sessions.is_pure(info.name)), Nil) else (Nil, Nil) } catch { case ERROR(msg) => (Nil, List(msg)) } val session_files = (theory_files ::: loaded_files.flatMap(_._2) ::: info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand) val imported_files = if (inlined_files) dependencies.imported_files else Nil if (list_files) progress.echo(cat_lines(session_files.map(_.implode).sorted.map(" " + _))) if (check_keywords.nonEmpty) { Check_Keywords.check_keywords( progress, overall_syntax.keywords, check_keywords, theory_files) } val session_graph_display: Graph_Display.Graph = { def session_node(name: String): Graph_Display.Node = Graph_Display.Node("[" + name + "]", "session." + name) def node(name: Document.Node.Name): Graph_Display.Node = { val qualifier = deps_base.theory_qualifier(name) if (qualifier == info.name) Graph_Display.Node(name.theory_base_name, "theory." + name.theory) else session_node(qualifier) } val required_sessions = dependencies.loaded_theories.all_preds(dependencies.theories.map(_.theory)) .map(theory => deps_base.theory_qualifier(theory)) .filter(name => name != info.name && sessions_structure.defined(name)) val required_subgraph = sessions_structure.imports_graph .restrict(sessions_structure.imports_graph.all_preds(required_sessions).toSet) .transitive_closure .restrict(required_sessions.toSet) .transitive_reduction_acyclic val graph0 = (Graph_Display.empty_graph /: required_subgraph.topological_order)( { case (g, session) => val a = session_node(session) val bs = required_subgraph.imm_preds(session).toList.map(session_node) ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) }) (graph0 /: dependencies.entries)( { case (g, entry) => val a = node(entry.name) val bs = entry.header.imports.map(node).filterNot(_ == a) ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) }) } val known_theories = (deps_base.known_theories /: dependencies.entries.iterator.map(entry => entry.name.theory -> entry))(_ + _) val known_loaded_files = deps_base.known_loaded_files ++ loaded_files val import_errors = { val known_sessions = sessions_structure.imports_requirements(List(session_name)).toSet for { name <- dependencies.theories qualifier = deps_base.theory_qualifier(name) if !known_sessions(qualifier) } yield "Bad import of theory " + quote(name.toString) + ": need to include sessions " + quote(qualifier) + " in ROOT" } val document_errors = info.document_theories.flatMap( { case (thy, pos) => val parent_sessions = sessions_structure.build_requirements(List(session_name)) def err(msg: String): Option[String] = Some(msg + " " + quote(thy) + Position.here(pos)) known_theories.get(thy).map(_.name) match { case None => err("Unknown document theory") case Some(name) => val qualifier = deps_base.theory_qualifier(name) if (session_theories.contains(name)) { err("Redundant document theory from this session:") } else if (parent_sessions.contains(qualifier)) None else if (dependencies.theories.contains(name)) None else err("Document theory from other session not imported properly:") } }) val document_theories = info.document_theories.map({ case (thy, _) => known_theories(thy).name }) val dir_errors = { val ok = info.dirs.map(_.canonical_file).toSet val bad = (for { name <- session_theories.iterator path = name.master_dir_path if !ok(path.canonical_file) path1 = File.relative_path(info.dir.canonical, path).getOrElse(path) } yield (path1, name)).toList val bad_dirs = (for { (path1, _) <- bad } yield path1.toString).distinct.sorted val errs1 = for { (path1, name) <- bad } yield "Implicit use of directory " + path1 + " for theory " + quote(name.toString) val errs2 = if (bad_dirs.isEmpty) Nil else List("Implicit use of session directories: " + commas(bad_dirs)) val errs3 = for (p <- info.dirs if !p.is_dir) yield "No such directory: " + p val errs4 = (for { name <- session_theories.iterator name1 <- resources.find_theory_node(name.theory) if name.node != name1.node } yield "Incoherent theory file import:\n " + name.path + " vs. \n " + name1.path) .toList errs1 ::: errs2 ::: errs3 ::: errs4 } val sources_errors = for (p <- session_files if !p.is_file) yield "No such file: " + p val path_errors = try { Path.check_case_insensitive(session_files ::: imported_files); Nil } catch { case ERROR(msg) => List(msg) } val bibtex_errors = try { info.bibtex_entries; Nil } catch { case ERROR(msg) => List(msg) } val base = Base( pos = info.pos, doc_names = doc_names, session_directories = sessions_structure.session_directories, global_theories = sessions_structure.global_theories, session_theories = session_theories, document_theories = document_theories, loaded_theories = dependencies.loaded_theories, used_theories = dependencies.theories_adjunct, known_theories = known_theories, known_loaded_files = known_loaded_files, overall_syntax = overall_syntax, imported_sources = check_sources(imported_files), sources = check_sources(session_files), session_graph_display = session_graph_display, errors = dependencies.errors ::: loaded_files_errors ::: import_errors ::: document_errors ::: dir_errors ::: sources_errors ::: path_errors ::: bibtex_errors) session_bases + (info.name -> base) } catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred in session " + quote(info.name) + Position.here(info.pos)) } }) Deps(sessions_structure, session_bases) } /* base info */ sealed case class Base_Info( session: String, sessions_structure: Structure, errors: List[String], base: Base, infos: List[Info]) { - def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors)) + def check: Base_Info = if (errors.isEmpty) this else error(cat_lines(errors)) } def base_info(options: Options, session: String, progress: Progress = new Progress, dirs: List[Path] = Nil, include_sessions: List[String] = Nil, session_ancestor: Option[String] = None, session_requirements: Boolean = false): Base_Info = { val full_sessions = load_structure(options, dirs = dirs) val selected_sessions = full_sessions.selection(Selection(sessions = session :: session_ancestor.toList)) val info = selected_sessions(session) val ancestor = session_ancestor orElse info.parent val (session1, infos1) = if (session_requirements && ancestor.isDefined) { val deps = Sessions.deps(selected_sessions, progress = progress) val base = deps(session) val ancestor_loaded = deps.get(ancestor.get) match { case Some(ancestor_base) if !selected_sessions.imports_requirements(List(ancestor.get)).contains(session) => ancestor_base.loaded_theories.defined _ case _ => error("Bad ancestor " + quote(ancestor.get) + " for session " + quote(session)) } val required_theories = for { thy <- base.loaded_theories.keys if !ancestor_loaded(thy) && base.theory_qualifier(thy) != session } yield thy if (required_theories.isEmpty) (ancestor.get, Nil) else { val other_name = info.name + "_requirements(" + ancestor.get + ")" Isabelle_System.isabelle_tmp_prefix() (other_name, List( make_info(info.options, dir_selected = false, dir = Path.explode("$ISABELLE_TMP_PREFIX"), chapter = info.chapter, Session_Entry( pos = info.pos, name = other_name, groups = info.groups, path = ".", parent = ancestor, description = "Required theory imports from other sessions", options = Nil, imports = info.deps, directories = Nil, theories = List((Nil, required_theories.map(thy => ((thy, Position.none), false)))), document_theories = Nil, document_files = Nil, export_files = Nil)))) } } else (session, Nil) val full_sessions1 = if (infos1.isEmpty) full_sessions else load_structure(options, dirs = dirs, infos = infos1) val selected_sessions1 = full_sessions1.selection(Selection(sessions = session1 :: session :: include_sessions)) val deps1 = Sessions.deps(selected_sessions1, progress = progress) Base_Info(session1, full_sessions1, deps1.errors, deps1(session1), infos1) } /* cumulative session info */ sealed case class Info( name: String, chapter: String, dir_selected: Boolean, pos: Position.T, groups: List[String], dir: Path, parent: Option[String], description: String, directories: List[Path], options: Options, imports: List[String], theories: List[(Options, List[(String, Position.T)])], global_theories: List[String], document_theories: List[(String, Position.T)], document_files: List[(Path, Path)], export_files: List[(Path, Int, List[String])], meta_digest: SHA1.Digest) { def chapter_session: Path = Path.basic(chapter) + Path.basic(name) def deps: List[String] = parent.toList ::: imports def deps_base(session_bases: String => Base): Base = { val parent_base = session_bases(parent.getOrElse("")) val imports_bases = imports.map(session_bases) parent_base.copy( known_theories = (parent_base.known_theories /: (for { base <- imports_bases.iterator (_, entry) <- base.known_theories.iterator } yield (entry.name.theory -> entry)))(_ + _), known_loaded_files = (parent_base.known_loaded_files /: imports_bases.iterator.map(_.known_loaded_files))(_ ++ _)) } def dirs: List[Path] = dir :: directories def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale")) def document_enabled: Boolean = options.string("document") match { case "" | "false" => false case "pdf" => true case doc => error("Bad document specification " + quote(doc)) } def documents: List[(String, List[String])] = { val variants = for (s <- Library.space_explode(':', options.string("document_variants"))) yield { Library.space_explode('=', s) match { case List(name) => (name, Nil) case List(name, tags) => (name, Library.space_explode(',', tags)) case _ => error("Malformed document_variants: " + quote(s)) } } val dups = Library.duplicates(variants.map(_._1)) if (dups.nonEmpty) error("Duplicate document variants: " + commas_quote(dups)) if (!document_enabled || document_files.isEmpty) Nil else variants } def document_output: Option[Path] = options.string("document_output") match { case "" => None case s => Some(dir + Path.explode(s)) } lazy val bibtex_entries: List[Text.Info[String]] = (for { (document_dir, file) <- document_files.iterator if Bibtex.is_bibtex(file.file_name) info <- Bibtex.entries(File.read(dir + document_dir + file)).iterator } yield info).toList def record_proofs: Boolean = options.int("record_proofs") >= 2 def is_afp: Boolean = chapter == AFP.chapter def is_afp_bulky: Boolean = is_afp && groups.exists(AFP.groups_bulky.contains) } def make_info(options: Options, dir_selected: Boolean, dir: Path, chapter: String, entry: Session_Entry): Info = { try { val name = entry.name if (exclude_session(name)) error("Bad session name") if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session") if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session") val session_path = dir + Path.explode(entry.path) val directories = entry.directories.map(dir => session_path + Path.explode(dir)) val session_options = options ++ entry.options val theories = entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map({ case ((thy, pos), _) => if (exclude_theory(thy)) error("Bad theory name " + quote(thy) + Position.here(pos)) else (thy, pos) })) }) val global_theories = for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global } yield { val thy_name = Path.explode(thy).file_name if (Long_Name.is_qualified(thy_name)) error("Bad qualified name for global theory " + quote(thy_name) + Position.here(pos)) else thy_name } val conditions = theories.flatMap(thys => space_explode(',', thys._1.string("condition"))).distinct.sorted. map(x => (x, Isabelle_System.getenv(x) != "")) val document_files = entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) }) val export_files = entry.export_files.map({ case (dir, prune, pats) => (Path.explode(dir), prune, pats) }) val meta_digest = SHA1.digest( (name, chapter, entry.parent, entry.directories, entry.options, entry.imports, entry.theories_no_position, conditions, entry.document_theories, entry.document_files) .toString) Info(name, chapter, dir_selected, entry.pos, entry.groups, session_path, entry.parent, entry.description, directories, session_options, entry.imports, theories, global_theories, entry.document_theories, document_files, export_files, meta_digest) } catch { case ERROR(msg) => error(msg + "\nThe error(s) above occurred in session entry " + quote(entry.name) + Position.here(entry.pos)) } } object Selection { val empty: Selection = Selection() val all: Selection = Selection(all_sessions = true) def session(session: String): Selection = Selection(sessions = List(session)) } sealed case class Selection( requirements: Boolean = false, all_sessions: Boolean = false, base_sessions: List[String] = Nil, exclude_session_groups: List[String] = Nil, exclude_sessions: List[String] = Nil, session_groups: List[String] = Nil, sessions: List[String] = Nil) { def ++ (other: Selection): Selection = Selection( requirements = requirements || other.requirements, all_sessions = all_sessions || other.all_sessions, base_sessions = Library.merge(base_sessions, other.base_sessions), exclude_session_groups = Library.merge(exclude_session_groups, other.exclude_session_groups), exclude_sessions = Library.merge(exclude_sessions, other.exclude_sessions), session_groups = Library.merge(session_groups, other.session_groups), sessions = Library.merge(sessions, other.sessions)) } def make(infos: List[Info]): Structure = { def add_edges(graph: Graph[String, Info], kind: String, edges: Info => Traversable[String]) : Graph[String, Info] = { def add_edge(pos: Position.T, name: String, g: Graph[String, Info], parent: String) = { if (!g.defined(parent)) error("Bad " + kind + " session " + quote(parent) + " for " + quote(name) + Position.here(pos)) try { g.add_edge_acyclic(parent, name) } catch { case exn: Graph.Cycles[_] => error(cat_lines(exn.cycles.map(cycle => "Cyclic session dependency of " + cycle.map(c => quote(c.toString)).mkString(" via "))) + Position.here(pos)) } } (graph /: graph.iterator) { case (g, (name, (info, _))) => (g /: edges(info))(add_edge(info.pos, name, _, _)) } } val info_graph = (Graph.string[Info] /: infos) { case (graph, info) => if (graph.defined(info.name)) error("Duplicate session " + quote(info.name) + Position.here(info.pos) + Position.here(graph.get_node(info.name).pos)) else graph.new_node(info.name, info) } val build_graph = add_edges(info_graph, "parent", _.parent) val imports_graph = add_edges(build_graph, "imports", _.imports) val session_positions: List[(String, Position.T)] = (for ((name, (info, _)) <- info_graph.iterator) yield (name, info.pos)).toList val session_directories: Map[JFile, String] = (Map.empty[JFile, String] /: (for { session <- imports_graph.topological_order.iterator info = info_graph.get_node(session) dir <- info.dirs.iterator } yield (info, dir)))({ case (dirs, (info, dir)) => val session = info.name val canonical_dir = dir.canonical_file dirs.get(canonical_dir) match { case Some(session1) => val info1 = info_graph.get_node(session1) error("Duplicate use of directory " + dir + "\n for session " + quote(session1) + Position.here(info1.pos) + "\n vs. session " + quote(session) + Position.here(info.pos)) case None => dirs + (canonical_dir -> session) } }) val global_theories: Map[String, String] = (Thy_Header.bootstrap_global_theories.toMap /: (for { session <- imports_graph.topological_order.iterator info = info_graph.get_node(session) thy <- info.global_theories.iterator } yield (info, thy)))({ case (global, (info, thy)) => val qualifier = info.name global.get(thy) match { case Some(qualifier1) if qualifier != qualifier1 => error("Duplicate global theory " + quote(thy) + Position.here(info.pos)) case _ => global + (thy -> qualifier) } }) new Structure( session_positions, session_directories, global_theories, build_graph, imports_graph) } final class Structure private[Sessions]( val session_positions: List[(String, Position.T)], val session_directories: Map[JFile, String], val global_theories: Map[String, String], val build_graph: Graph[String, Info], val imports_graph: Graph[String, Info]) { sessions_structure => def dest_session_directories: List[(String, String)] = for ((file, session) <- session_directories.toList) yield (File.standard_path(file), session) lazy val chapters: SortedMap[String, List[Info]] = (SortedMap.empty[String, List[Info]] /: build_graph.iterator)( { case (chs, (_, (info, _))) => chs + (info.chapter -> (info :: chs.getOrElse(info.chapter, Nil))) }) def build_graph_display: Graph_Display.Graph = Graph_Display.make_graph(build_graph) def imports_graph_display: Graph_Display.Graph = Graph_Display.make_graph(imports_graph) def defined(name: String): Boolean = imports_graph.defined(name) def apply(name: String): Info = imports_graph.get_node(name) def get(name: String): Option[Info] = if (defined(name)) Some(apply(name)) else None def theory_qualifier(name: String): String = global_theories.getOrElse(name, Long_Name.qualifier(name)) def check_sessions(names: List[String]) { val bad_sessions = SortedSet(names.filterNot(defined): _*).toList if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions)) } def check_sessions(sel: Selection): Unit = check_sessions(sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions) private def selected(graph: Graph[String, Info], sel: Selection): List[String] = { check_sessions(sel) val select_group = sel.session_groups.toSet val select_session = sel.sessions.toSet ++ imports_graph.all_succs(sel.base_sessions) val selected0 = if (sel.all_sessions) graph.keys else { (for { (name, (info, _)) <- graph.iterator if info.dir_selected || select_session(name) || graph.get_node(name).groups.exists(select_group) } yield name).toList } if (sel.requirements) (graph.all_preds(selected0).toSet -- selected0).toList else selected0 } def selection(sel: Selection): Structure = { check_sessions(sel) val excluded = { val exclude_group = sel.exclude_session_groups.toSet val exclude_group_sessions = (for { (name, (info, _)) <- imports_graph.iterator if imports_graph.get_node(name).groups.exists(exclude_group) } yield name).toList imports_graph.all_succs(exclude_group_sessions ::: sel.exclude_sessions).toSet } def restrict(graph: Graph[String, Info]): Graph[String, Info] = { val sessions = graph.all_preds(selected(graph, sel)).filterNot(excluded) graph.restrict(graph.all_preds(sessions).toSet) } new Structure( session_positions, session_directories, global_theories, restrict(build_graph), restrict(imports_graph)) } def selection(session: String): Structure = selection(Selection.session(session)) def selection_deps( selection: Selection, progress: Progress = new Progress, loading_sessions: Boolean = false, inlined_files: Boolean = false, verbose: Boolean = false): Deps = { val deps = Sessions.deps(sessions_structure.selection(selection), progress = progress, inlined_files = inlined_files, verbose = verbose) if (loading_sessions) { val selection_size = deps.sessions_structure.build_graph.size if (selection_size > 1) progress.echo("Loading " + selection_size + " sessions ...") } deps } def build_selection(sel: Selection): List[String] = selected(build_graph, sel) def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss) def build_requirements(ss: List[String]): List[String] = build_graph.all_preds_rev(ss) def build_topological_order: List[String] = build_graph.topological_order def imports_selection(sel: Selection): List[String] = selected(imports_graph, sel) def imports_descendants(ss: List[String]): List[String] = imports_graph.all_succs(ss) def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds_rev(ss) def imports_topological_order: List[String] = imports_graph.topological_order def bibtex_entries: List[(String, List[String])] = build_topological_order.flatMap(name => apply(name).bibtex_entries match { case Nil => None case entries => Some(name -> entries.map(_.info)) }) def session_chapters: List[(String, String)] = imports_topological_order.map(name => name -> apply(name).chapter) override def toString: String = imports_graph.keys_iterator.mkString("Sessions.Structure(", ", ", ")") } /* parser */ val ROOT: Path = Path.explode("ROOT") val ROOTS: Path = Path.explode("ROOTS") private val CHAPTER = "chapter" private val SESSION = "session" private val IN = "in" private val DESCRIPTION = "description" private val DIRECTORIES = "directories" private val OPTIONS = "options" private val SESSIONS = "sessions" private val THEORIES = "theories" private val GLOBAL = "global" private val DOCUMENT_THEORIES = "document_theories" private val DOCUMENT_FILES = "document_files" private val EXPORT_FILES = "export_files" val root_syntax: Outer_Syntax = Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" + GLOBAL + IN + (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) + (DESCRIPTION, Keyword.QUASI_COMMAND) + (DIRECTORIES, Keyword.QUASI_COMMAND) + (OPTIONS, Keyword.QUASI_COMMAND) + (SESSIONS, Keyword.QUASI_COMMAND) + (THEORIES, Keyword.QUASI_COMMAND) + (DOCUMENT_THEORIES, Keyword.QUASI_COMMAND) + (DOCUMENT_FILES, Keyword.QUASI_COMMAND) + (EXPORT_FILES, Keyword.QUASI_COMMAND) abstract class Entry sealed case class Chapter(name: String) extends Entry sealed case class Session_Entry( pos: Position.T, name: String, groups: List[String], path: String, parent: Option[String], description: String, options: List[Options.Spec], imports: List[String], directories: List[String], theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])], document_theories: List[(String, Position.T)], document_files: List[(String, String)], export_files: List[(String, Int, List[String])]) extends Entry { def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] = theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) }) } private object Parser extends Options.Parser { private val chapter: Parser[Chapter] = { val chapter_name = atom("chapter name", _.is_name) command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) } } private val session_entry: Parser[Session_Entry] = { val option = option_name ~ opt($$$("=") ~! option_value ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) } val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]") val theory_entry = position(theory_name) ~ opt_keyword(GLOBAL) ^^ { case x ~ y => (x, y) } val theories = $$$(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_entry)) ^^ { case _ ~ (x ~ y) => (x, y) } val in_path = $$$("(") ~! ($$$(IN) ~ path ~ $$$(")")) ^^ { case _ ~ (_ ~ x ~ _) => x } val document_theories = $$$(DOCUMENT_THEORIES) ~! rep1(position(name)) ^^ { case _ ~ x => x } val document_files = $$$(DOCUMENT_FILES) ~! ((in_path | success("document")) ~ rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) } val prune = $$$("[") ~! (nat ~ $$$("]")) ^^ { case _ ~ (x ~ _) => x } | success(0) val export_files = $$$(EXPORT_FILES) ~! ((in_path | success("export")) ~ prune ~ rep1(embedded)) ^^ { case _ ~ (x ~ y ~ z) => (x, y, z) } command(SESSION) ~! (position(session_name) ~ (($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~ (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~ ($$$("=") ~! (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~ (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~ (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~ (($$$(SESSIONS) ~! rep1(session_name) ^^ { case _ ~ x => x }) | success(Nil)) ~ (($$$(DIRECTORIES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~ rep(theories) ~ (opt(document_theories) ^^ (x => x.getOrElse(Nil))) ~ (rep(document_files) ^^ (x => x.flatten)) ~ rep(export_files)))) ^^ { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j ~ k ~ l))) => Session_Entry(pos, a, b, c, d, e, f, g, h, i, j, k, l) } } def parse_root(path: Path): List[Entry] = { val toks = Token.explode(root_syntax.keywords, File.read(path)) val start = Token.Pos.file(path.implode) parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match { case Success(result, _) => result case bad => error(bad.toString) } } } def parse_root(path: Path): List[Entry] = Parser.parse_root(path) def parse_root_entries(path: Path): List[Session_Entry] = for (entry <- Parser.parse_root(path) if entry.isInstanceOf[Session_Entry]) yield entry.asInstanceOf[Session_Entry] def read_root(options: Options, select: Boolean, path: Path): List[Info] = { var entry_chapter = UNSORTED val infos = new mutable.ListBuffer[Info] parse_root(path).foreach { case Chapter(name) => entry_chapter = name case entry: Session_Entry => infos += make_info(options, select, path.dir, entry_chapter, entry) } infos.toList } def parse_roots(roots: Path): List[String] = { for { line <- split_lines(File.read(roots)) if !(line == "" || line.startsWith("#")) } yield line } /* load sessions from certain directories */ private def is_session_dir(dir: Path): Boolean = (dir + ROOT).is_file || (dir + ROOTS).is_file private def check_session_dir(dir: Path): Path = if (is_session_dir(dir)) File.pwd() + dir.expand else error("Bad session root directory: " + dir.toString) def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] = { val default_dirs = Isabelle_System.components().filter(is_session_dir) for { (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _)) } yield (select, dir.canonical) } def load_structure(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, infos: List[Info] = Nil): Structure = { def load_dir(select: Boolean, dir: Path): List[(Boolean, Path)] = load_root(select, dir) ::: load_roots(select, dir) def load_root(select: Boolean, dir: Path): List[(Boolean, Path)] = { val root = dir + ROOT if (root.is_file) List((select, root)) else Nil } def load_roots(select: Boolean, dir: Path): List[(Boolean, Path)] = { val roots = dir + ROOTS if (roots.is_file) { for { entry <- parse_roots(roots) dir1 = try { check_session_dir(dir + Path.explode(entry)) } catch { case ERROR(msg) => error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString) } res <- load_dir(select, dir1) } yield res } else Nil } val roots = for { (select, dir) <- directories(dirs, select_dirs) res <- load_dir(select, check_session_dir(dir)) } yield res val unique_roots = ((Map.empty[JFile, (Boolean, Path)] /: roots) { case (m, (select, path)) => val file = path.canonical_file m.get(file) match { case None => m + (file -> (select, path)) case Some((select1, path1)) => m + (file -> (select1 || select, path1)) } }).toList.map(_._2) make(unique_roots.flatMap(p => read_root(options, p._1, p._2)) ::: infos) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("sessions", "explore structure of Isabelle sessions", args => { var base_sessions: List[String] = Nil var select_dirs: List[Path] = Nil var requirements = false var exclude_session_groups: List[String] = Nil var all_sessions = false var dirs: List[Path] = Nil var session_groups: List[String] = Nil var exclude_sessions: List[String] = Nil val getopts = Getopts(""" Usage: isabelle sessions [OPTIONS] [SESSIONS ...] Options are: -B NAME include session NAME and all descendants -D DIR include session directory and select its sessions -R refer to requirements of selected sessions -X NAME exclude sessions from group NAME and all descendants -a select all sessions -d DIR include session directory -g NAME select session group NAME -x NAME exclude session NAME and all descendants Explore the structure of Isabelle sessions and print result names in topological order (on stdout). """, "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), "R" -> (_ => requirements = true), "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), "a" -> (_ => all_sessions = true), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "g:" -> (arg => session_groups = session_groups ::: List(arg)), "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) val sessions = getopts(args) val options = Options.init() val selection = Selection(requirements = requirements, all_sessions = all_sessions, base_sessions = base_sessions, exclude_session_groups = exclude_session_groups, exclude_sessions = exclude_sessions, session_groups = session_groups, sessions = sessions) val sessions_structure = load_structure(options, dirs = dirs, select_dirs = select_dirs).selection(selection) for (name <- sessions_structure.imports_topological_order) { Output.writeln(name, stdout = true) } }) /** heap file with SHA1 digest **/ private val sha1_prefix = "SHA1:" def read_heap_digest(heap: Path): Option[String] = { if (heap.is_file) { using(FileChannel.open(heap.file.toPath, StandardOpenOption.READ))(file => { val len = file.size val n = sha1_prefix.length + SHA1.digest_length if (len >= n) { file.position(len - n) val buf = ByteBuffer.allocate(n) var i = 0 var m = 0 do { m = file.read(buf) if (m != -1) i += m } while (m != -1 && n > i) if (i == n) { val prefix = new String(buf.array(), 0, sha1_prefix.length, UTF8.charset) val s = new String(buf.array(), sha1_prefix.length, SHA1.digest_length, UTF8.charset) if (prefix == sha1_prefix) Some(s) else None } else None } else None }) } else None } def write_heap_digest(heap: Path): String = read_heap_digest(heap) match { case None => val s = SHA1.digest(heap).rep File.append(heap, sha1_prefix + s) s case Some(s) => s } /** persistent store **/ object Session_Info { val session_name = SQL.Column.string("session_name").make_primary_key // Build_Log.Session_Info val session_timing = SQL.Column.bytes("session_timing") val command_timings = SQL.Column.bytes("command_timings") val theory_timings = SQL.Column.bytes("theory_timings") val ml_statistics = SQL.Column.bytes("ml_statistics") val task_statistics = SQL.Column.bytes("task_statistics") val errors = SQL.Column.bytes("errors") val build_log_columns = List(session_name, session_timing, command_timings, theory_timings, ml_statistics, task_statistics, errors) // Build.Session_Info val sources = SQL.Column.string("sources") val input_heaps = SQL.Column.string("input_heaps") val output_heap = SQL.Column.string("output_heap") val return_code = SQL.Column.int("return_code") val build_columns = List(sources, input_heaps, output_heap, return_code) val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns) } def store(options: Options): Store = new Store(options) class Store private[Sessions](val options: Options) { override def toString: String = "Store(output_dir = " + output_dir.expand + ")" val xml_cache: XML.Cache = XML.make_cache() val xz_cache: XZ.Cache = XZ.make_cache() /* directories */ val system_output_dir: Path = Path.explode("$ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER") val user_output_dir: Path = Path.explode("$ISABELLE_HEAPS/$ML_IDENTIFIER") def system_heaps: Boolean = options.bool("system_heaps") val output_dir: Path = if (system_heaps) system_output_dir else user_output_dir val input_dirs: List[Path] = if (system_heaps) List(system_output_dir) else List(user_output_dir, system_output_dir) val browser_info: Path = if (system_heaps) Path.explode("$ISABELLE_BROWSER_INFO_SYSTEM") else Path.explode("$ISABELLE_BROWSER_INFO") /* file names */ def heap(name: String): Path = Path.basic(name) def database(name: String): Path = Path.basic("log") + Path.basic(name).ext("db") def log(name: String): Path = Path.basic("log") + Path.basic(name) def log_gz(name: String): Path = log(name).ext("gz") def output_heap(name: String): Path = output_dir + heap(name) def output_database(name: String): Path = output_dir + database(name) def output_log(name: String): Path = output_dir + log(name) def output_log_gz(name: String): Path = output_dir + log_gz(name) def prepare_output_dir() { Isabelle_System.make_directory(output_dir + Path.basic("log")) } /* heap */ def find_heap(name: String): Option[Path] = input_dirs.map(_ + heap(name)).find(_.is_file) def find_heap_digest(name: String): Option[String] = find_heap(name).flatMap(read_heap_digest) def the_heap(name: String): Path = find_heap(name) getOrElse error("Missing heap image for session " + quote(name) + " -- expected in:\n" + cat_lines(input_dirs.map(dir => " " + dir.expand.implode))) /* database */ private def database_server: Boolean = options.bool("build_database_server") def access_database(name: String, output: Boolean = false): Option[SQL.Database] = { if (database_server) { val db = PostgreSQL.open_database( user = options.string("build_database_user"), password = options.string("build_database_password"), database = options.string("build_database_name"), host = options.string("build_database_host"), port = options.int("build_database_port"), ssh = options.proper_string("build_database_ssh_host").map(ssh_host => SSH.open_session(options, host = ssh_host, user = options.string("build_database_ssh_user"), port = options.int("build_database_ssh_port"))), ssh_close = true) if (output || has_session_info(db, name)) Some(db) else { db.close; None } } else if (output) Some(SQLite.open_database(output_database(name))) else input_dirs.map(_ + database(name)).find(_.is_file).map(SQLite.open_database) } def open_database(name: String, output: Boolean = false): SQL.Database = access_database(name, output = output) getOrElse error("Missing build database for session " + quote(name)) def clean_output(name: String): (Boolean, Boolean) = { val relevant_db = database_server && { access_database(name) match { case Some(db) => try { db.transaction { val relevant_db = has_session_info(db, name) init_session_info(db, name) relevant_db } } finally { db.close } case None => false } } val del = for { dir <- (if (system_heaps) List(user_output_dir, system_output_dir) else List(user_output_dir)) file <- List(heap(name), database(name), log(name), log_gz(name)) path = dir + file if path.is_file } yield path.file.delete val relevant = relevant_db || del.nonEmpty val ok = del.forall(b => b) (relevant, ok) } /* SQL database content */ def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes = db.using_statement(Session_Info.table.select(List(column), Session_Info.session_name.where_equal(name)))(stmt => { val res = stmt.execute_query() if (!res.next()) Bytes.empty else res.bytes(column) }) def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] = Properties.uncompress( read_bytes(db, name, column), cache = xz_cache, xml_cache = Some(xml_cache)) /* session info */ def init_session_info(db: SQL.Database, name: String) { db.transaction { db.create_table(Session_Info.table) db.using_statement( Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute) db.create_table(Export.Data.table) db.using_statement( Export.Data.table.delete(Export.Data.session_name.where_equal(name)))(_.execute) } } def has_session_info(db: SQL.Database, name: String): Boolean = { db.transaction { db.tables.contains(Session_Info.table.name) && { db.using_statement( Session_Info.table.select(List(Session_Info.session_name), Session_Info.session_name.where_equal(name)))(stmt => stmt.execute_query().next()) } } } def write_session_info( db: SQL.Database, name: String, build_log: Build_Log.Session_Info, build: Build.Session_Info) { db.transaction { db.using_statement(Session_Info.table.insert())(stmt => { stmt.string(1) = name stmt.bytes(2) = Properties.encode(build_log.session_timing) stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = xz_cache) stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = xz_cache) stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = xz_cache) stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = xz_cache) stmt.bytes(7) = Build_Log.compress_errors(build_log.errors, cache = xz_cache) stmt.string(8) = build.sources stmt.string(9) = cat_lines(build.input_heaps) stmt.string(10) = build.output_heap getOrElse "" stmt.int(11) = build.return_code stmt.execute() }) } } def read_session_timing(db: SQL.Database, name: String): Properties.T = Properties.decode(read_bytes(db, name, Session_Info.session_timing), Some(xml_cache)) def read_command_timings(db: SQL.Database, name: String): List[Properties.T] = read_properties(db, name, Session_Info.command_timings) def read_theory_timings(db: SQL.Database, name: String): List[Properties.T] = read_properties(db, name, Session_Info.theory_timings) def read_ml_statistics(db: SQL.Database, name: String): List[Properties.T] = read_properties(db, name, Session_Info.ml_statistics) def read_task_statistics(db: SQL.Database, name: String): List[Properties.T] = read_properties(db, name, Session_Info.task_statistics) def read_errors(db: SQL.Database, name: String): List[String] = Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors), cache = xz_cache) def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] = { if (db.tables.contains(Session_Info.table.name)) { db.using_statement(Session_Info.table.select(Session_Info.build_columns, Session_Info.session_name.where_equal(name)))(stmt => { val res = stmt.execute_query() if (!res.next()) None else { Some( Build.Session_Info( res.string(Session_Info.sources), split_lines(res.string(Session_Info.input_heaps)), res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) }, res.int(Session_Info.return_code))) } }) } else None } } } diff --git a/src/Pure/Tools/server_commands.scala b/src/Pure/Tools/server_commands.scala --- a/src/Pure/Tools/server_commands.scala +++ b/src/Pure/Tools/server_commands.scala @@ -1,346 +1,345 @@ /* Title: Pure/Tools/server_commands.scala Author: Makarius Miscellaneous Isabelle server commands. */ package isabelle object Server_Commands { def default_preferences: String = Options.read_prefs() object Help extends Server.Command("help") { override val command_body: Server.Command_Body = { case (context, ()) => context.command_list } } object Echo extends Server.Command("echo") { override val command_body: Server.Command_Body = { case (_, t) => t } } object Cancel extends Server.Command("cancel") { sealed case class Args(task: UUID.T) def unapply(json: JSON.T): Option[Args] = for { task <- JSON.uuid(json, "task") } yield Args(task) override val command_body: Server.Command_Body = { case (context, Cancel(args)) => context.cancel_task(args.task) } } object Shutdown extends Server.Command("shutdown") { override val command_body: Server.Command_Body = { case (context, ()) => context.server.shutdown() } } object Session_Build extends Server.Command("session_build") { sealed case class Args( session: String, preferences: String = default_preferences, options: List[String] = Nil, dirs: List[String] = Nil, include_sessions: List[String] = Nil, verbose: Boolean = false) def unapply(json: JSON.T): Option[Args] = for { session <- JSON.string(json, "session") preferences <- JSON.string_default(json, "preferences", default_preferences) options <- JSON.strings_default(json, "options") dirs <- JSON.strings_default(json, "dirs") include_sessions <- JSON.strings_default(json, "include_sessions") verbose <- JSON.bool_default(json, "verbose") } yield { Args(session, preferences = preferences, options = options, dirs = dirs, include_sessions = include_sessions, verbose = verbose) } def command(args: Args, progress: Progress = new Progress) : (JSON.Object.T, Build.Results, Options, Sessions.Base_Info) = { val options = Options.init(prefs = args.preferences, opts = args.options) val dirs = args.dirs.map(Path.explode) val base_info = Sessions.base_info(options, args.session, progress = progress, dirs = dirs, - include_sessions = args.include_sessions) - val base = base_info.check_base + include_sessions = args.include_sessions).check val results = Build.build(options, selection = Sessions.Selection.session(args.session), progress = progress, build_heap = true, dirs = dirs, infos = base_info.infos, verbose = args.verbose) val sessions_order = base_info.sessions_structure.imports_topological_order.zipWithIndex. toMap.withDefaultValue(-1) val results_json = JSON.Object( "ok" -> results.ok, "return_code" -> results.rc, "sessions" -> results.sessions.toList.sortBy(sessions_order).map(session => { val result = results(session) JSON.Object( "session" -> session, "ok" -> result.ok, "return_code" -> result.rc, "timeout" -> result.timeout, "timing" -> result.timing.json) })) if (results.ok) (results_json, results, options, base_info) else { throw new Server.Error("Session build failed: " + Process_Result.print_rc(results.rc), results_json) } } override val command_body: Server.Command_Body = { case (context, Session_Build(args)) => context.make_task(task => Session_Build.command(args, progress = task.progress)._1) } } object Session_Start extends Server.Command("session_start") { sealed case class Args( build: Session_Build.Args, print_mode: List[String] = Nil) def unapply(json: JSON.T): Option[Args] = for { build <- Session_Build.unapply(json) print_mode <- JSON.strings_default(json, "print_mode") } yield Args(build = build, print_mode = print_mode) def command(args: Args, progress: Progress = new Progress, log: Logger = No_Logger) : (JSON.Object.T, (UUID.T, Headless.Session)) = { val (_, _, options, base_info) = try { Session_Build.command(args.build, progress = progress) } catch { case exn: Server.Error => error(exn.message) } val resources = Headless.Resources(options, base_info, log = log) val session = resources.start_session(print_mode = args.print_mode, progress = progress) val id = UUID.random() val res = JSON.Object( "session_id" -> id.toString, "tmp_dir" -> File.path(session.tmp_dir).implode) (res, id -> session) } override val command_body: Server.Command_Body = { case (context, Session_Start(args)) => context.make_task(task => { val (res, entry) = Session_Start.command(args, progress = task.progress, log = context.server.log) context.server.add_session(entry) res }) } } object Session_Stop extends Server.Command("session_stop") { def unapply(json: JSON.T): Option[UUID.T] = JSON.uuid(json, "session_id") def command(session: Headless.Session): (JSON.Object.T, Process_Result) = { val result = session.stop() val result_json = JSON.Object("ok" -> result.ok, "return_code" -> result.rc) if (result.ok) (result_json, result) else throw new Server.Error("Session shutdown failed: " + result.print_rc, result_json) } override val command_body: Server.Command_Body = { case (context, Session_Stop(id)) => context.make_task(_ => { val session = context.server.remove_session(id) Session_Stop.command(session)._1 }) } } object Use_Theories extends Server.Command("use_theories") { sealed case class Args( session_id: UUID.T, theories: List[String], master_dir: String = "", pretty_margin: Double = Pretty.default_margin, unicode_symbols: Boolean = false, export_pattern: String = "", check_delay: Option[Time] = None, check_limit: Option[Int] = None, watchdog_timeout: Option[Time] = None, nodes_status_delay: Option[Time] = None, commit_cleanup_delay: Option[Time] = None) def unapply(json: JSON.T): Option[Args] = for { session_id <- JSON.uuid(json, "session_id") theories <- JSON.strings(json, "theories") master_dir <- JSON.string_default(json, "master_dir") pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin) unicode_symbols <- JSON.bool_default(json, "unicode_symbols") export_pattern <- JSON.string_default(json, "export_pattern") check_delay = JSON.seconds(json, "check_delay") check_limit = JSON.int(json, "check_limit") watchdog_timeout = JSON.seconds(json, "watchdog_timeout") nodes_status_delay = JSON.seconds(json, "nodes_status_delay") commit_cleanup_delay = JSON.seconds(json, "commit_cleanup_delay") } yield { Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin, unicode_symbols = unicode_symbols, export_pattern = export_pattern, check_delay = check_delay, check_limit = check_limit, watchdog_timeout = watchdog_timeout, nodes_status_delay = nodes_status_delay, commit_cleanup_delay = commit_cleanup_delay) } def command(args: Args, session: Headless.Session, id: UUID.T = UUID.random(), progress: Progress = new Progress): (JSON.Object.T, Headless.Use_Theories_Result) = { val result = session.use_theories(args.theories, master_dir = args.master_dir, check_delay = args.check_delay.getOrElse(session.default_check_delay), check_limit = args.check_limit.getOrElse(session.default_check_limit), watchdog_timeout = args.watchdog_timeout.getOrElse(session.default_watchdog_timeout), nodes_status_delay = args.nodes_status_delay.getOrElse(session.default_nodes_status_delay), commit_cleanup_delay = args.commit_cleanup_delay.getOrElse(session.default_commit_cleanup_delay), id = id, progress = progress) def output_text(s: String): String = if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s) def output_message(tree: XML.Tree, pos: Position.T): JSON.Object.T = { val position = "pos" -> Position.JSON(pos) tree match { case XML.Text(msg) => Server.Reply.message(output_text(msg)) + position case elem: XML.Elem => val msg = XML.content(Pretty.formatted(List(elem), margin = args.pretty_margin)) val kind = Markup.messages.collectFirst({ case (a, b) if b == elem.name => if (Protocol.is_legacy(elem)) Markup.WARNING else a }) getOrElse "" Server.Reply.message(output_text(msg), kind = kind) + position } } val result_json = JSON.Object( "ok" -> result.ok, "errors" -> (for { (name, status) <- result.nodes if !status.ok (tree, pos) <- result.snapshot(name).messages if Protocol.is_error(tree) } yield output_message(tree, pos)), "nodes" -> (for ((name, status) <- result.nodes) yield { val snapshot = result.snapshot(name) name.json + ("status" -> status.json) + ("messages" -> (for { (tree, pos) <- snapshot.messages if Protocol.is_exported(tree) } yield output_message(tree, pos))) + ("exports" -> (if (args.export_pattern == "") Nil else { val matcher = Export.make_matcher(args.export_pattern) for { entry <- snapshot.exports if matcher(entry.theory_name, entry.name) } yield { val (base64, body) = entry.uncompressed().maybe_base64 JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body) } })) })) (result_json, result) } override val command_body: Server.Command_Body = { case (context, Use_Theories(args)) => context.make_task(task => { val session = context.server.the_session(args.session_id) Use_Theories.command(args, session, id = task.id, progress = task.progress)._1 }) } } object Purge_Theories extends Server.Command("purge_theories") { sealed case class Args( session_id: UUID.T, theories: List[String] = Nil, master_dir: String = "", all: Boolean = false) def unapply(json: JSON.T): Option[Args] = for { session_id <- JSON.uuid(json, "session_id") theories <- JSON.strings_default(json, "theories") master_dir <- JSON.string_default(json, "master_dir") all <- JSON.bool_default(json, "all") } yield { Args(session_id, theories = theories, master_dir = master_dir, all = all) } def command(args: Args, session: Headless.Session) : (JSON.Object.T, (List[Document.Node.Name], List[Document.Node.Name])) = { val (purged, retained) = session.purge_theories( theories = args.theories, master_dir = args.master_dir, all = args.all) val result_json = JSON.Object("purged" -> purged.map(_.json), "retained" -> retained.map(_.json)) (result_json, (purged, retained)) } override val command_body: Server.Command_Body = { case (context, Purge_Theories(args)) => val session = context.server.the_session(args.session_id) command(args, session)._1 } } } class Server_Commands extends Server.Commands( Server_Commands.Help, Server_Commands.Echo, Server_Commands.Cancel, Server_Commands.Shutdown, Server_Commands.Session_Build, Server_Commands.Session_Start, Server_Commands.Session_Stop, Server_Commands.Use_Theories, Server_Commands.Purge_Theories) diff --git a/src/Tools/VSCode/src/build_vscode.scala b/src/Tools/VSCode/src/build_vscode.scala --- a/src/Tools/VSCode/src/build_vscode.scala +++ b/src/Tools/VSCode/src/build_vscode.scala @@ -1,74 +1,74 @@ /* Title: Tools/VSCode/src/build_vscode.scala Author: Makarius Build VSCode configuration and extension module for Isabelle. */ package isabelle.vscode import isabelle._ object Build_VSCode { val extension_dir = Path.explode("~~/src/Tools/VSCode/extension") /* grammar */ def build_grammar(options: Options, progress: Progress = new Progress) { val logic = Grammar.default_logic - val keywords = Sessions.base_info(options, logic).check_base.overall_syntax.keywords + val keywords = Sessions.base_info(options, logic).check.base.overall_syntax.keywords val output_path = extension_dir + Path.explode(Grammar.default_output(logic)) progress.echo(output_path.implode) File.write_backup(output_path, Grammar.generate(keywords)) } /* extension */ def build_extension(progress: Progress = new Progress, publish: Boolean = false) { val output_path = extension_dir + Path.explode("out") progress.echo(output_path.implode) progress.bash( "npm install && npm update --dev && vsce package" + (if (publish) " && vsce publish" else ""), cwd = extension_dir.file, echo = true).check } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_vscode", "build Isabelle/VSCode extension module", args => { var publish = false val getopts = Getopts(""" Usage: isabelle build_vscode Options are: -P publish the package Build Isabelle/VSCode extension module in directory """ + extension_dir.expand + """ This requires npm and the vsce build and publishing tool, see also https://code.visualstudio.com/docs/tools/vscecli """, "P" -> (_ => publish = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val options = Options.init() val progress = new Console_Progress() build_grammar(options, progress) build_extension(progress, publish = publish) }) } diff --git a/src/Tools/VSCode/src/grammar.scala b/src/Tools/VSCode/src/grammar.scala --- a/src/Tools/VSCode/src/grammar.scala +++ b/src/Tools/VSCode/src/grammar.scala @@ -1,167 +1,167 @@ /* Title: Tools/VSCode/src/grammar.scala Author: Makarius Generate static TextMate grammar for VSCode editor. */ package isabelle.vscode import isabelle._ object Grammar { /* generate grammar */ lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC") def default_output(logic: String = ""): String = if (logic == "" || logic == default_logic) "isabelle-grammar.json" else "isabelle-" + logic + "-grammar.json" def generate(keywords: Keyword.Keywords): JSON.S = { val (minor_keywords, operators) = keywords.minor.iterator.toList.partition(Symbol.is_ascii_identifier) def major_keywords(pred: String => Boolean): List[String] = (for { k <- keywords.major.iterator kind <- keywords.kinds.get(k) if pred(kind) } yield k).toList val keywords1 = major_keywords(k => k != Keyword.THY_END && k != Keyword.PRF_ASM && k != Keyword.PRF_ASM_GOAL) val keywords2 = minor_keywords ::: major_keywords(Set(Keyword.THY_END)) val keywords3 = major_keywords(Set(Keyword.PRF_ASM, Keyword.PRF_ASM_GOAL)) def grouped_names(as: List[String]): String = JSON.Format("\\b(" + as.sorted.map(Library.escape_regex).mkString("|") + ")\\b") """{ "name": "Isabelle", "scopeName": "source.isabelle", "fileTypes": ["thy"], "uuid": """ + JSON.Format(UUID.random_string()) + """, "repository": { "comment": { "patterns": [ { "name": "comment.block.isabelle", "begin": "\\(\\*", "patterns": [{ "include": "#comment" }], "end": "\\*\\)" } ] }, "cartouche": { "patterns": [ { "name": "string.quoted.other.multiline.isabelle", "begin": "(?:\\\\|‹)", "patterns": [{ "include": "#cartouche" }], "end": "(?:\\\\|›)" } ] } }, "patterns": [ { "include": "#comment" }, { "include": "#cartouche" }, { "name": "keyword.control.isabelle", "match": """ + grouped_names(keywords1) + """ }, { "name": "keyword.other.unit.isabelle", "match": """ + grouped_names(keywords2) + """ }, { "name": "keyword.operator.isabelle", "match": """ + grouped_names(operators) + """ }, { "name": "entity.name.type.isabelle", "match": """ + grouped_names(keywords3) + """ }, { "name": "constant.numeric.isabelle", "match": "\\b\\d*\\.?\\d+\\b" }, { "name": "string.quoted.double.isabelle", "begin": "\"", "patterns": [ { "name": "constant.character.escape.isabelle", "match": """ + JSON.Format("""\\[\"]|\\\d\d\d""") + """ } ], "end": "\"" }, { "name": "string.quoted.backtick.isabelle", "begin": "`", "patterns": [ { "name": "constant.character.escape.isabelle", "match": """ + JSON.Format("""\\[\`]|\\\d\d\d""") + """ } ], "end": "`" }, { "name": "string.quoted.verbatim.isabelle", "begin": """ + JSON.Format("""\{\*""") + """, "patterns": [ { "match": """ + JSON.Format("""[^*]+|\*(?!\})""") + """ } ], "end": """ + JSON.Format("""\*\}""") + """ } ] } """ } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("vscode_grammar", "generate static TextMate grammar for VSCode editor", args => { var dirs: List[Path] = Nil var logic = default_logic var output: Option[Path] = None val getopts = Getopts(""" Usage: isabelle vscode_grammar [OPTIONS] Options are: -d DIR include session directory -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """) -o FILE output file name (default """ + default_output() + """) Generate static TextMate grammar for VSCode editor. """, "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "l:" -> (arg => logic = arg), "o:" -> (arg => output = Some(Path.explode(arg)))) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val keywords = - Sessions.base_info(Options.init(), logic, dirs = dirs).check_base.overall_syntax.keywords + Sessions.base_info(Options.init(), logic, dirs = dirs).check.base.overall_syntax.keywords val output_path = output getOrElse Path.explode(default_output(logic)) Output.writeln(output_path.implode) File.write_backup(output_path, generate(keywords)) }) } diff --git a/src/Tools/VSCode/src/server.scala b/src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala +++ b/src/Tools/VSCode/src/server.scala @@ -1,562 +1,560 @@ /* Title: Tools/VSCode/src/server.scala Author: Makarius Server for VS Code Language Server Protocol 2.0/3.0, see also https://github.com/Microsoft/language-server-protocol https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md PIDE protocol extensions depend on system option "vscode_pide_extensions". */ package isabelle.vscode import isabelle._ import java.io.{PrintStream, OutputStream, File => JFile} import scala.annotation.tailrec import scala.collection.mutable object Server { type Editor = isabelle.Editor[Unit] /* Isabelle tool wrapper */ private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC") val isabelle_tool = Isabelle_Tool("vscode_server", "VSCode Language Server for PIDE", args => { try { var logic_ancestor: Option[String] = None var log_file: Option[Path] = None var logic_requirements = false var dirs: List[Path] = Nil var include_sessions: List[String] = Nil var logic = default_logic var modes: List[String] = Nil var options = Options.init() var verbose = false val getopts = Getopts(""" Usage: isabelle vscode_server [OPTIONS] Options are: -A NAME ancestor session for option -R (default: parent) -L FILE logging on FILE -R NAME build image with requirements from other sessions -d DIR include session directory -i NAME include session in name-space of theories -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """) -m MODE add print mode for output -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose logging Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout. """, "A:" -> (arg => logic_ancestor = Some(arg)), "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))), "R:" -> (arg => { logic = arg; logic_requirements = true }), "d:" -> (arg => dirs = dirs ::: List(Path.explode(File.standard_path(arg)))), "i:" -> (arg => include_sessions = include_sessions ::: List(arg)), "l:" -> (arg => logic = arg), "m:" -> (arg => modes = arg :: modes), "o:" -> (arg => options = options + arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val log = Logger.make(log_file) val channel = new Channel(System.in, System.out, log, verbose) val server = new Server(channel, options, session_name = logic, session_dirs = dirs, include_sessions = include_sessions, session_ancestor = logic_ancestor, session_requirements = logic_requirements, modes = modes, log = log) // prevent spurious garbage on the main protocol channel val orig_out = System.out try { System.setOut(new PrintStream(new OutputStream { def write(n: Int) {} })) server.start() } finally { System.setOut(orig_out) } } catch { case exn: Throwable => val channel = new Channel(System.in, System.out, No_Logger) channel.error_message(Exn.message(exn)) throw(exn) } }) } class Server( val channel: Channel, options: Options, session_name: String = Server.default_logic, session_dirs: List[Path] = Nil, include_sessions: List[String] = Nil, session_ancestor: Option[String] = None, session_requirements: Boolean = false, modes: List[String] = Nil, log: Logger = No_Logger) { server => /* prover session */ private val session_ = Synchronized(None: Option[Session]) def session: Session = session_.value getOrElse error("Server inactive") def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources] def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] = for { model <- resources.get_model(new JFile(node_pos.name)) rendering = model.rendering() offset <- model.content.doc.offset(node_pos.pos) } yield (rendering, offset) private val dynamic_output = Dynamic_Output(server) /* input from client or file-system */ private val delay_input: Delay = Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger) { resources.flush_input(session, channel) } private val delay_load: Delay = Delay.last(options.seconds("vscode_load_delay"), channel.Error_Logger) { val (invoke_input, invoke_load) = resources.resolve_dependencies(session, editor, file_watcher) if (invoke_input) delay_input.invoke() if (invoke_load) delay_load.invoke } private val file_watcher = File_Watcher(sync_documents, options.seconds("vscode_load_delay")) private def close_document(file: JFile) { if (resources.close_model(file)) { file_watcher.register_parent(file) sync_documents(Set(file)) delay_input.invoke() delay_output.invoke() } } private def sync_documents(changed: Set[JFile]) { resources.sync_models(changed) delay_input.invoke() delay_output.invoke() } private def change_document(file: JFile, version: Long, changes: List[Protocol.TextDocumentChange]) { val norm_changes = new mutable.ListBuffer[Protocol.TextDocumentChange] @tailrec def norm(chs: List[Protocol.TextDocumentChange]) { if (chs.nonEmpty) { val (full_texts, rest1) = chs.span(_.range.isEmpty) val (edits, rest2) = rest1.span(_.range.nonEmpty) norm_changes ++= full_texts norm_changes ++= edits.sortBy(_.range.get.start)(Line.Position.Ordering).reverse norm(rest2) } } norm(changes) norm_changes.foreach(change => resources.change_model(session, editor, file, version, change.text, change.range)) delay_input.invoke() delay_output.invoke() } /* caret handling */ private val delay_caret_update: Delay = Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger) { session.caret_focus.post(Session.Caret_Focus) } private def update_caret(caret: Option[(JFile, Line.Position)]) { resources.update_caret(caret) delay_caret_update.invoke() delay_input.invoke() } /* preview */ private lazy val preview_panel = new Preview_Panel(resources) private lazy val delay_preview: Delay = Delay.last(options.seconds("vscode_output_delay"), channel.Error_Logger) { if (preview_panel.flush(channel)) delay_preview.invoke() } private def request_preview(file: JFile, column: Int) { preview_panel.request(file, column) delay_preview.invoke() } /* output to client */ private val delay_output: Delay = Delay.last(options.seconds("vscode_output_delay"), channel.Error_Logger) { if (resources.flush_output(channel)) delay_output.invoke() } def update_output(changed_nodes: Traversable[JFile]) { resources.update_output(changed_nodes) delay_output.invoke() } def update_output_visible() { resources.update_output_visible() delay_output.invoke() } private val prover_output = Session.Consumer[Session.Commands_Changed](getClass.getName) { case changed => update_output(changed.nodes.toList.map(resources.node_file(_))) } private val syslog_messages = Session.Consumer[Prover.Output](getClass.getName) { case output => channel.log_writeln(resources.output_xml(output.message)) } /* init and exit */ def init(id: Protocol.Id) { def reply_ok(msg: String) { channel.write(Protocol.Initialize.reply(id, "")) channel.writeln(msg) } def reply_error(msg: String) { channel.write(Protocol.Initialize.reply(id, msg)) channel.error_message(msg) } val try_session = try { val base_info = Sessions.base_info( options, session_name, dirs = session_dirs, include_sessions = include_sessions, - session_ancestor = session_ancestor, session_requirements = session_requirements) - - base_info.check_base + session_ancestor = session_ancestor, session_requirements = session_requirements).check def build(no_build: Boolean = false): Build.Results = Build.build(options, selection = Sessions.Selection.session(base_info.session), build_heap = true, no_build = no_build, dirs = session_dirs, infos = base_info.infos) if (!build(no_build = true).ok) { val start_msg = "Build started for Isabelle/" + base_info.session + " ..." val fail_msg = "Session build failed -- prover process remains inactive!" val progress = channel.progress(verbose = true) progress.echo(start_msg); channel.writeln(start_msg) if (!build().ok) { progress.echo(fail_msg); error(fail_msg) } } val resources = new VSCode_Resources(options, base_info, log) { override def commit(change: Session.Change): Unit = if (change.deps_changed || undefined_blobs(change.version.nodes).nonEmpty) delay_load.invoke() } val session_options = options.bool("editor_output_state") = true val session = new Session(session_options, resources) Some((base_info, session)) } catch { case ERROR(msg) => reply_error(msg); None } for ((base_info, session) <- try_session) { session_.change(_ => Some(session)) session.commands_changed += prover_output session.syslog_messages += syslog_messages dynamic_output.init() try { Isabelle_Process(session, options, base_info.sessions_structure, Sessions.store(options), modes = modes, logic = base_info.session).await_startup reply_ok("Welcome to Isabelle/" + base_info.session + " (" + Distribution.version + ")") } catch { case ERROR(msg) => reply_error(msg) } } } def shutdown(id: Protocol.Id) { def reply(err: String): Unit = channel.write(Protocol.Shutdown.reply(id, err)) session_.change({ case Some(session) => session.commands_changed -= prover_output session.syslog_messages -= syslog_messages dynamic_output.exit() delay_load.revoke() file_watcher.shutdown() delay_input.revoke() delay_output.revoke() delay_caret_update.revoke() delay_preview.revoke() val result = session.stop() if (result.ok) reply("") else reply("Prover shutdown failed: " + result.rc) None case None => reply("Prover inactive") None }) } def exit() { log("\n") sys.exit(if (session_.value.isDefined) 2 else 0) } /* completion */ def completion(id: Protocol.Id, node_pos: Line.Node_Position) { val result = (for ((rendering, offset) <- rendering_offset(node_pos)) yield rendering.completion(node_pos.pos, offset)) getOrElse Nil channel.write(Protocol.Completion.reply(id, result)) } /* spell-checker dictionary */ def update_dictionary(include: Boolean, permanent: Boolean) { for { spell_checker <- resources.spell_checker.get caret <- resources.get_caret() rendering = caret.model.rendering() range = rendering.before_caret_range(caret.offset) Text.Info(_, word) <- Spell_Checker.current_word(rendering, range) } { spell_checker.update(word, include, permanent) update_output_visible() } } def reset_dictionary() { for (spell_checker <- resources.spell_checker.get) { spell_checker.reset() update_output_visible() } } /* hover */ def hover(id: Protocol.Id, node_pos: Line.Node_Position) { val result = for { (rendering, offset) <- rendering_offset(node_pos) info <- rendering.tooltips(VSCode_Rendering.tooltip_elements, Text.Range(offset, offset + 1)) } yield { val range = rendering.model.content.doc.range(info.range) val contents = info.info.map(t => Protocol.MarkedString(resources.output_pretty_tooltip(List(t)))) (range, contents) } channel.write(Protocol.Hover.reply(id, result)) } /* goto definition */ def goto_definition(id: Protocol.Id, node_pos: Line.Node_Position) { val result = (for ((rendering, offset) <- rendering_offset(node_pos)) yield rendering.hyperlinks(Text.Range(offset, offset + 1))) getOrElse Nil channel.write(Protocol.GotoDefinition.reply(id, result)) } /* document highlights */ def document_highlights(id: Protocol.Id, node_pos: Line.Node_Position) { val result = (for ((rendering, offset) <- rendering_offset(node_pos)) yield { val model = rendering.model rendering.caret_focus_ranges(Text.Range(offset, offset + 1), model.content.text_range) .map(r => Protocol.DocumentHighlight.text(model.content.doc.range(r))) }) getOrElse Nil channel.write(Protocol.DocumentHighlights.reply(id, result)) } /* main loop */ def start() { log("Server started " + Date.now()) def handle(json: JSON.T) { try { json match { case Protocol.Initialize(id) => init(id) case Protocol.Initialized(()) => case Protocol.Shutdown(id) => shutdown(id) case Protocol.Exit(()) => exit() case Protocol.DidOpenTextDocument(file, _, version, text) => change_document(file, version, List(Protocol.TextDocumentChange(None, text))) delay_load.invoke() case Protocol.DidChangeTextDocument(file, version, changes) => change_document(file, version, changes) case Protocol.DidCloseTextDocument(file) => close_document(file) case Protocol.Completion(id, node_pos) => completion(id, node_pos) case Protocol.Include_Word(()) => update_dictionary(true, false) case Protocol.Include_Word_Permanently(()) => update_dictionary(true, true) case Protocol.Exclude_Word(()) => update_dictionary(false, false) case Protocol.Exclude_Word_Permanently(()) => update_dictionary(false, true) case Protocol.Reset_Words(()) => reset_dictionary() case Protocol.Hover(id, node_pos) => hover(id, node_pos) case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos) case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos) case Protocol.Caret_Update(caret) => update_caret(caret) case Protocol.State_Init(()) => State_Panel.init(server) case Protocol.State_Exit(id) => State_Panel.exit(id) case Protocol.State_Locate(id) => State_Panel.locate(id) case Protocol.State_Update(id) => State_Panel.update(id) case Protocol.State_Auto_Update(id, enabled) => State_Panel.auto_update(id, enabled) case Protocol.Preview_Request(file, column) => request_preview(file, column) case Protocol.Symbols_Request(()) => channel.write(Protocol.Symbols()) case _ => if (!Protocol.ResponseMessage.is_empty(json)) log("### IGNORED") } } catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) } } @tailrec def loop() { channel.read() match { case Some(json) => json match { case bulk: List[_] => bulk.foreach(handle) case _ => handle(json) } loop() case None => log("### TERMINATE") } } loop() } /* abstract editor operations */ object editor extends Server.Editor { /* session */ override def session: Session = server.session override def flush(): Unit = resources.flush_input(session, channel) override def invoke(): Unit = delay_input.invoke() /* current situation */ override def current_node(context: Unit): Option[Document.Node.Name] = resources.get_caret().map(_.model.node_name) override def current_node_snapshot(context: Unit): Option[Document.Snapshot] = resources.get_caret().map(_.model.snapshot()) override def node_snapshot(name: Document.Node.Name): Document.Snapshot = { resources.get_model(name) match { case Some(model) => model.snapshot() case None => session.snapshot(name) } } def current_command(snapshot: Document.Snapshot): Option[Command] = { resources.get_caret() match { case Some(caret) => snapshot.current_command(caret.node_name, caret.offset) case None => None } } override def current_command(context: Unit, snapshot: Document.Snapshot): Option[Command] = current_command(snapshot) /* overlays */ override def node_overlays(name: Document.Node.Name): Document.Node.Overlays = resources.node_overlays(name) override def insert_overlay(command: Command, fn: String, args: List[String]): Unit = resources.insert_overlay(command, fn, args) override def remove_overlay(command: Command, fn: String, args: List[String]): Unit = resources.remove_overlay(command, fn, args) /* hyperlinks */ override def hyperlink_command( focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0): Option[Hyperlink] = { if (snapshot.is_outdated) None else snapshot.find_command_position(id, offset).map(node_pos => new Hyperlink { def follow(unit: Unit) { channel.write(Protocol.Caret_Update(node_pos, focus)) } }) } /* dispatcher thread */ override def assert_dispatcher[A](body: => A): A = session.assert_dispatcher(body) override def require_dispatcher[A](body: => A): A = session.require_dispatcher(body) override def send_dispatcher(body: => Unit): Unit = session.send_dispatcher(body) override def send_wait_dispatcher(body: => Unit): Unit = session.send_wait_dispatcher(body) } } diff --git a/src/Tools/VSCode/src/vscode_resources.scala b/src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala +++ b/src/Tools/VSCode/src/vscode_resources.scala @@ -1,373 +1,373 @@ /* Title: Tools/VSCode/src/vscode_resources.scala Author: Makarius Resources for VSCode Language Server: file-system access and global state. */ package isabelle.vscode import isabelle._ import java.io.{File => JFile} import scala.util.parsing.input.Reader object VSCode_Resources { /* internal state */ sealed case class State( models: Map[JFile, Document_Model] = Map.empty, caret: Option[(JFile, Line.Position)] = None, overlays: Document.Overlays = Document.Overlays.empty, pending_input: Set[JFile] = Set.empty, pending_output: Set[JFile] = Set.empty) { def update_models(changed: Traversable[(JFile, Document_Model)]): State = copy( models = models ++ changed, pending_input = (pending_input /: changed) { case (set, (file, _)) => set + file }, pending_output = (pending_output /: changed) { case (set, (file, _)) => set + file }) def update_caret(new_caret: Option[(JFile, Line.Position)]): State = if (caret == new_caret) this else copy( caret = new_caret, pending_input = pending_input ++ caret.map(_._1) ++ new_caret.map(_._1)) def get_caret(file: JFile): Option[Line.Position] = caret match { case Some((caret_file, caret_pos)) if caret_file == file => Some(caret_pos) case _ => None } lazy val document_blobs: Document.Blobs = Document.Blobs( (for { (_, model) <- models.iterator blob <- model.get_blob } yield (model.node_name -> blob)).toMap) def change_overlay(insert: Boolean, file: JFile, command: Command, fn: String, args: List[String]): State = copy( overlays = if (insert) overlays.insert(command, fn, args) else overlays.remove(command, fn, args), pending_input = pending_input + file) } /* caret */ sealed case class Caret(file: JFile, model: Document_Model, offset: Text.Offset) { def node_name: Document.Node.Name = model.node_name } } class VSCode_Resources( val options: Options, session_base_info: Sessions.Base_Info, log: Logger = No_Logger) - extends Resources(session_base_info.sessions_structure, session_base_info.check_base, log = log) + extends Resources(session_base_info.sessions_structure, session_base_info.check.base, log = log) { resources => private val state = Synchronized(VSCode_Resources.State()) /* options */ def pide_extensions: Boolean = options.bool("vscode_pide_extensions") def unicode_symbols: Boolean = options.bool("vscode_unicode_symbols") def tooltip_margin: Int = options.int("vscode_tooltip_margin") def message_margin: Int = options.int("vscode_message_margin") /* document node name */ def node_file(name: Document.Node.Name): JFile = new JFile(name.node) def node_name(file: JFile): Document.Node.Name = find_theory(file) getOrElse { val node = file.getPath val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) if (session_base.loaded_theory(theory)) loaded_theory_node(theory) else { val master_dir = file.getParent Document.Node.Name(node, master_dir, theory) } } override def append(dir: String, source_path: Path): String = { val path = source_path.expand if (dir == "" || path.is_absolute) File.platform_path(path) else if (path.is_current) dir else if (path.is_basic && !dir.endsWith("/") && !dir.endsWith(JFile.separator)) dir + JFile.separator + File.platform_path(path) else if (path.is_basic) dir + File.platform_path(path) else File.absolute_name(new JFile(dir + JFile.separator + File.platform_path(path))) } def get_models: Map[JFile, Document_Model] = state.value.models def get_model(file: JFile): Option[Document_Model] = get_models.get(file) def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name)) /* file content */ def read_file_content(name: Document.Node.Name): Option[String] = { make_theory_content(name) orElse { try { Some(Line.normalize(File.read(node_file(name)))) } catch { case ERROR(_) => None } } } def get_file_content(name: Document.Node.Name): Option[String] = get_model(name) match { case Some(model) => Some(model.content.text) case None => read_file_content(name) } override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = { val file = node_file(name) get_model(file) match { case Some(model) => f(Scan.char_reader(model.content.text)) case None if file.isFile => using(Scan.byte_reader(file))(f) case None => error("No such file: " + quote(file.toString)) } } /* document models */ def visible_node(name: Document.Node.Name): Boolean = get_model(name) match { case Some(model) => model.node_visible case None => false } def change_model( session: Session, editor: Server.Editor, file: JFile, version: Long, text: String, range: Option[Line.Range] = None) { state.change(st => { val model = st.models.getOrElse(file, Document_Model.init(session, editor, node_name(file))) val model1 = (model.change_text(text, range) getOrElse model).set_version(version).external(false) st.update_models(Some(file -> model1)) }) } def close_model(file: JFile): Boolean = state.change_result(st => st.models.get(file) match { case None => (false, st) case Some(model) => (true, st.update_models(Some(file -> model.external(true)))) }) def sync_models(changed_files: Set[JFile]): Unit = state.change(st => { val changed_models = (for { (file, model) <- st.models.iterator if changed_files(file) && model.external_file text <- read_file_content(model.node_name) model1 <- model.change_text(text) } yield (file, model1)).toList st.update_models(changed_models) }) /* overlays */ def node_overlays(name: Document.Node.Name): Document.Node.Overlays = state.value.overlays(name) def insert_overlay(command: Command, fn: String, args: List[String]): Unit = state.change(_.change_overlay(true, node_file(command.node_name), command, fn, args)) def remove_overlay(command: Command, fn: String, args: List[String]): Unit = state.change(_.change_overlay(false, node_file(command.node_name), command, fn, args)) /* resolve dependencies */ def resolve_dependencies( session: Session, editor: Server.Editor, file_watcher: File_Watcher): (Boolean, Boolean) = { state.change_result(st => { /* theory files */ val thys = (for ((_, model) <- st.models.iterator if model.is_theory) yield (model.node_name, Position.none)).toList val thy_files1 = resources.dependencies(thys).theories val thy_files2 = (for { (_, model) <- st.models.iterator thy_name <- resources.make_theory_name(model.node_name) } yield thy_name).toList /* auxiliary files */ val stable_tip_version = if (st.models.forall(entry => entry._2.is_stable)) session.get_state().stable_tip_version else None val aux_files = stable_tip_version match { case Some(version) => undefined_blobs(version.nodes) case None => Nil } /* loaded models */ val loaded_models = (for { node_name <- thy_files1.iterator ++ thy_files2.iterator ++ aux_files.iterator file = node_file(node_name) if !st.models.isDefinedAt(file) text <- { file_watcher.register_parent(file); read_file_content(node_name) } } yield { val model = Document_Model.init(session, editor, node_name) val model1 = (model.change_text(text) getOrElse model).external(true) (file, model1) }).toList val invoke_input = loaded_models.nonEmpty val invoke_load = stable_tip_version.isEmpty ((invoke_input, invoke_load), st.update_models(loaded_models)) }) } /* pending input */ def flush_input(session: Session, channel: Channel) { state.change(st => { val changed_models = (for { file <- st.pending_input.iterator model <- st.models.get(file) (edits, model1) <- model.flush_edits(unicode_symbols, st.document_blobs, file, st.get_caret(file)) } yield (edits, (file, model1))).toList for { ((workspace_edits, _), _) <- changed_models if workspace_edits.nonEmpty } channel.write(Protocol.WorkspaceEdit(workspace_edits)) session.update(st.document_blobs, changed_models.flatMap(res => res._1._2)) st.copy( models = st.models ++ changed_models.iterator.map(_._2), pending_input = Set.empty) }) } /* pending output */ def update_output(changed_nodes: Traversable[JFile]): Unit = state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes)) def update_output_visible(): Unit = state.change(st => st.copy(pending_output = st.pending_output ++ (for ((file, model) <- st.models.iterator if model.node_visible) yield file))) def flush_output(channel: Channel): Boolean = { state.change_result(st => { val (postponed, flushed) = (for { file <- st.pending_output.iterator model <- st.models.get(file) } yield (file, model, model.rendering())).toList.partition(_._3.snapshot.is_outdated) val changed_iterator = for { (file, model, rendering) <- flushed.iterator (changed_diags, changed_decos, model1) = model.publish(rendering) if changed_diags.isDefined || changed_decos.isDefined } yield { for (diags <- changed_diags) channel.write(Protocol.PublishDiagnostics(file, rendering.diagnostics_output(diags))) if (pide_extensions) { for (decos <- changed_decos; deco <- decos) channel.write(rendering.decoration_output(deco).json(file)) } (file, model1) } (postponed.nonEmpty, st.copy( models = st.models ++ changed_iterator, pending_output = postponed.map(_._1).toSet)) } ) } /* output text */ def output_text(s: String): String = if (unicode_symbols) Symbol.decode(s) else Symbol.encode(s) def output_xml(xml: XML.Tree): String = output_text(XML.content(xml)) def output_pretty(body: XML.Body, margin: Int): String = output_text(Pretty.string_of(body, margin = margin, metric = Symbol.Metric)) def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin) def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin) /* caret handling */ def update_caret(caret: Option[(JFile, Line.Position)]) { state.change(_.update_caret(caret)) } def get_caret(): Option[VSCode_Resources.Caret] = { val st = state.value for { (file, pos) <- st.caret model <- st.models.get(file) offset <- model.content.doc.offset(pos) } yield VSCode_Resources.Caret(file, model, offset) } /* spell checker */ val spell_checker = new Spell_Checker_Variable spell_checker.update(options) }