diff --git a/src/Pure/PIDE/command.scala b/src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala +++ b/src/Pure/PIDE/command.scala @@ -1,582 +1,582 @@ /* Title: Pure/PIDE/command.scala Author: Fabian Immler, TU Munich Author: Makarius Prover commands with accumulated results from execution. */ package isabelle import scala.collection.mutable import scala.collection.immutable.SortedMap object Command { type Edit = (Option[Command], Option[Command]) sealed case class Blob( name: Document.Node.Name, src_path: Path, content: Option[(SHA1.Digest, Symbol.Text_Chunk)]) type Blobs_Info = (List[Exn.Result[Blob]], Int) val no_blobs: Blobs_Info = (Nil, -1) /** accumulated results from prover **/ /* results */ object Results { type Entry = (Long, XML.Tree) val empty: Results = new Results(SortedMap.empty) def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _) def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _) } final class Results private(private val rep: SortedMap[Long, XML.Tree]) { def is_empty: Boolean = rep.isEmpty def defined(serial: Long): Boolean = rep.isDefinedAt(serial) def get(serial: Long): Option[XML.Tree] = rep.get(serial) def iterator: Iterator[Results.Entry] = rep.iterator def + (entry: Results.Entry): Results = if (defined(entry._1)) this else new Results(rep + entry) def ++ (other: Results): Results = if (this eq other) this else if (rep.isEmpty) other else (this /: other.iterator)(_ + _) override def hashCode: Int = rep.hashCode override def equals(that: Any): Boolean = that match { case other: Results => rep == other.rep case _ => false } override def toString: String = iterator.mkString("Results(", ", ", ")") } /* exports */ object Exports { type Entry = (Long, Export.Entry) val empty: Exports = new Exports(SortedMap.empty) def merge(args: TraversableOnce[Exports]): Exports = (empty /: args)(_ ++ _) } final class Exports private(private val rep: SortedMap[Long, Export.Entry]) { def is_empty: Boolean = rep.isEmpty def iterator: Iterator[Exports.Entry] = rep.iterator def + (entry: Exports.Entry): Exports = if (rep.isDefinedAt(entry._1)) this else new Exports(rep + entry) def ++ (other: Exports): Exports = if (this eq other) this else if (rep.isEmpty) other else (this /: other.iterator)(_ + _) override def hashCode: Int = rep.hashCode override def equals(that: Any): Boolean = that match { case other: Exports => rep == other.rep case _ => false } override def toString: String = iterator.mkString("Exports(", ", ", ")") } /* markups */ object Markup_Index { val markup: Markup_Index = Markup_Index(false, Symbol.Text_Chunk.Default) } sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name) object Markups { val empty: Markups = new Markups(Map.empty) def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup)) def merge(args: TraversableOnce[Markups]): Markups = (empty /: args)(_ ++ _) } final class Markups private(private val rep: Map[Markup_Index, Markup_Tree]) { def is_empty: Boolean = rep.isEmpty def apply(index: Markup_Index): Markup_Tree = rep.getOrElse(index, Markup_Tree.empty) def add(index: Markup_Index, markup: Text.Markup): Markups = new Markups(rep + (index -> (this(index) + markup))) def + (entry: (Markup_Index, Markup_Tree)): Markups = { val (index, tree) = entry new Markups(rep + (index -> (this(index).merge(tree, Text.Range.full, Markup.Elements.full)))) } def ++ (other: Markups): Markups = if (this eq other) this else if (rep.isEmpty) other else (this /: other.rep.iterator)(_ + _) def redirection_iterator: Iterator[Document_ID.Generic] = for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator) yield id def redirect(other_id: Document_ID.Generic): Markups = { val rep1 = (for { (Markup_Index(status, Symbol.Text_Chunk.Id(id)), markup) <- rep.iterator if other_id == id } yield (Markup_Index(status, Symbol.Text_Chunk.Default), markup)).toMap if (rep1.isEmpty) Markups.empty else new Markups(rep1) } override def hashCode: Int = rep.hashCode override def equals(that: Any): Boolean = that match { case other: Markups => rep == other.rep case _ => false } override def toString: String = rep.iterator.mkString("Markups(", ", ", ")") } /* state */ object State { def get_result(states: List[State], serial: Long): Option[XML.Tree] = states.find(st => st.results.defined(serial)).map(st => st.results.get(serial).get) def get_result_proper(states: List[State], props: Properties.T): Option[Results.Entry] = for { serial <- Markup.Serial.unapply(props) tree @ XML.Elem(_, body) <- get_result(states, serial) if body.nonEmpty } yield (serial -> tree) def merge_results(states: List[State]): Results = Results.merge(states.map(_.results)) def merge_exports(states: List[State]): Exports = Exports.merge(states.map(_.exports)) def merge_markups(states: List[State]): Markups = Markups.merge(states.map(_.markups)) def merge_markup(states: List[State], index: Markup_Index, range: Text.Range, elements: Markup.Elements): Markup_Tree = Markup_Tree.merge(states.map(_.markup(index)), range, elements) def merge(command: Command, states: List[State]): State = State(command, states.flatMap(_.status), merge_results(states), merge_exports(states), merge_markups(states)) } sealed case class State( command: Command, status: List[Markup] = Nil, results: Results = Results.empty, exports: Exports = Exports.empty, markups: Markups = Markups.empty) { def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED) def consolidating: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATING) def consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED) lazy val maybe_consolidated: Boolean = { var touched = false var forks = 0 var runs = 0 for (markup <- status) { markup.name match { case Markup.FORKED => touched = true; forks += 1 case Markup.JOINED => forks -= 1 case Markup.RUNNING => touched = true; runs += 1 case Markup.FINISHED => runs -= 1 case _ => } } touched && forks == 0 && runs == 0 } lazy val document_status: Document_Status.Command_Status = { val warnings = if (results.iterator.exists(p => Protocol.is_warning(p._2) || Protocol.is_legacy(p._2))) List(Markup(Markup.WARNING, Nil)) else Nil val errors = if (results.iterator.exists(p => Protocol.is_error(p._2))) List(Markup(Markup.ERROR, Nil)) else Nil Document_Status.Command_Status.make((warnings ::: errors ::: status).iterator) } def markup(index: Markup_Index): Markup_Tree = markups(index) def redirect(other_command: Command): Option[State] = { val markups1 = markups.redirect(other_command.id) if (markups1.is_empty) None else Some(new State(other_command, markups = markups1)) } private def add_status(st: Markup): State = copy(status = st :: status) private def add_result(entry: Results.Entry): State = copy(results = results + entry) def add_export(entry: Exports.Entry): Option[State] = if (command.node_name.theory == entry._2.theory_name) Some(copy(exports = exports + entry)) else None private def add_markup( status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State = { val markups1 = if (status || Document_Status.Command_Status.liberal_elements(m.info.name)) markups.add(Markup_Index(true, chunk_name), m) else markups copy(markups = markups1.add(Markup_Index(false, chunk_name), m)) } def accumulate( self_id: Document_ID.Generic => Boolean, other_id: Document_ID.Generic => Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)], message: XML.Elem, xml_cache: XML.Cache): State = message match { case XML.Elem(Markup(Markup.STATUS, _), msgs) => if (command.span.is_theory) this else { (this /: msgs)((state, msg) => msg match { case elem @ XML.Elem(markup, Nil) => state. add_status(markup). add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem)) case _ => Output.warning("Ignored status message: " + msg) state }) } case XML.Elem(Markup(Markup.REPORT, atts0), msgs) => (this /: msgs)((state, msg) => { def bad(): Unit = Output.warning("Ignored report message: " + msg) msg match { case XML.Elem(Markup(name, atts1), args) => val atts = atts1 ::: atts0 command.reported_position(atts) match { case Some((id, chunk_name)) => val target = if (self_id(id) && command.chunks.isDefinedAt(chunk_name)) Some((chunk_name, command.chunks(chunk_name))) else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id) else None (target, atts) match { case (Some((target_name, target_chunk)), Position.Range(symbol_range)) => target_chunk.incorporate(symbol_range) match { case Some(range) => val props = atts.filterNot(Markup.position_property) val elem = xml_cache.elem(XML.Elem(Markup(name, props), args)) state.add_markup(false, target_name, Text.Info(range, elem)) case None => bad(); state } case _ => // silently ignore excessive reports state } case _ => bad(); state } case _ => bad(); state } }) case XML.Elem(Markup(name, props), body) => props match { case Markup.Serial(i) => val markup_message = xml_cache.elem(XML.Elem(Markup(Markup.message(name), props), body)) val message_markup = xml_cache.elem(XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL)))) var st = add_result(i -> markup_message) if (Protocol.is_inlined(message)) { for { (chunk_name, chunk) <- command.chunks.iterator range <- command.message_positions(self_id, chunk_name, chunk, message) } st = st.add_markup(false, chunk_name, Text.Info(range, message_markup)) } st case _ => Output.warning("Ignored message without serial number: " + message) this } } } /** static content **/ /* make commands */ def apply( id: Document_ID.Command, node_name: Document.Node.Name, blobs_info: Blobs_Info, span: Command_Span.Span): Command = { val (source, span1) = span.compact_source new Command(id, node_name, blobs_info, span1, source, Results.empty, Markups.empty) } val empty: Command = Command(Document_ID.none, Document.Node.Name.empty, no_blobs, Command_Span.empty) def unparsed( source: String, theory: Boolean = false, id: Document_ID.Command = Document_ID.none, node_name: Document.Node.Name = Document.Node.Name.empty, results: Results = Results.empty, markups: Markups = Markups.empty): Command = { val (source1, span1) = Command_Span.unparsed(source, theory).compact_source new Command(id, node_name, no_blobs, span1, source1, results, markups) } def text(source: String): Command = unparsed(source) def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command = unparsed(XML.content(body), id = id, results = results, markups = Markups.init(Markup_Tree.from_XML(body))) /* perspective */ object Perspective { val empty: Perspective = Perspective(Nil) } sealed case class Perspective(commands: List[Command]) // visible commands in canonical order { def is_empty: Boolean = commands.isEmpty def same(that: Perspective): Boolean = { val cmds1 = this.commands val cmds2 = that.commands require(!cmds1.exists(_.is_undefined)) require(!cmds2.exists(_.is_undefined)) cmds1.length == cmds2.length && (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id }) } } /* blobs: inlined errors and auxiliary files */ def blobs_info( resources: Resources, syntax: Outer_Syntax, get_blob: Document.Node.Name => Option[Document.Blob], can_import: Document.Node.Name => Boolean, node_name: Document.Node.Name, span: Command_Span.Span): Blobs_Info = { span.name match { // inlined errors case Thy_Header.THEORY => val reader = Scan.char_reader(Token.implode(span.content)) - val header = resources.check_thy_reader(node_name, reader) + val header = resources.check_thy(node_name, reader) val imports_pos = header.imports_pos val raw_imports = try { val read_imports = Thy_Header.read(reader, Token.Pos.none).imports if (imports_pos.length == read_imports.length) read_imports else error("") } catch { case _: Throwable => List.fill(imports_pos.length)("") } val errors = for { ((import_name, pos), s) <- imports_pos zip raw_imports if !can_import(import_name) } yield { val completion = if (Thy_Header.is_base_name(s)) resources.complete_import_name(node_name, s) else Nil val msg = "Bad theory import " + Markup.Path(import_name.node).markup(quote(import_name.toString)) + Position.here(pos) + Completion.report_theories(pos, completion) Exn.Exn[Command.Blob](ERROR(msg)) } (errors, -1) // auxiliary files case _ => val loaded_files = span.loaded_files(syntax) val blobs = loaded_files.files.map(file => (Exn.capture { val src_path = Path.explode(file) val name = Document.Node.Name(resources.append(node_name, src_path)) val content = get_blob(name).map(blob => (blob.bytes.sha1_digest, blob.chunk)) Blob(name, src_path, content) }).user_error) (blobs, loaded_files.index) } } } final class Command private( val id: Document_ID.Command, val node_name: Document.Node.Name, val blobs_info: Command.Blobs_Info, val span: Command_Span.Span, val source: String, val init_results: Command.Results, val init_markups: Command.Markups) { override def toString: String = id + "/" + span.kind.toString /* classification */ def is_proper: Boolean = span.kind.isInstanceOf[Command_Span.Command_Span] def is_ignored: Boolean = span.kind == Command_Span.Ignored_Span def is_undefined: Boolean = id == Document_ID.none val is_unparsed: Boolean = span.content.exists(_.is_unparsed) val is_unfinished: Boolean = span.content.exists(_.is_unfinished) def potentially_initialized: Boolean = span.name == Thy_Header.THEORY /* blobs */ def blobs: List[Exn.Result[Command.Blob]] = blobs_info._1 def blobs_index: Int = blobs_info._2 def blobs_ok: Boolean = blobs.forall({ case Exn.Res(_) => true case _ => false }) def blobs_names: List[Document.Node.Name] = for (Exn.Res(blob) <- blobs) yield blob.name def blobs_undefined: List[Document.Node.Name] = for (Exn.Res(blob) <- blobs if blob.content.isEmpty) yield blob.name def blobs_defined: List[(Document.Node.Name, SHA1.Digest)] = for (Exn.Res(blob) <- blobs; (digest, _) <- blob.content) yield (blob.name, digest) def blobs_changed(doc_blobs: Document.Blobs): Boolean = blobs.exists({ case Exn.Res(blob) => doc_blobs.changed(blob.name) case _ => false }) /* source chunks */ val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(source) val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] = ((Symbol.Text_Chunk.Default -> chunk) :: (for (Exn.Res(blob) <- blobs; (_, file) <- blob.content) yield Symbol.Text_Chunk.File(blob.name.node) -> file)).toMap def length: Int = source.length def range: Text.Range = chunk.range val core_range: Text.Range = Text.Range(0, (length /: span.content.reverse.iterator.takeWhile(_.is_ignored))(_ - _.source.length)) def source(range: Text.Range): String = range.substring(source) /* reported positions */ def reported_position(pos: Position.T): Option[(Document_ID.Generic, Symbol.Text_Chunk.Name)] = pos match { case Position.Id(id) => val chunk_name = pos match { case Position.File(name) if name != node_name.node => Symbol.Text_Chunk.File(name) case _ => Symbol.Text_Chunk.Default } Some((id, chunk_name)) case _ => None } def message_positions( self_id: Document_ID.Generic => Boolean, chunk_name: Symbol.Text_Chunk.Name, chunk: Symbol.Text_Chunk, message: XML.Elem): Set[Text.Range] = { def elem(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] = reported_position(props) match { case Some((id, name)) if self_id(id) && name == chunk_name => val opt_range = Position.Range.unapply(props) orElse { if (name == Symbol.Text_Chunk.Default) Position.Range.unapply(span.position) else None } opt_range match { case Some(symbol_range) => chunk.incorporate(symbol_range) match { case Some(range) => set + range case _ => set } case None => set } case _ => set } def tree(set: Set[Text.Range], t: XML.Tree): Set[Text.Range] = t match { case XML.Wrapped_Elem(Markup(name, props), _, body) => body.foldLeft(if (Rendering.position_elements(name)) elem(props, set) else set)(tree) case XML.Elem(Markup(name, props), body) => body.foldLeft(if (Rendering.position_elements(name)) elem(props, set) else set)(tree) case XML.Text(_) => set } val set = tree(Set.empty, message) if (set.isEmpty) elem(message.markup.properties, set) else set } /* accumulated results */ val init_state: Command.State = Command.State(this, results = init_results, markups = init_markups) val empty_state: Command.State = Command.State(this) } 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) { 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)) + val node_header = resources.check_thy(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/PIDE/resources.scala b/src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala +++ b/src/Pure/PIDE/resources.scala @@ -1,448 +1,447 @@ /* Title: Pure/PIDE/resources.scala Author: Makarius Resources for theories and auxiliary files. */ package isabelle import scala.util.parsing.input.Reader import java.io.{File => JFile} class Resources( val sessions_structure: Sessions.Structure, val session_base: Sessions.Base, val log: Logger = No_Logger, command_timings: List[Properties.T] = Nil) { resources => /* init session */ def init_session_yxml: String = { import XML.Encode._ YXML.string_of_body( pair(list(pair(string, properties)), pair(list(pair(string, string)), pair(list(pair(string, string)), pair(list(pair(string, list(string))), pair(list(properties), pair(list(pair(string, properties)), pair(list(pair(string, string)), list(string))))))))( (sessions_structure.session_positions, (sessions_structure.dest_session_directories, (sessions_structure.session_chapters, (sessions_structure.bibtex_entries, (command_timings, (Scala.functions.map(fun => (fun.name, fun.position)), (session_base.global_theories.toList, session_base.loaded_theories.keys))))))))) } /* file formats */ def make_theory_name(name: Document.Node.Name): Option[Document.Node.Name] = File_Format.registry.get(name).flatMap(_.make_theory_name(resources, name)) def make_theory_content(thy_name: Document.Node.Name): Option[String] = File_Format.registry.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name)) def make_preview(snapshot: Document.Snapshot): Option[Presentation.Preview] = File_Format.registry.get(snapshot.node_name).flatMap(_.make_preview(snapshot)) def is_hidden(name: Document.Node.Name): Boolean = !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name) def thy_path(path: Path): Path = path.ext("thy") /* file-system operations */ def append(dir: String, source_path: Path): String = (Path.explode(dir) + source_path).expand.implode def append(node_name: Document.Node.Name, source_path: Path): String = append(node_name.master_dir, source_path) def make_theory_node(dir: String, file: Path, theory: String): Document.Node.Name = { val node = append(dir, file) val master_dir = append(dir, file.dir) Document.Node.Name(node, master_dir, theory) } def loaded_theory_node(theory: String): Document.Node.Name = Document.Node.Name(theory, "", theory) /* source files of Isabelle/ML bootstrap */ def source_file(raw_name: String): Option[String] = { if (Path.is_wellformed(raw_name)) { if (Path.is_valid(raw_name)) { def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None val path = Path.explode(raw_name) val path1 = if (path.is_absolute || path.is_current) check(path) else { check(Path.explode("~~/src/Pure") + path) orElse (if (Isabelle_System.getenv("ML_SOURCES") == "") None else check(Path.explode("$ML_SOURCES") + path)) } Some(File.platform_path(path1 getOrElse path)) } else None } else Some(raw_name) } /* theory files */ def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name): () => List[Path] = { val (is_utf8, raw_text) = with_thy_reader(name, reader => (Scan.reader_is_utf8(reader), reader.source.toString)) () => { if (syntax.has_load_commands(raw_text)) { val text = Symbol.decode(Scan.reader_decode_utf8(is_utf8, raw_text)) val spans = syntax.parse_spans(text) val dir = Path.explode(name.master_dir) (for { span <- spans.iterator file <- span.loaded_files(syntax).files } yield (dir + Path.explode(file)).expand).toList } else Nil } } def pure_files(syntax: Outer_Syntax): List[Path] = { val pure_dir = Path.explode("~~/src/Pure") val roots = for { (name, _) <- Thy_Header.ml_roots } yield (pure_dir + Path.explode(name)).expand val files = for { (path, (_, theory)) <- roots zip Thy_Header.ml_roots file <- loaded_files(syntax, Document.Node.Name(path.implode, path.dir.implode, theory))() } yield file roots ::: files } def theory_name(qualifier: String, theory: String): String = if (Long_Name.is_qualified(theory) || session_base.global_theories.isDefinedAt(theory)) theory else Long_Name.qualify(qualifier, theory) def find_theory_node(theory: String): Option[Document.Node.Name] = { val thy_file = thy_path(Path.basic(Long_Name.base_name(theory))) val session = session_base.theory_qualifier(theory) val dirs = sessions_structure.get(session) match { case Some(info) => info.dirs case None => Nil } dirs.collectFirst({ case dir if (dir + thy_file).is_file => make_theory_node("", dir + thy_file, theory) }) } def import_name(qualifier: String, dir: String, s: String): Document.Node.Name = { val theory = theory_name(qualifier, Thy_Header.import_name(s)) def theory_node = make_theory_node(dir, thy_path(Path.explode(s)), theory) if (!Thy_Header.is_base_name(s)) theory_node else if (session_base.loaded_theory(theory)) loaded_theory_node(theory) else { find_theory_node(theory) match { case Some(node_name) => node_name case None => if (Long_Name.is_qualified(s)) loaded_theory_node(theory) else theory_node } } } def import_name(name: Document.Node.Name, s: String): Document.Node.Name = import_name(session_base.theory_qualifier(name), name.master_dir, s) def import_name(info: Sessions.Info, s: String): Document.Node.Name = import_name(info.name, info.dir.implode, s) def find_theory(file: JFile): Option[Document.Node.Name] = { for { qualifier <- session_base.session_directories.get(File.canonical(file).getParentFile) theory_base <- proper_string(Thy_Header.theory_name(file.getName)) theory = theory_name(qualifier, theory_base) theory_node <- find_theory_node(theory) if File.eq(theory_node.path.file, file) } yield theory_node } def complete_import_name(context_name: Document.Node.Name, s: String): List[String] = { val context_session = session_base.theory_qualifier(context_name) val context_dir = try { Some(context_name.master_dir_path) } catch { case ERROR(_) => None } (for { (session, (info, _)) <- sessions_structure.imports_graph.iterator dir <- (if (session == context_session) context_dir.toList else info.dirs).iterator theory <- Thy_Header.try_read_dir(dir).iterator if Completion.completed(s)(theory) } yield { if (session == context_session || session_base.global_theories.isDefinedAt(theory)) theory else Long_Name.qualify(session, theory) }).toList.sorted } def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = { val path = name.path if (path.is_file) using(Scan.byte_reader(path.file))(f) else if (name.node == name.theory) error("Cannot load theory " + quote(name.theory)) else error ("Cannot load theory file " + path) } - def check_thy_reader(node_name: Document.Node.Name, reader: Reader[Char], + def check_thy(node_name: Document.Node.Name, reader: Reader[Char], start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header = { if (node_name.is_theory && reader.source.length > 0) { try { val header = Thy_Header.read(reader, start, strict).check_keywords val base_name = node_name.theory_base_name if (Long_Name.is_qualified(header.name)) { error("Bad theory name " + quote(header.name) + " with qualification" + Position.here(header.pos)) } if (base_name != header.name) { error("Bad theory name " + quote(header.name) + " for file " + thy_path(Path.basic(base_name)) + Position.here(header.pos) + Completion.report_theories(header.pos, List(base_name))) } val imports_pos = header.imports_pos.map({ case (s, pos) => val name = import_name(node_name, s) if (Sessions.exclude_theory(name.theory_base_name)) error("Bad theory name " + quote(name.theory_base_name) + Position.here(pos)) (name, pos) }) Document.Node.Header(imports_pos, header.keywords, header.abbrevs) } catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) } } else Document.Node.no_header } - def check_thy(name: Document.Node.Name, start: Token.Pos = Token.Pos.command, - strict: Boolean = true): Document.Node.Header = - with_thy_reader(name, check_thy_reader(name, _, start, strict)) - /* special header */ def special_header(name: Document.Node.Name): Option[Document.Node.Header] = { val imports = if (name.theory == Sessions.root_name) List(import_name(name, Sessions.theory_name)) else if (Thy_Header.is_ml_root(name.theory)) List(import_name(name, Thy_Header.ML_BOOTSTRAP)) else if (Thy_Header.is_bootstrap(name.theory)) List(import_name(name, Thy_Header.PURE)) else Nil if (imports.isEmpty) None else Some(Document.Node.Header(imports.map((_, Position.none)))) } /* blobs */ def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] = (for { (node_name, node) <- nodes.iterator if !session_base.loaded_theory(node_name) cmd <- node.load_commands.iterator name <- cmd.blobs_undefined.iterator } yield name).toList /* document changes */ def parse_change( reparse_limit: Int, previous: Document.Version, doc_blobs: Document.Blobs, edits: List[Document.Edit_Text], consolidate: List[Document.Node.Name]): Session.Change = Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate) def commit(change: Session.Change) { } /* theory and file dependencies */ def dependencies( thys: List[(Document.Node.Name, Position.T)], progress: Progress = new Progress): Dependencies[Unit] = Dependencies.empty[Unit].require_thys((), thys, progress = progress) def session_dependencies(info: Sessions.Info, progress: Progress = new Progress) : Dependencies[Options] = { (Dependencies.empty[Options] /: info.theories)({ case (dependencies, (options, thys)) => dependencies.require_thys(options, for { (thy, pos) <- thys } yield (import_name(info, thy), pos), progress = progress) }) } object Dependencies { def empty[A]: Dependencies[A] = new Dependencies[A](Nil, Map.empty) private def show_path(names: List[Document.Node.Name]): String = names.map(name => quote(name.theory)).mkString(" via ") private def cycle_msg(names: List[Document.Node.Name]): String = "Cyclic dependency of " + show_path(names) private def required_by(initiators: List[Document.Node.Name]): String = if (initiators.isEmpty) "" else "\n(required by " + show_path(initiators.reverse) + ")" } final class Dependencies[A] private( rev_entries: List[Document.Node.Entry], seen: Map[Document.Node.Name, A]) { private def cons(entry: Document.Node.Entry): Dependencies[A] = new Dependencies[A](entry :: rev_entries, seen) def require_thy(adjunct: A, thy: (Document.Node.Name, Position.T), initiators: List[Document.Node.Name] = Nil, progress: Progress = new Progress): Dependencies[A] = { val (name, pos) = thy def message: String = "The error(s) above occurred for theory " + quote(name.theory) + Dependencies.required_by(initiators) + Position.here(pos) if (seen.isDefinedAt(name)) this else { val dependencies1 = new Dependencies[A](rev_entries, seen + (name -> adjunct)) if (session_base.loaded_theory(name)) dependencies1 else { try { if (initiators.contains(name)) error(Dependencies.cycle_msg(initiators)) progress.expose_interrupt() val header = - try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) } + try { + val start = Token.Pos.file(name.node) + with_thy_reader(name, check_thy(name, _, start = start)).cat_errors(message) + } catch { case ERROR(msg) => cat_error(msg, message) } val entry = Document.Node.Entry(name, header) dependencies1.require_thys(adjunct, header.imports_pos, initiators = name :: initiators, progress = progress).cons(entry) } catch { case e: Throwable => dependencies1.cons(Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e)))) } } } } def require_thys(adjunct: A, thys: List[(Document.Node.Name, Position.T)], progress: Progress = new Progress, initiators: List[Document.Node.Name] = Nil): Dependencies[A] = (this /: thys)(_.require_thy(adjunct, _, progress = progress, initiators = initiators)) def entries: List[Document.Node.Entry] = rev_entries.reverse def theories: List[Document.Node.Name] = entries.map(_.name) def theories_adjunct: List[(Document.Node.Name, A)] = theories.map(name => (name, seen(name))) def errors: List[String] = entries.flatMap(_.header.errors) def check_errors: Dependencies[A] = errors match { case Nil => this case errs => error(cat_lines(errs)) } lazy val theory_graph: Document.Node.Name.Graph[Unit] = { val regular = theories.toSet val irregular = (for { entry <- entries.iterator imp <- entry.header.imports if !regular(imp) } yield imp).toSet Document.Node.Name.make_graph( irregular.toList.map(name => ((name, ()), Nil)) ::: entries.map(entry => ((entry.name, ()), entry.header.imports))) } lazy val loaded_theories: Graph[String, Outer_Syntax] = (session_base.loaded_theories /: entries)({ case (graph, entry) => val name = entry.name.theory val imports = entry.header.imports.map(_.theory) val graph1 = (graph /: (name :: imports))(_.default_node(_, Outer_Syntax.empty)) val graph2 = (graph1 /: imports)(_.add_edge(_, name)) val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node) val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header graph2.map_node(name, _ => syntax) }) def loaded_files(pure: Boolean): List[(String, List[Path])] = { val loaded_files = theories.map(_.theory) zip Par_List.map((e: () => List[Path]) => e(), theories.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name))) if (pure) { val pure_files = resources.pure_files(overall_syntax) loaded_files.map({ case (name, files) => (name, if (name == Thy_Header.PURE) pure_files ::: files else files) }) } else loaded_files } def imported_files: List[Path] = { val base_theories = loaded_theories.all_preds(theories.map(_.theory)). filter(session_base.loaded_theories.defined) base_theories.map(theory => session_base.known_theories(theory).name.path) ::: base_theories.flatMap(session_base.known_loaded_files(_)) } lazy val overall_syntax: Outer_Syntax = Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node)) override def toString: String = entries.toString } } diff --git a/src/Tools/VSCode/src/vscode_model.scala b/src/Tools/VSCode/src/vscode_model.scala --- a/src/Tools/VSCode/src/vscode_model.scala +++ b/src/Tools/VSCode/src/vscode_model.scala @@ -1,248 +1,248 @@ /* Title: Tools/VSCode/src/vscode_model.scala Author: Makarius VSCode document model for line-oriented text. */ package isabelle.vscode import isabelle._ import java.io.{File => JFile} object VSCode_Model { /* decorations */ object Decoration { def empty(typ: String): Decoration = Decoration(typ, Nil) def ranges(typ: String, ranges: List[Text.Range]): Decoration = Decoration(typ, ranges.map(Text.Info(_, List.empty[XML.Body]))) } sealed case class Decoration(typ: String, content: List[Text.Info[List[XML.Body]]]) /* content */ object Content { val empty: Content = Content(Line.Document.empty) } sealed case class Content(doc: Line.Document) { override def toString: String = doc.toString def text_length: Text.Offset = doc.text_length def text_range: Text.Range = doc.text_range def text: String = doc.text lazy val bytes: Bytes = Bytes(text) lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text) lazy val bibtex_entries: List[Text.Info[String]] = try { Bibtex.entries(text) } catch { case ERROR(_) => Nil } def recode_symbols: List[LSP.TextEdit] = (for { (line, l) <- doc.lines.iterator.zipWithIndex text1 = Symbol.encode(line.text) if (line.text != text1) } yield { val range = Line.Range(Line.Position(l), Line.Position(l, line.text.length)) LSP.TextEdit(range, text1) }).toList } def init(session: Session, editor: Language_Server.Editor, node_name: Document.Node.Name) : VSCode_Model = { VSCode_Model(session, editor, node_name, Content.empty, node_required = File_Format.registry.is_theory(node_name)) } } sealed case class VSCode_Model( session: Session, editor: Language_Server.Editor, node_name: Document.Node.Name, content: VSCode_Model.Content, version: Option[Long] = None, external_file: Boolean = false, node_required: Boolean = false, last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text, pending_edits: List[Text.Edit] = Nil, published_diagnostics: List[Text.Info[Command.Results]] = Nil, published_decorations: List[VSCode_Model.Decoration] = Nil) extends Document.Model { model => /* content */ def get_text(range: Text.Range): Option[String] = content.doc.get_text(range) def set_version(new_version: Long): VSCode_Model = copy(version = Some(new_version)) /* external file */ def external(b: Boolean): VSCode_Model = copy(external_file = b) def node_visible: Boolean = !external_file /* header */ def node_header: Document.Node.Header = resources.special_header(node_name) getOrElse - resources.check_thy_reader(node_name, Scan.char_reader(content.text)) + resources.check_thy(node_name, Scan.char_reader(content.text)) /* perspective */ def node_perspective(doc_blobs: Document.Blobs, caret: Option[Line.Position]) : (Boolean, Document.Node.Perspective_Text) = { if (is_theory) { val snapshot = model.snapshot() val caret_perspective = resources.options.int("vscode_caret_perspective") max 0 val caret_range = if (caret_perspective != 0) { caret match { case Some(pos) => val doc = content.doc val pos1 = Line.Position((pos.line - caret_perspective) max 0) val pos2 = Line.Position((pos.line + caret_perspective + 1) min doc.lines.length) Text.Range(doc.offset(pos1).get, doc.offset(pos2).get) case None => Text.Range.offside } } else if (node_visible) content.text_range else Text.Range.offside val text_perspective = if (snapshot.commands_loading_ranges(resources.visible_node(_)).nonEmpty) Text.Perspective.full else content.text_range.try_restrict(caret_range) match { case Some(range) => Text.Perspective(List(range)) case None => Text.Perspective.empty } val overlays = editor.node_overlays(node_name) (snapshot.node.load_commands_changed(doc_blobs), Document.Node.Perspective(node_required, text_perspective, overlays)) } else (false, Document.Node.no_perspective_text) } /* blob */ def get_blob: Option[Document.Blob] = if (is_theory) None else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty)) /* bibtex entries */ def bibtex_entries: List[Text.Info[String]] = model.content.bibtex_entries /* edits */ def change_text(text: String, range: Option[Line.Range] = None): Option[VSCode_Model] = { val insert = Line.normalize(text) range match { case None => Text.Edit.replace(0, content.text, insert) match { case Nil => None case edits => val content1 = VSCode_Model.Content(Line.Document(insert)) Some(copy(content = content1, pending_edits = pending_edits ::: edits)) } case Some(remove) => content.doc.change(remove, insert) match { case None => error("Failed to apply document change: " + remove) case Some((Nil, _)) => None case Some((edits, doc1)) => val content1 = VSCode_Model.Content(doc1) Some(copy(content = content1, pending_edits = pending_edits ::: edits)) } } } def flush_edits( unicode_symbols: Boolean, doc_blobs: Document.Blobs, file: JFile, caret: Option[Line.Position]) : Option[((List[LSP.TextDocumentEdit], List[Document.Edit_Text]), VSCode_Model)] = { val workspace_edits = if (unicode_symbols && version.isDefined) { val edits = content.recode_symbols if (edits.nonEmpty) List(LSP.TextDocumentEdit(file, version.get, edits)) else Nil } else Nil val (reparse, perspective) = node_perspective(doc_blobs, caret) if (reparse || pending_edits.nonEmpty || last_perspective != perspective || workspace_edits.nonEmpty) { val prover_edits = node_edits(node_header, pending_edits, perspective) val edits = (workspace_edits, prover_edits) Some((edits, copy(pending_edits = Nil, last_perspective = perspective))) } else None } /* publish annotations */ def publish(rendering: VSCode_Rendering): (Option[List[Text.Info[Command.Results]]], Option[List[VSCode_Model.Decoration]], VSCode_Model) = { val diagnostics = rendering.diagnostics val decorations = if (node_visible) rendering.decorations else { for (deco <- published_decorations) yield VSCode_Model.Decoration.empty(deco.typ) } val changed_diagnostics = if (diagnostics == published_diagnostics) None else Some(diagnostics) val changed_decorations = if (decorations == published_decorations) None else if (published_decorations.isEmpty) Some(decorations) else Some(for { (a, b) <- decorations zip published_decorations if a != b } yield a) (changed_diagnostics, changed_decorations, copy(published_diagnostics = diagnostics, published_decorations = decorations)) } /* prover session */ def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources] def is_stable: Boolean = pending_edits.isEmpty def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits) def rendering(snapshot: Document.Snapshot): VSCode_Rendering = new VSCode_Rendering(snapshot, model) def rendering(): VSCode_Rendering = rendering(snapshot()) /* syntax */ def syntax(): Outer_Syntax = if (is_theory) session.recent_syntax(node_name) else Outer_Syntax.empty } diff --git a/src/Tools/jEdit/src/document_model.scala b/src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala +++ b/src/Tools/jEdit/src/document_model.scala @@ -1,695 +1,695 @@ /* Title: Tools/jEdit/src/document_model.scala Author: Fabian Immler, TU Munich Author: Makarius Document model connected to jEdit buffer or external file: content of theory node or auxiliary file (blob). */ package isabelle.jedit import isabelle._ import java.io.{File => JFile} import scala.collection.mutable import scala.annotation.tailrec import org.gjt.sp.jedit.{jEdit, View} import org.gjt.sp.jedit.Buffer import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer} object Document_Model { /* document models */ sealed case class State( models: Map[Document.Node.Name, Document_Model] = Map.empty, buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty, overlays: Document.Overlays = Document.Overlays.empty) { def file_models_iterator: Iterator[(Document.Node.Name, File_Model)] = for { (node_name, model) <- models.iterator if model.isInstanceOf[File_Model] } yield (node_name, model.asInstanceOf[File_Model]) def document_blobs: Document.Blobs = Document.Blobs( (for { (node_name, model) <- models.iterator blob <- model.get_blob } yield (node_name -> blob)).toMap) def open_buffer(session: Session, node_name: Document.Node.Name, buffer: Buffer) : (Buffer_Model, State) = { val old_model = models.get(node_name) match { case Some(file_model: File_Model) => Some(file_model) case Some(buffer_model: Buffer_Model) => Some(buffer_model.exit()) case _ => None } val buffer_model = Buffer_Model(session, node_name, buffer).init(old_model) (buffer_model, copy(models = models + (node_name -> buffer_model), buffer_models = buffer_models + (buffer -> buffer_model))) } def close_buffer(buffer: JEditBuffer): State = { buffer_models.get(buffer) match { case None => this case Some(buffer_model) => val file_model = buffer_model.exit() copy(models = models + (file_model.node_name -> file_model), buffer_models = buffer_models - buffer) } } def provide_file(session: Session, node_name: Document.Node.Name, text: String): State = if (models.isDefinedAt(node_name)) this else { val edit = Text.Edit.insert(0, text) val model = File_Model.init(session, node_name, text, pending_edits = List(edit)) copy(models = models + (node_name -> model)) } } private val state = Synchronized(State()) // owned by GUI thread def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models def get(name: Document.Node.Name): Option[Document_Model] = get_models().get(name) def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer) def document_blobs(): Document.Blobs = state.value.document_blobs /* bibtex */ def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] = Bibtex.entries_iterator(state.value.models) def bibtex_completion(history: Completion.History, rendering: Rendering, caret: Text.Offset) : Option[Completion.Result] = Bibtex.completion(history, rendering, caret, state.value.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(st => st.copy(overlays = st.overlays.insert(command, fn, args))) def remove_overlay(command: Command, fn: String, args: List[String]): Unit = state.change(st => st.copy(overlays = st.overlays.remove(command, fn, args))) /* sync external files */ def sync_files(changed_files: Set[JFile]): Boolean = { state.change_result(st => { val changed_models = (for { (node_name, model) <- st.file_models_iterator file <- model.file if changed_files(file) text <- PIDE.resources.read_file_content(node_name) if model.content.text != text } yield { val content = Document_Model.File_Content(text) val edits = Text.Edit.replace(0, model.content.text, text) (node_name, model.copy(content = content, pending_edits = model.pending_edits ::: edits)) }).toList if (changed_models.isEmpty) (false, st) else (true, st.copy(models = (st.models /: changed_models)(_ + _))) }) } /* syntax */ def syntax_changed(names: List[Document.Node.Name]) { GUI_Thread.require {} val models = state.value.models for (name <- names.iterator; model <- models.get(name)) { model match { case buffer_model: Buffer_Model => buffer_model.syntax_changed() case _ => } } } /* init and exit */ def init(session: Session, node_name: Document.Node.Name, buffer: Buffer): Buffer_Model = { GUI_Thread.require {} state.change_result(st => st.buffer_models.get(buffer) match { case Some(buffer_model) if buffer_model.node_name == node_name => buffer_model.init_token_marker (buffer_model, st) case _ => val res = st.close_buffer(buffer).open_buffer(session, node_name, buffer) buffer.propertiesChanged res }) } def exit(buffer: Buffer) { GUI_Thread.require {} state.change(st => if (st.buffer_models.isDefinedAt(buffer)) { val res = st.close_buffer(buffer) buffer.propertiesChanged res } else st) } def provide_files(session: Session, files: List[(Document.Node.Name, String)]) { GUI_Thread.require {} state.change(st => (st /: files) { case (st1, (node_name, text)) => st1.provide_file(session, node_name, text) }) } /* required nodes */ def required_nodes(): Set[Document.Node.Name] = (for { (node_name, model) <- state.value.models.iterator if model.node_required } yield node_name).toSet def node_required(name: Document.Node.Name, toggle: Boolean = false, set: Boolean = false) { GUI_Thread.require {} val changed = state.change_result(st => st.models.get(name) match { case None => (false, st) case Some(model) => val required = if (toggle) !model.node_required else set model match { case model1: File_Model if required != model1.node_required => (true, st.copy(models = st.models + (name -> model1.copy(node_required = required)))) case model1: Buffer_Model if required != model1.node_required => model1.set_node_required(required); (true, st) case _ => (false, st) } }) if (changed) { PIDE.plugin.options_changed() PIDE.editor.flush() } } def view_node_required(view: View, toggle: Boolean = false, set: Boolean = false): Unit = Document_Model.get(view.getBuffer).foreach(model => node_required(model.node_name, toggle = toggle, set = set)) /* flushed edits */ def flush_edits(hidden: Boolean, purge: Boolean): (Document.Blobs, List[Document.Edit_Text]) = { GUI_Thread.require {} state.change_result(st => { val doc_blobs = st.document_blobs val buffer_edits = (for { (_, model) <- st.buffer_models.iterator edit <- model.flush_edits(doc_blobs, hidden).iterator } yield edit).toList val file_edits = (for { (node_name, model) <- st.file_models_iterator (edits, model1) <- model.flush_edits(doc_blobs, hidden) } yield (edits, node_name -> model1)).toList val model_edits = buffer_edits ::: file_edits.flatMap(_._1) val purge_edits = if (purge) { val purged = (for ((node_name, model) <- st.file_models_iterator) yield (node_name -> model.purge_edits(doc_blobs))).toList val imports = { val open_nodes = (for ((_, model) <- st.buffer_models.iterator) yield model.node_name).toList val touched_nodes = model_edits.map(_._1) val pending_nodes = for ((node_name, None) <- purged) yield node_name (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none)) } val retain = PIDE.resources.dependencies(imports).theories.toSet for ((node_name, Some(edits)) <- purged if !retain(node_name); edit <- edits) yield edit } else Nil val st1 = st.copy(models = st.models ++ file_edits.map(_._2) -- purge_edits.map(_._1)) PIDE.plugin.file_watcher.purge( (for { (_, model) <- st1.file_models_iterator file <- model.file } yield file.getParentFile).toSet) ((doc_blobs, model_edits ::: purge_edits), st1) }) } /* file content */ sealed case class File_Content(text: String) { lazy val bytes: Bytes = Bytes(Symbol.encode(text)) lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text) lazy val bibtex_entries: List[Text.Info[String]] = try { Bibtex.entries(text) } catch { case ERROR(_) => Nil } } /* HTTP preview */ private val plain_text_prefix = "plain_text=" def open_preview(view: View, plain_text: Boolean) { Document_Model.get(view.getBuffer) match { case Some(model) => val name = model.node_name val url = PIDE.plugin.http_server.url.toString + PIDE.plugin.http_root + "/preview?" + (if (plain_text) plain_text_prefix else "") + Url.encode(name.node) PIDE.editor.hyperlink_url(url).follow(view) case _ => } } def http_handlers(http_root: String): List[HTTP.Handler] = { val fonts_root = http_root + "/fonts" val preview_root = http_root + "/preview" val preview = HTTP.get(preview_root, arg => for { query <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode) name = Library.perhaps_unprefix(plain_text_prefix, query) model <- get(PIDE.resources.node_name(name)) } yield { val snapshot = model.await_stable_snapshot() val preview = Presentation.preview(PIDE.resources, snapshot, fonts_url = HTML.fonts_dir(fonts_root), plain_text = query.startsWith(plain_text_prefix)) HTTP.Response.html(preview.content) }) List(HTTP.fonts(fonts_root), preview) } } sealed abstract class Document_Model extends Document.Model { /* perspective */ def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil def node_perspective( doc_blobs: Document.Blobs, hidden: Boolean): (Boolean, Document.Node.Perspective_Text) = { GUI_Thread.require {} if (Isabelle.continuous_checking && is_theory) { val snapshot = this.snapshot() val reparse = snapshot.node.load_commands_changed(doc_blobs) val perspective = if (hidden) Text.Perspective.empty else { val view_ranges = document_view_ranges(snapshot) val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node) Text.Perspective(view_ranges ::: load_ranges) } val overlays = PIDE.editor.node_overlays(node_name) (reparse, Document.Node.Perspective(node_required, perspective, overlays)) } else (false, Document.Node.no_perspective_text) } /* snapshot */ @tailrec final def await_stable_snapshot(): Document.Snapshot = { val snapshot = this.snapshot() if (snapshot.is_outdated) { PIDE.options.seconds("editor_output_delay").sleep await_stable_snapshot() } else snapshot } } object File_Model { def empty(session: Session): File_Model = File_Model(session, Document.Node.Name.empty, None, Document_Model.File_Content(""), false, Document.Node.no_perspective_text, Nil) def init(session: Session, node_name: Document.Node.Name, text: String, node_required: Boolean = false, last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text, pending_edits: List[Text.Edit] = Nil): File_Model = { val file = JEdit_Lib.check_file(node_name.node) file.foreach(PIDE.plugin.file_watcher.register_parent(_)) val content = Document_Model.File_Content(text) val node_required1 = node_required || File_Format.registry.is_theory(node_name) File_Model(session, node_name, file, content, node_required1, last_perspective, pending_edits) } } case class File_Model( session: Session, node_name: Document.Node.Name, file: Option[JFile], content: Document_Model.File_Content, node_required: Boolean, last_perspective: Document.Node.Perspective_Text, pending_edits: List[Text.Edit]) extends Document_Model { /* text */ def get_text(range: Text.Range): Option[String] = range.try_substring(content.text) /* header */ def node_header: Document.Node.Header = PIDE.resources.special_header(node_name) getOrElse - PIDE.resources.check_thy_reader(node_name, Scan.char_reader(content.text), strict = false) + PIDE.resources.check_thy(node_name, Scan.char_reader(content.text), strict = false) /* content */ def node_position(offset: Text.Offset): Line.Node_Position = Line.Node_Position(node_name.node, Line.Position.zero.advance(content.text.substring(0, offset))) def get_blob: Option[Document.Blob] = if (is_theory) None else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty)) def bibtex_entries: List[Text.Info[String]] = if (Bibtex.is_bibtex(node_name.node)) content.bibtex_entries else Nil /* edits */ def update_text(text: String): Option[File_Model] = Text.Edit.replace(0, content.text, text) match { case Nil => None case edits => val content1 = Document_Model.File_Content(text) val pending_edits1 = pending_edits ::: edits Some(copy(content = content1, pending_edits = pending_edits1)) } def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean) : Option[(List[Document.Edit_Text], File_Model)] = { val (reparse, perspective) = node_perspective(doc_blobs, hidden) if (reparse || pending_edits.nonEmpty || last_perspective != perspective) { val edits = node_edits(node_header, pending_edits, perspective) Some((edits, copy(last_perspective = perspective, pending_edits = Nil))) } else None } def purge_edits(doc_blobs: Document.Blobs): Option[List[Document.Edit_Text]] = if (pending_edits.nonEmpty || !File_Format.registry.is_theory(node_name) && (node_required || !Document.Node.is_no_perspective_text(last_perspective))) None else { val text_edits = List(Text.Edit.remove(0, content.text)) Some(node_edits(Document.Node.no_header, text_edits, Document.Node.no_perspective_text)) } /* snapshot */ def is_stable: Boolean = pending_edits.isEmpty def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits) } case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer) extends Document_Model { /* text */ def get_text(range: Text.Range): Option[String] = JEdit_Lib.get_text(buffer, range) /* header */ def node_header(): Document.Node.Header = { GUI_Thread.require {} PIDE.resources.special_header(node_name) getOrElse JEdit_Lib.buffer_lock(buffer) { - PIDE.resources.check_thy_reader(node_name, JEdit_Lib.buffer_reader(buffer), strict = false) + PIDE.resources.check_thy(node_name, JEdit_Lib.buffer_reader(buffer), strict = false) } } /* perspective */ // owned by GUI thread private var _node_required = false def node_required: Boolean = _node_required def set_node_required(b: Boolean) { GUI_Thread.require { _node_required = b } } def document_view_iterator: Iterator[Document_View] = for { text_area <- JEdit_Lib.jedit_text_areas(buffer) doc_view <- Document_View.get(text_area) } yield doc_view override def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = { GUI_Thread.require {} (for { doc_view <- document_view_iterator range <- doc_view.perspective(snapshot).ranges.iterator } yield range).toList } /* blob */ // owned by GUI thread private var _blob: Option[(Bytes, String, Symbol.Text_Chunk)] = None private def reset_blob(): Unit = GUI_Thread.require { _blob = None } def get_blob: Option[Document.Blob] = GUI_Thread.require { if (is_theory) None else { val (bytes, text, chunk) = _blob match { case Some(x) => x case None => val bytes = PIDE.resources.make_file_content(buffer) val text = buffer.getText(0, buffer.getLength) val chunk = Symbol.Text_Chunk(text) val x = (bytes, text, chunk) _blob = Some(x) x } val changed = pending_edits.nonEmpty Some(Document.Blob(bytes, text, chunk, changed)) } } /* bibtex entries */ // owned by GUI thread private var _bibtex_entries: Option[List[Text.Info[String]]] = None private def reset_bibtex_entries(): Unit = GUI_Thread.require { _bibtex_entries = None } def bibtex_entries: List[Text.Info[String]] = GUI_Thread.require { if (Bibtex.is_bibtex(node_name.node)) { _bibtex_entries match { case Some(entries) => entries case None => val text = JEdit_Lib.buffer_text(buffer) val entries = try { Bibtex.entries(text) } catch { case ERROR(msg) => Output.warning(msg); Nil } _bibtex_entries = Some(entries) entries } } else Nil } /* pending edits */ private object pending_edits { private val pending = new mutable.ListBuffer[Text.Edit] private var last_perspective = Document.Node.no_perspective_text def nonEmpty: Boolean = synchronized { pending.nonEmpty } def get_edits: List[Text.Edit] = synchronized { pending.toList } def get_last_perspective: Document.Node.Perspective_Text = synchronized { last_perspective } def set_last_perspective(perspective: Document.Node.Perspective_Text): Unit = synchronized { last_perspective = perspective } def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] = synchronized { GUI_Thread.require {} val edits = get_edits val (reparse, perspective) = node_perspective(doc_blobs, hidden) if (reparse || edits.nonEmpty || last_perspective != perspective) { pending.clear last_perspective = perspective node_edits(node_header(), edits, perspective) } else Nil } def edit(edits: List[Text.Edit]): Unit = synchronized { GUI_Thread.require {} reset_blob() reset_bibtex_entries() for (doc_view <- document_view_iterator) doc_view.rich_text_area.active_reset() pending ++= edits PIDE.editor.invoke() } } def is_stable: Boolean = !pending_edits.nonEmpty def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits) def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] = pending_edits.flush_edits(doc_blobs, hidden) /* buffer listener */ private val buffer_listener: BufferListener = new BufferAdapter { override def contentInserted(buffer: JEditBuffer, start_line: Int, offset: Int, num_lines: Int, length: Int) { pending_edits.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length)))) } override def preContentRemoved(buffer: JEditBuffer, start_line: Int, offset: Int, num_lines: Int, removed_length: Int) { pending_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length)))) } } /* syntax */ def syntax_changed() { JEdit_Lib.buffer_line_manager(buffer).setFirstInvalidLineContext(0) for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged"). invoke(text_area) buffer.invalidateCachedFoldLevels } def init_token_marker() { Isabelle.buffer_token_marker(buffer) match { case Some(marker) if marker != buffer.getTokenMarker => buffer.setTokenMarker(marker) syntax_changed() case _ => } } /* init */ def init(old_model: Option[File_Model]): Buffer_Model = { GUI_Thread.require {} old_model match { case None => pending_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))) case Some(file_model) => set_node_required(file_model.node_required) pending_edits.set_last_perspective(file_model.last_perspective) pending_edits.edit( file_model.pending_edits ::: Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer))) } buffer.addBufferListener(buffer_listener) init_token_marker() this } /* exit */ def exit(): File_Model = { GUI_Thread.require {} buffer.removeBufferListener(buffer_listener) init_token_marker() File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer), node_required, pending_edits.get_last_perspective, pending_edits.get_edits) } }