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,698 +1,700 @@ /* 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.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)(_ + _))) + else (true, st.copy(models = changed_models.foldLeft(st.models)(_ + _))) }) } /* syntax */ def syntax_changed(names: List[Document.Node.Name]): Unit = { 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): Unit = { 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)]): Unit = { GUI_Thread.require {} state.change(st => - (st /: files) { case (st1, (node_name, text)) => st1.provide_file(session, node_name, text) }) + files.foldLeft(st) { + 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): Unit = { 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): Unit = { Document_Model.get(view.getBuffer) match { case Some(model) => val name = model.node_name val url = PIDE.plugin.http_server.url + 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 html = 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 html_context = Presentation.html_context(fonts_url = HTML.fonts_dir(fonts_root)) val document = Presentation.html_document( PIDE.resources, snapshot, html_context, Presentation.elements2, plain_text = query.startsWith(plain_text_prefix)) HTTP.Response.html(document.content) }) List(HTTP.fonts(fonts_root), html) } } 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(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(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): Unit = 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): Unit = { 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): Unit = { pending_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length)))) } } /* syntax */ def syntax_changed(): Unit = { 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(): Unit = { 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) } } diff --git a/src/Tools/jEdit/src/isabelle_sidekick.scala b/src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala @@ -1,267 +1,267 @@ /* Title: Tools/jEdit/src/isabelle_sidekick.scala Author: Fabian Immler, TU Munich Author: Makarius SideKick parsers for Isabelle proof documents. */ package isabelle.jedit import isabelle._ import javax.swing.tree.DefaultMutableTreeNode import javax.swing.text.Position import javax.swing.{JLabel, Icon} import org.gjt.sp.jedit.Buffer import sidekick.{SideKickParser, SideKickParsedData, IAsset} object Isabelle_Sidekick { def int_to_pos(offset: Text.Offset): Position = new Position { def getOffset = offset; override def toString: String = offset.toString } def root_data(buffer: Buffer): SideKickParsedData = { val data = new SideKickParsedData(buffer.getName) data.getAsset(data.root).setEnd(int_to_pos(buffer.getLength)) data } class Keyword_Asset(keyword: String, text: String, range: Text.Range) extends IAsset { private val css = GUI.imitate_font_css(GUI.label_font()) protected var _name = text protected var _start = int_to_pos(range.start) protected var _end = int_to_pos(range.stop) override def getIcon: Icon = null override def getShortString: String = { val n = keyword.length val s = _name.indexOf(keyword) match { case i if i >= 0 && n > 0 => HTML.output(_name.substring(0, i)) + "" + HTML.output(keyword) + "" + HTML.output(_name.substring(i + n)) case _ => HTML.output(_name) } "" + s + "" } override def getLongString: String = _name override def getName: String = _name override def setName(name: String): Unit = _name = name override def getStart: Position = _start override def setStart(start: Position): Unit = _start = start override def getEnd: Position = _end override def setEnd(end: Position): Unit = _end = end override def toString: String = _name } class Asset(name: String, range: Text.Range) extends Keyword_Asset("", name, range) def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode, swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode): Unit = { for ((_, entry) <- tree.branches) { val node = swing_node(Text.Info(entry.range, entry.markup)) swing_markup_tree(entry.subtree, node, swing_node) parent.add(node) } } } class Isabelle_Sidekick(name: String) extends SideKickParser(name) { override def supportsCompletion = false /* parsing */ @volatile protected var stopped = false override def stop() = { stopped = true } def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData = { stopped = false // FIXME lock buffer (!??) val data = Isabelle_Sidekick.root_data(buffer) val syntax = Isabelle.buffer_syntax(buffer) val ok = if (syntax.isDefined) { val ok = parser(buffer, syntax.get, data) if (stopped) { data.root.add(new DefaultMutableTreeNode("")); true } else ok } else false if (!ok) data.root.add(new DefaultMutableTreeNode("")) data } } class Isabelle_Sidekick_Structure( name: String, node_name: Buffer => Option[Document.Node.Name], parse: (Outer_Syntax, Document.Node.Name, CharSequence) => List[Document_Structure.Document]) extends Isabelle_Sidekick(name) { override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = { def make_tree( parent: DefaultMutableTreeNode, offset: Text.Offset, documents: List[Document_Structure.Document]): Unit = { - (offset /: documents) { case (i, document) => + documents.foldLeft(offset) { case (i, document) => document match { case Document_Structure.Block(name, text, body) => val range = Text.Range(i, i + document.length) val node = new DefaultMutableTreeNode( new Isabelle_Sidekick.Keyword_Asset(name, Library.first_line(text), range)) parent.add(node) make_tree(node, i, body) case _ => } i + document.length } } node_name(buffer) match { case Some(name) => make_tree(data.root, 0, parse(syntax, name, JEdit_Lib.buffer_text(buffer))) true case None => false } } } class Isabelle_Sidekick_Default extends Isabelle_Sidekick_Structure("isabelle", PIDE.resources.theory_node_name, Document_Structure.parse_sections) class Isabelle_Sidekick_Context extends Isabelle_Sidekick_Structure("isabelle-context", PIDE.resources.theory_node_name, Document_Structure.parse_blocks) class Isabelle_Sidekick_Options extends Isabelle_Sidekick_Structure("isabelle-options", _ => Some(Document.Node.Name("options")), Document_Structure.parse_sections) class Isabelle_Sidekick_Root extends Isabelle_Sidekick_Structure("isabelle-root", _ => Some(Document.Node.Name("ROOT")), Document_Structure.parse_sections) class Isabelle_Sidekick_ML extends Isabelle_Sidekick_Structure("isabelle-ml", buffer => Some(PIDE.resources.node_name(buffer)), (_, _, text) => Document_Structure.parse_ml_sections(false, text)) class Isabelle_Sidekick_SML extends Isabelle_Sidekick_Structure("isabelle-sml", buffer => Some(PIDE.resources.node_name(buffer)), (_, _, text) => Document_Structure.parse_ml_sections(true, text)) class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup") { override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = { val opt_snapshot = Document_Model.get(buffer) match { case Some(model) if model.is_theory => Some(model.snapshot) case _ => None } opt_snapshot match { case Some(snapshot) => for ((command, command_start) <- snapshot.node.command_iterator() if !stopped) { val markup = snapshot.state.command_markup( snapshot.version, command, Command.Markup_Index.markup, command.range, Markup.Elements.full) Isabelle_Sidekick.swing_markup_tree(markup, data.root, (info: Text.Info[List[XML.Elem]]) => { val range = info.range + command_start val content = command.source(info.range).replace('\n', ' ') val info_text = Pretty.formatted(Pretty.fbreaks(info.info), margin = 40.0).mkString new DefaultMutableTreeNode( new Isabelle_Sidekick.Asset(command.toString, range) { override def getShortString: String = content override def getLongString: String = info_text override def toString: String = quote(content) + " " + range.toString }) }) } true case None => false } } } class Isabelle_Sidekick_News extends Isabelle_Sidekick("isabelle-news") { private val Heading1 = """^New in (.*)\w*$""".r private val Heading2 = """^\*\*\*\w*(.*)\w*\*\*\*\w*$""".r private def make_node(s: String, start: Text.Offset, stop: Text.Offset): DefaultMutableTreeNode = new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, Text.Range(start, stop))) override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = { var offset = 0 var end_offset = 0 var start1: Option[(Int, String, Vector[DefaultMutableTreeNode])] = None var start2: Option[(Int, String)] = None def close1: Unit = start1 match { case Some((start_offset, s, body)) => val node = make_node(s, start_offset, end_offset) body.foreach(node.add(_)) data.root.add(node) start1 = None case None => } def close2: Unit = start2 match { case Some((start_offset, s)) => start1 match { case Some((start_offset1, s1, body)) => val node = make_node(s, start_offset, end_offset) start1 = Some((start_offset1, s1, body :+ node)) case None => } start2 = None case None => } for (line <- split_lines(JEdit_Lib.buffer_text(buffer)) if !stopped) { line match { case Heading1(s) => close2; close1; start1 = Some((offset, s, Vector())) case Heading2(s) => close2; start2 = Some((offset, s)) case _ => } offset += line.length + 1 if (!line.forall(Character.isSpaceChar)) end_offset = offset } if (!stopped) { close2; close1 } true } } diff --git a/src/Tools/jEdit/src/jedit_editor.scala b/src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala +++ b/src/Tools/jEdit/src/jedit_editor.scala @@ -1,323 +1,322 @@ /* Title: Tools/jEdit/src/jedit_editor.scala Author: Makarius PIDE editor operations for jEdit. */ package isabelle.jedit import isabelle._ import java.io.{File => JFile} import org.gjt.sp.jedit.{jEdit, View, Buffer} import org.gjt.sp.jedit.browser.VFSBrowser import org.gjt.sp.jedit.io.{VFSManager, VFSFile} class JEdit_Editor extends Editor[View] { /* session */ override def session: Session = PIDE.session def flush_edits(hidden: Boolean = false, purge: Boolean = false): Unit = GUI_Thread.require { val (doc_blobs, edits) = Document_Model.flush_edits(hidden, purge) session.update(doc_blobs, edits) } override def flush(): Unit = flush_edits() def purge(): Unit = flush_edits(purge = true) private val delay1_flush = Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { flush() } private val delay2_flush = Delay.first(PIDE.options.seconds("editor_generated_input_delay"), gui = true) { flush() } def invoke(): Unit = delay1_flush.invoke() def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() } def shutdown(): Unit = GUI_Thread.require { delay1_flush.revoke() delay2_flush.revoke() Document_Model.flush_edits(hidden = false, purge = false) } def visible_node(name: Document.Node.Name): Boolean = (for { text_area <- JEdit_Lib.jedit_text_areas() doc_view <- Document_View.get(text_area) } yield doc_view.model.node_name).contains(name) /* current situation */ override def current_node(view: View): Option[Document.Node.Name] = GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.node_name) } override def current_node_snapshot(view: View): Option[Document.Snapshot] = GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.snapshot()) } override def node_snapshot(name: Document.Node.Name): Document.Snapshot = { GUI_Thread.require {} Document_Model.get(name) match { case Some(model) => model.snapshot case None => session.snapshot(name) } } override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] = { GUI_Thread.require {} val text_area = view.getTextArea val buffer = view.getBuffer Document_View.get(text_area) match { case Some(doc_view) if doc_view.model.is_theory => snapshot.current_command(doc_view.model.node_name, text_area.getCaretPosition) case _ => Document_Model.get(buffer) match { case Some(model) if !model.is_theory => snapshot.version.nodes.commands_loading(model.node_name).headOption case _ => None } } } /* overlays */ override def node_overlays(name: Document.Node.Name): Document.Node.Overlays = Document_Model.node_overlays(name) override def insert_overlay(command: Command, fn: String, args: List[String]): Unit = Document_Model.insert_overlay(command, fn, args) override def remove_overlay(command: Command, fn: String, args: List[String]): Unit = Document_Model.remove_overlay(command, fn, args) /* navigation */ def push_position(view: View): Unit = { val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin") if (navigator != null) { try { Untyped.method(navigator.getClass, "pushPosition", view.getClass).invoke(null, view) } catch { case _: NoSuchMethodException => } } } def goto_buffer(focus: Boolean, view: View, buffer: Buffer, offset: Text.Offset): Unit = { GUI_Thread.require {} push_position(view) if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer) try { view.getTextArea.moveCaretPosition(offset) } catch { case _: ArrayIndexOutOfBoundsException => case _: IllegalArgumentException => } } def goto_file(focus: Boolean, view: View, name: String): Unit = goto_file(focus, view, Line.Node_Position.offside(name)) def goto_file(focus: Boolean, view: View, pos: Line.Node_Position): Unit = { GUI_Thread.require {} push_position(view) val name = pos.name val line = pos.line val column = pos.column JEdit_Lib.jedit_buffer(name) match { case Some(buffer) => if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer) val text_area = view.getTextArea try { val line_start = text_area.getBuffer.getLineStartOffset(line) text_area.moveCaretPosition(line_start) if (column > 0) text_area.moveCaretPosition(line_start + column) } catch { case _: ArrayIndexOutOfBoundsException => case _: IllegalArgumentException => } case None => val is_dir = try { val vfs = VFSManager.getVFSForPath(name) val vfs_file = vfs._getFile((), name, view) vfs_file != null && vfs_file.getType == VFSFile.DIRECTORY } catch { case ERROR(_) => false } if (is_dir) VFSBrowser.browseDirectory(view, name) else if (!Isabelle_System.open_external_file(name)) { val args = if (line <= 0) Array(name) else if (column <= 0) Array(name, "+line:" + (line + 1)) else Array(name, "+line:" + (line + 1) + "," + (column + 1)) jEdit.openFiles(view, null, args) } } } def goto_doc(view: View, path: Path): Unit = { if (path.is_file) goto_file(true, view, File.platform_path(path)) else { Isabelle_Thread.fork(name = "documentation") { try { Doc.view(path) } catch { case exn: Throwable => GUI_Thread.later { GUI.error_dialog(view, "Documentation error", GUI.scrollable_text(Exn.message(exn))) } } } } } /* hyperlinks */ def hyperlink_doc(name: String): Option[Hyperlink] = Doc.contents().collectFirst({ case doc: Doc.Text_File if doc.name == name => doc.path case doc: Doc.Doc if doc.name == name => doc.path}).map(path => new Hyperlink { override val external: Boolean = !path.is_file def follow(view: View): Unit = goto_doc(view, path) override def toString: String = "doc " + quote(name) }) def hyperlink_url(name: String): Hyperlink = new Hyperlink { override val external = true def follow(view: View): Unit = Isabelle_Thread.fork(name = "hyperlink_url") { try { Isabelle_System.open(Url.escape_name(name)) } catch { case exn: Throwable => GUI_Thread.later { GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn))) } } } override def toString: String = "URL " + quote(name) } def hyperlink_file(focus: Boolean, name: String): Hyperlink = hyperlink_file(focus, Line.Node_Position.offside(name)) def hyperlink_file(focus: Boolean, pos: Line.Node_Position): Hyperlink = new Hyperlink { def follow(view: View): Unit = goto_file(focus, view, pos) override def toString: String = "file " + quote(pos.name) } def hyperlink_model(focus: Boolean, model: Document_Model, offset: Text.Offset): Hyperlink = model match { case file_model: File_Model => val pos = try { file_model.node_position(offset) } catch { case ERROR(_) => Line.Node_Position(file_model.node_name.node) } hyperlink_file(focus, pos) case buffer_model: Buffer_Model => new Hyperlink { def follow(view: View): Unit = goto_buffer(focus, view, buffer_model.buffer, offset) override def toString: String = "buffer " + quote(model.node_name.node) } } def hyperlink_source_file(focus: Boolean, source_name: String, line1: Int, offset: Symbol.Offset) : Option[Hyperlink] = { for (name <- PIDE.resources.source_file(source_name)) yield { def hyperlink(pos: Line.Position) = hyperlink_file(focus, Line.Node_Position(name, pos)) if (offset > 0) { PIDE.resources.get_file_content(PIDE.resources.node_name(name)) match { case Some(text) => hyperlink( - (Line.Position.zero /: - (Symbol.iterator(text). - zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_))) + Symbol.iterator(text).zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1). + foldLeft(Line.Position.zero)(_.advance(_))) case None => hyperlink(Line.Position((line1 - 1) max 0)) } } else hyperlink(Line.Position((line1 - 1) max 0)) } } 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(hyperlink_file(focus, _)) } def is_hyperlink_position(snapshot: Document.Snapshot, text_offset: Text.Offset, pos: Position.T): Boolean = { pos match { case Position.Item_Id(id, range) if range.start > 0 => snapshot.find_command(id) match { case Some((node, command)) if snapshot.get_node(command.node_name) eq node => node.command_start(command) match { case Some(start) => text_offset == start + command.chunk.decode(range.start) case None => false } case _ => false } case _ => false } } def hyperlink_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T) : Option[Hyperlink] = pos match { case Position.Item_File(name, line, range) => hyperlink_source_file(focus, name, line, range.start) case Position.Item_Id(id, range) => hyperlink_command(focus, snapshot, id, range.start) case _ => None } def hyperlink_def_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T) : Option[Hyperlink] = pos match { case Position.Item_Def_File(name, line, range) => hyperlink_source_file(focus, name, line, range.start) case Position.Item_Def_Id(id, range) => hyperlink_command(focus, snapshot, id, range.start) case _ => None } /* dispatcher thread */ override def assert_dispatcher[A](body: => A): A = GUI_Thread.assert(body) override def require_dispatcher[A](body: => A): A = GUI_Thread.require(body) override def send_dispatcher(body: => Unit): Unit = GUI_Thread.later(body) override def send_wait_dispatcher(body: => Unit): Unit = GUI_Thread.now(body) } diff --git a/src/Tools/jEdit/src/jedit_rendering.scala b/src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala +++ b/src/Tools/jEdit/src/jedit_rendering.scala @@ -1,428 +1,428 @@ /* Title: Tools/jEdit/src/jedit_rendering.scala Author: Makarius Isabelle/jEdit-specific implementation of quasi-abstract rendering and markup interpretation. */ package isabelle.jedit import isabelle._ import java.awt.Color import javax.swing.Icon import org.gjt.sp.jedit.syntax.{Token => JEditToken} import org.gjt.sp.jedit.jEdit import scala.collection.immutable.SortedMap object JEdit_Rendering { /* make rendering */ def apply(snapshot: Document.Snapshot, model: Document_Model, options: Options): JEdit_Rendering = new JEdit_Rendering(snapshot, model, options) def text(snapshot: Document.Snapshot, formatted_body: XML.Body, results: Command.Results = Command.Results.empty): (String, JEdit_Rendering) = { val command = Command.rich_text(Document_ID.make(), results, formatted_body) val snippet = snapshot.snippet(command) val model = File_Model.empty(PIDE.session) val rendering = apply(snippet, model, PIDE.options.value) (command.source, rendering) } /* popup window bounds */ def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8 /* Isabelle/Isar token markup */ private val command_style: Map[String, Byte] = { import JEditToken._ Map[String, Byte]( Keyword.THY_END -> KEYWORD2, Keyword.PRF_ASM -> KEYWORD3, Keyword.PRF_ASM_GOAL -> KEYWORD3 ).withDefaultValue(KEYWORD1) } private val token_style: Map[Token.Kind.Value, Byte] = { import JEditToken._ Map[Token.Kind.Value, Byte]( Token.Kind.KEYWORD -> KEYWORD2, Token.Kind.IDENT -> NULL, Token.Kind.LONG_IDENT -> NULL, Token.Kind.SYM_IDENT -> NULL, Token.Kind.VAR -> NULL, Token.Kind.TYPE_IDENT -> NULL, Token.Kind.TYPE_VAR -> NULL, Token.Kind.NAT -> NULL, Token.Kind.FLOAT -> NULL, Token.Kind.SPACE -> NULL, Token.Kind.STRING -> LITERAL1, Token.Kind.ALT_STRING -> LITERAL2, Token.Kind.VERBATIM -> COMMENT3, Token.Kind.CARTOUCHE -> COMMENT3, Token.Kind.INFORMAL_COMMENT -> COMMENT1, Token.Kind.FORMAL_COMMENT -> COMMENT1, Token.Kind.ERROR -> INVALID ).withDefaultValue(NULL) } def token_markup(syntax: Outer_Syntax, token: Token): Byte = if (token.is_command) command_style(syntax.keywords.kinds.getOrElse(token.content, "")) else if (token.is_delimiter) JEditToken.OPERATOR else token_style(token.kind) /* Isabelle/ML token markup */ private val ml_token_style: Map[ML_Lex.Kind.Value, Byte] = { import JEditToken._ Map[ML_Lex.Kind.Value, Byte]( ML_Lex.Kind.KEYWORD -> NULL, ML_Lex.Kind.IDENT -> NULL, ML_Lex.Kind.LONG_IDENT -> NULL, ML_Lex.Kind.TYPE_VAR -> NULL, ML_Lex.Kind.WORD -> DIGIT, ML_Lex.Kind.INT -> DIGIT, ML_Lex.Kind.REAL -> DIGIT, ML_Lex.Kind.CHAR -> LITERAL2, ML_Lex.Kind.STRING -> LITERAL1, ML_Lex.Kind.SPACE -> NULL, ML_Lex.Kind.INFORMAL_COMMENT -> COMMENT1, ML_Lex.Kind.FORMAL_COMMENT -> COMMENT1, ML_Lex.Kind.ANTIQ -> NULL, ML_Lex.Kind.ANTIQ_START -> LITERAL4, ML_Lex.Kind.ANTIQ_STOP -> LITERAL4, ML_Lex.Kind.ANTIQ_OTHER -> NULL, ML_Lex.Kind.ANTIQ_STRING -> NULL, ML_Lex.Kind.ANTIQ_ALT_STRING -> NULL, ML_Lex.Kind.ANTIQ_CARTOUCHE -> NULL, ML_Lex.Kind.ERROR -> INVALID ).withDefaultValue(NULL) } def ml_token_markup(token: ML_Lex.Token): Byte = if (!token.is_keyword) ml_token_style(token.kind) else if (token.is_delimiter) JEditToken.OPERATOR else if (ML_Lex.keywords2(token.source)) JEditToken.KEYWORD2 else if (ML_Lex.keywords3(token.source)) JEditToken.KEYWORD3 else JEditToken.KEYWORD1 /* markup elements */ private val indentation_elements = Markup.Elements(Markup.Command_Indent.name) private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT) private val highlight_elements = Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT, Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name) private val hyperlink_elements = Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.EXPORT_PATH, Markup.DOC, Markup.URL, Markup.POSITION, Markup.CITATION) private val gutter_elements = Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR) private val squiggly_elements = Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR) private val line_background_elements = Markup.Elements(Markup.WRITELN_MESSAGE, Markup.STATE_MESSAGE, Markup.INFORMATION_MESSAGE, Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.LEGACY_MESSAGE, Markup.ERROR_MESSAGE) private val separator_elements = Markup.Elements(Markup.SEPARATOR) private val bullet_elements = Markup.Elements(Markup.BULLET, Markup.ML_BREAKPOINT) private val fold_depth_elements = Markup.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL) } class JEdit_Rendering(snapshot: Document.Snapshot, model: Document_Model, options: Options) extends Rendering(snapshot, options, PIDE.session) { override def get_text(range: Text.Range): Option[String] = model.get_text(range) /* colors */ def color(s: String): Color = if (s == "main_color") main_color else Color_Value(options.string(s)) def color(c: Rendering.Color.Value): Color = _rendering_colors(c) lazy val _rendering_colors: Map[Rendering.Color.Value, Color] = Rendering.Color.values.iterator.map(c => c -> color(c.toString + "_color")).toMap val main_color = jEdit.getColorProperty("view.fgColor") val outdated_color = color("outdated_color") val bullet_color = color("bullet_color") val tooltip_color = color("tooltip_color") val spell_checker_color = color("spell_checker_color") val entity_ref_color = color("entity_ref_color") val breakpoint_disabled_color = color("breakpoint_disabled_color") val breakpoint_enabled_color = color("breakpoint_enabled_color") val caret_debugger_color = color("caret_debugger_color") val highlight_color = color("highlight_color") val hyperlink_color = color("hyperlink_color") val active_hover_color = color("active_hover_color") val caret_invisible_color = color("caret_invisible_color") val completion_color = color("completion_color") val search_color = color("search_color") /* indentation */ def indentation(range: Text.Range): Int = snapshot.select(range, JEdit_Rendering.indentation_elements, _ => { case Text.Info(_, XML.Elem(Markup.Command_Indent(i), _)) => Some(i) case _ => None }).headOption.map(_.info).getOrElse(0) /* breakpoints */ def breakpoint(range: Text.Range): Option[(Command, Long)] = if (snapshot.is_outdated) None else snapshot.select(range, JEdit_Rendering.breakpoint_elements, command_states => { case Text.Info(_, Protocol.ML_Breakpoint(breakpoint)) => command_states match { case st :: _ => Some((st.command, breakpoint)) case _ => None } case _ => None }).headOption.map(_.info) /* caret focus */ def entity_ref(range: Text.Range, focus: Rendering.Focus): List[Text.Info[Color]] = snapshot.select(range, Rendering.entity_elements, _ => { case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Ref(i)), _)) if focus(i) => Some(entity_ref_color) case _ => None }) /* highlighted area */ def highlight(range: Text.Range): Option[Text.Info[Color]] = snapshot.select(range, JEdit_Rendering.highlight_elements, _ => { case info => Some(Text.Info(snapshot.convert(info.range), highlight_color)) }).headOption.map(_.info) /* hyperlinks */ def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] = { snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]]( range, Vector.empty, JEdit_Rendering.hyperlink_elements, _ => { case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) => val file = perhaps_append_file(snapshot.node_name, name) val link = PIDE.editor.hyperlink_file(true, file) Some(links :+ Text.Info(snapshot.convert(info_range), link)) case (links, Text.Info(info_range, XML.Elem(Markup.Export_Path(name), _))) => val link = PIDE.editor.hyperlink_file(true, Isabelle_Export.vfs_prefix + name) Some(links :+ Text.Info(snapshot.convert(info_range), link)) case (links, Text.Info(info_range, XML.Elem(Markup.Doc(name), _))) => PIDE.editor.hyperlink_doc(name).map(link => (links :+ Text.Info(snapshot.convert(info_range), link))) case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) => val link = PIDE.editor.hyperlink_url(name) Some(links :+ Text.Info(snapshot.convert(info_range), link)) case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) => val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props) opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link)) case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) => val opt_link = PIDE.editor.hyperlink_position(true, snapshot, props) opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link)) case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) => val opt_link = Document_Model.bibtex_entries_iterator().collectFirst( { case Text.Info(entry_range, (entry, model)) if entry == name => PIDE.editor.hyperlink_model(true, model, entry_range.start) }) opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link)) case _ => None }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None } } def hyperlink_entity(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] = { snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]]( range, Vector.empty, Rendering.entity_elements, _ => { case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) => val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props) opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link)) case _ => None }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None } } /* active elements */ def active(range: Text.Range): Option[Text.Info[XML.Elem]] = snapshot.select(range, Rendering.active_elements, command_states => { case Text.Info(info_range, elem) => if (elem.name == Markup.DIALOG) { elem match { case Protocol.Dialog(_, serial, _) if !command_states.exists(st => st.results.defined(serial)) => Some(Text.Info(snapshot.convert(info_range), elem)) case _ => None } } else Some(Text.Info(snapshot.convert(info_range), elem)) }).headOption.map(_.info) /* tooltips */ def tooltip_margin: Int = options.int("jedit_tooltip_margin") override def timing_threshold: Double = options.real("jedit_timing_threshold") def tooltip(range: Text.Range, control: Boolean): Option[Text.Info[XML.Body]] = { val elements = if (control) Rendering.tooltip_elements else Rendering.tooltip_message_elements tooltips(elements, range).map(info => info.map(Pretty.fbreaks)) } lazy val tooltip_close_icon: Icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon")) lazy val tooltip_detach_icon: Icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon")) /* gutter */ private def gutter_message_pri(msg: XML.Tree): Int = if (Protocol.is_error(msg)) Rendering.error_pri else if (Protocol.is_legacy(msg)) Rendering.legacy_pri else if (Protocol.is_warning(msg)) Rendering.warning_pri else if (Protocol.is_information(msg)) Rendering.information_pri else 0 private lazy val gutter_message_content = Map( Rendering.information_pri -> (JEdit_Lib.load_icon(options.string("gutter_information_icon")), color(Rendering.Color.information_message)), Rendering.warning_pri -> (JEdit_Lib.load_icon(options.string("gutter_warning_icon")), color(Rendering.Color.warning_message)), Rendering.legacy_pri -> (JEdit_Lib.load_icon(options.string("gutter_legacy_icon")), color(Rendering.Color.legacy_message)), Rendering.error_pri -> (JEdit_Lib.load_icon(options.string("gutter_error_icon")), color(Rendering.Color.error_message))) def gutter_content(range: Text.Range): Option[(Icon, Color)] = { val pris = snapshot.cumulate[Int](range, 0, JEdit_Rendering.gutter_elements, _ => { case (pri, Text.Info(_, elem)) => Some(pri max gutter_message_pri(elem)) case _ => None }).map(_.info) - gutter_message_content.get((0 /: pris)(_ max _)) + gutter_message_content.get(pris.foldLeft(0)(_ max _)) } /* message output */ def squiggly_underline(range: Text.Range): List[Text.Info[Rendering.Color.Value]] = message_underline_color(JEdit_Rendering.squiggly_elements, range) def line_background(range: Text.Range): Option[(Rendering.Color.Value, Boolean)] = { val results = snapshot.cumulate[Int](range, 0, JEdit_Rendering.line_background_elements, _ => { case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name)) }) - val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 } + val pri = results.foldLeft(0) { case (p1, Text.Info(_, p2)) => p1 max p2 } Rendering.message_background_color.get(pri).map(message_color => { val is_separator = snapshot.cumulate[Boolean](range, false, JEdit_Rendering.separator_elements, _ => { case _ => Some(true) }).exists(_.info) (message_color, is_separator) }) } /* text color */ def text_color(range: Text.Range, current_color: Color): List[Text.Info[Color]] = { if (current_color == Syntax_Style.hidden_color) List(Text.Info(range, current_color)) else snapshot.cumulate(range, current_color, Rendering.text_color_elements, _ => { case (_, Text.Info(_, elem)) => Rendering.text_color.get(elem.name).map(color) }) } /* virtual bullets */ def bullet(range: Text.Range): List[Text.Info[Color]] = snapshot.select(range, JEdit_Rendering.bullet_elements, _ => { case Text.Info(_, Protocol.ML_Breakpoint(breakpoint)) => PIDE.session.debugger.active_breakpoint_state(breakpoint).map(b => if (b) breakpoint_enabled_color else breakpoint_disabled_color) case _ => Some(bullet_color) }) /* text folds */ def fold_depth(range: Text.Range): List[Text.Info[Int]] = snapshot.cumulate[Int](range, 0, JEdit_Rendering.fold_depth_elements, _ => { case (depth, _) => Some(depth + 1) }) } diff --git a/src/Tools/jEdit/src/pretty_tooltip.scala b/src/Tools/jEdit/src/pretty_tooltip.scala --- a/src/Tools/jEdit/src/pretty_tooltip.scala +++ b/src/Tools/jEdit/src/pretty_tooltip.scala @@ -1,290 +1,291 @@ /* Title: Tools/jEdit/src/pretty_tooltip.scala Author: Makarius Tooltip based on Pretty_Text_Area. */ package isabelle.jedit import isabelle._ import java.awt.{Color, Point, BorderLayout, Dimension} import java.awt.event.{FocusAdapter, FocusEvent} import javax.swing.{JPanel, JComponent, SwingUtilities, JLayeredPane} import javax.swing.border.LineBorder import scala.swing.{FlowPanel, Label} import scala.swing.event.MouseClicked import org.gjt.sp.jedit.View import org.gjt.sp.jedit.textarea.TextArea object Pretty_Tooltip { /* tooltip hierarchy */ // owned by GUI thread private var stack: List[Pretty_Tooltip] = Nil private def hierarchy(tip: Pretty_Tooltip): Option[(List[Pretty_Tooltip], List[Pretty_Tooltip])] = { GUI_Thread.require {} if (stack.contains(tip)) Some(stack.span(_ != tip)) else None } private def descendant(parent: JComponent): Option[Pretty_Tooltip] = GUI_Thread.require { stack.find(tip => tip.original_parent == parent) } def apply( view: View, parent: JComponent, location: Point, rendering: JEdit_Rendering, results: Command.Results, info: Text.Info[XML.Body]): Unit = { GUI_Thread.require {} stack match { case top :: _ if top.results == results && top.info == info => case _ => GUI.layered_pane(parent) match { case None => case Some(layered) => val (old, rest) = GUI.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match { case Some(tip) => hierarchy(tip).getOrElse((stack, Nil)) case None => (stack, Nil) } old.foreach(_.hide_popup) val loc = SwingUtilities.convertPoint(parent, location, layered) val tip = new Pretty_Tooltip(view, layered, parent, loc, rendering, results, info) stack = tip :: rest tip.show_popup } } } /* pending event and active state */ // owned by GUI thread private var pending: Option[() => Unit] = None private var active = true private val pending_delay = Delay.last(PIDE.options.seconds("jedit_tooltip_delay"), gui = true) { pending match { case Some(body) => pending = None; body() case None => } } def invoke(body: () => Unit): Unit = GUI_Thread.require { if (active) { pending = Some(body) pending_delay.invoke() } } def revoke(): Unit = GUI_Thread.require { pending = None pending_delay.revoke() } private lazy val reactivate_delay = Delay.last(PIDE.options.seconds("jedit_tooltip_delay"), gui = true) { active = true } private def deactivate(): Unit = GUI_Thread.require { revoke() active = false reactivate_delay.invoke() } /* dismiss */ private lazy val focus_delay = Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { dismiss_unfocused() } def dismiss_unfocused(): Unit = { stack.span(tip => !tip.pretty_text_area.isFocusOwner) match { case (Nil, _) => case (unfocused, rest) => deactivate() unfocused.foreach(_.hide_popup) stack = rest } } def dismiss(tip: Pretty_Tooltip): Unit = { deactivate() hierarchy(tip) match { case Some((old, _ :: rest)) => rest match { case top :: _ => top.request_focus case Nil => JEdit_Lib.request_focus_view() } old.foreach(_.hide_popup) tip.hide_popup stack = rest case _ => } } def dismiss_descendant(parent: JComponent): Unit = descendant(parent).foreach(dismiss) def dismissed_all(): Boolean = { deactivate() if (stack.isEmpty) false else { JEdit_Lib.request_focus_view() stack.foreach(_.hide_popup) stack = Nil true } } } class Pretty_Tooltip private( view: View, layered: JLayeredPane, val original_parent: JComponent, location: Point, rendering: JEdit_Rendering, private val results: Command.Results, private val info: Text.Info[XML.Body]) extends JPanel(new BorderLayout) { tip => GUI_Thread.require {} /* controls */ private val close = new Label { icon = rendering.tooltip_close_icon tooltip = "Close tooltip window" listenTo(mouse.clicks) reactions += { case _: MouseClicked => Pretty_Tooltip.dismiss(tip) } } private val detach = new Label { icon = rendering.tooltip_detach_icon tooltip = "Detach tooltip window" listenTo(mouse.clicks) reactions += { case _: MouseClicked => Info_Dockable(view, rendering.snapshot, results, info.info) Pretty_Tooltip.dismiss(tip) } } private val controls = new FlowPanel(FlowPanel.Alignment.Left)(close, detach) { background = rendering.tooltip_color } /* text area */ val pretty_text_area: Pretty_Text_Area = new Pretty_Text_Area(view, () => Pretty_Tooltip.dismiss(tip), true) { override def get_background() = Some(rendering.tooltip_color) } pretty_text_area.addFocusListener(new FocusAdapter { override def focusGained(e: FocusEvent): Unit = { tip_border(true) Pretty_Tooltip.focus_delay.invoke() } override def focusLost(e: FocusEvent): Unit = { tip_border(false) Pretty_Tooltip.focus_delay.invoke() } }) pretty_text_area.resize(Font_Info.main(PIDE.options.real("jedit_popup_font_scale"))) /* main content */ def tip_border(has_focus: Boolean): Unit = { tip.setBorder(new LineBorder(if (has_focus) Color.BLACK else Color.GRAY)) tip.repaint() } tip_border(true) override def getFocusTraversalKeysEnabled = false tip.setBackground(rendering.tooltip_color) tip.add(controls.peer, BorderLayout.NORTH) tip.add(pretty_text_area) /* popup */ private val popup = { val screen = GUI.screen_location(layered, location) val size = { val bounds = JEdit_Rendering.popup_bounds val w_max = layered.getWidth min (screen.bounds.width * bounds).toInt val h_max = layered.getHeight min (screen.bounds.height * bounds).toInt val painter = pretty_text_area.getPainter val geometry = JEdit_Lib.window_geometry(tip, painter) val metric = JEdit_Lib.pretty_metric(painter) val margin = ((rendering.tooltip_margin * metric.average) min ((w_max - geometry.deco_width) / metric.unit).toInt) max 20 val formatted = Pretty.formatted(info.info, margin = margin, metric = metric) val lines = XML.traverse_text(formatted)(if (XML.text_length(formatted) == 0) 0 else 1)( (n: Int, s: String) => n + s.iterator.count(_ == '\n')) val h = painter.getLineHeight * lines + geometry.deco_height val margin1 = - if (h <= h_max) - (0.0 /: split_lines(XML.content(formatted)))({ case (m, line) => m max metric(line) }) + if (h <= h_max) { + split_lines(XML.content(formatted)).foldLeft(0.0)({ case (m, line) => m max metric(line) }) + } else margin val w = (metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width new Dimension(w min w_max, h min h_max) } new Popup(layered, tip, screen.relative(layered, size), size) } private def show_popup: Unit = { popup.show pretty_text_area.requestFocus pretty_text_area.update(rendering.snapshot, results, info.info) } private def hide_popup: Unit = popup.hide private def request_focus: Unit = pretty_text_area.requestFocus } diff --git a/src/Tools/jEdit/src/text_structure.scala b/src/Tools/jEdit/src/text_structure.scala --- a/src/Tools/jEdit/src/text_structure.scala +++ b/src/Tools/jEdit/src/text_structure.scala @@ -1,354 +1,354 @@ /* Title: Tools/jEdit/src/text_structure.scala Author: Makarius Text structure based on Isabelle/Isar outer syntax. */ package isabelle.jedit import isabelle._ import org.gjt.sp.jedit.indent.{IndentRule, IndentAction} import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher, Selection} import org.gjt.sp.jedit.buffer.JEditBuffer import org.gjt.sp.jedit.Buffer object Text_Structure { /* token navigator */ class Navigator(syntax: Outer_Syntax, buffer: JEditBuffer, comments: Boolean) { val limit: Int = PIDE.options.value.int("jedit_structure_limit") max 0 def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = { val it = Token_Markup.line_token_iterator(syntax, buffer, line, line + lim) if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper) } def reverse_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = { val it = Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim) if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper) } } /* indentation */ object Indent_Rule extends IndentRule { private val keyword_open = Keyword.theory_goal ++ Keyword.proof_open private val keyword_close = Keyword.proof_close def apply(buffer: JEditBuffer, current_line: Int, prev_line0: Int, prev_prev_line0: Int, actions: java.util.List[IndentAction]): Unit = { Isabelle.buffer_syntax(buffer) match { case Some(syntax) => val keywords = syntax.keywords val nav = new Navigator(syntax, buffer, true) val indent_size = buffer.getIndentSize def line_indent(line: Int): Int = if (line < 0 || line >= buffer.getLineCount) 0 else buffer.getCurrentIndentForLine(line, null) def line_head(line: Int): Option[Text.Info[Token]] = nav.iterator(line, 1).nextOption() def head_is_quasi_command(line: Int): Boolean = line_head(line) match { case None => false case Some(Text.Info(_, tok)) => keywords.is_quasi_command(tok) } val prev_line: Int = Range.inclusive(current_line - 1, 0, -1).find(line => Token_Markup.Line_Context.before(buffer, line).get_context == Scan.Finished && (!Token_Markup.Line_Context.after(buffer, line).structure.improper || Token_Markup.Line_Context.after(buffer, line).structure.blank)) getOrElse -1 def prev_line_command: Option[Token] = nav.reverse_iterator(prev_line, 1). collectFirst({ case Text.Info(_, tok) if tok.is_begin_or_command => tok }) def prev_line_span: Iterator[Token] = nav.reverse_iterator(prev_line, 1).map(_.info).takeWhile(tok => !tok.is_begin_or_command) def prev_span: Iterator[Token] = nav.reverse_iterator(prev_line).map(_.info).takeWhile(tok => !tok.is_begin_or_command) val script_indent: Text.Info[Token] => Int = { val opt_rendering: Option[JEdit_Rendering] = if (PIDE.options.value.bool("jedit_indent_script")) GUI_Thread.now { (for { text_area <- JEdit_Lib.jedit_text_areas(buffer) doc_view <- Document_View.get(text_area) } yield doc_view.get_rendering).nextOption() } else None val limit = PIDE.options.value.int("jedit_indent_script_limit") (info: Text.Info[Token]) => opt_rendering match { case Some(rendering) if keywords.is_command(info.info, Keyword.prf_script) => (rendering.indentation(info.range) min limit) max 0 case _ => 0 } } def indent_indent(tok: Token): Int = if (keywords.is_command(tok, keyword_open)) indent_size else if (keywords.is_command(tok, keyword_close)) - indent_size else 0 def indent_offset(tok: Token): Int = if (keywords.is_command(tok, Keyword.proof_enclose)) indent_size else 0 def indent_structure: Int = nav.reverse_iterator(current_line - 1).scanLeft((0, false))( { case ((ind, _), Text.Info(range, tok)) => val ind1 = ind + indent_indent(tok) if (tok.is_begin_or_command && !keywords.is_command(tok, Keyword.prf_script)) { val line = buffer.getLineOfOffset(range.start) line_head(line) match { case Some(info) if info.info == tok => (ind1 + indent_offset(tok) + line_indent(line), true) case _ => (ind1, false) } } else (ind1, false) }).collectFirst({ case (i, true) => i }).getOrElse(0) def indent_brackets: Int = - (0 /: prev_line_span)( + prev_line_span.foldLeft(0)( { case (i, tok) => if (tok.is_open_bracket) i + indent_size else if (tok.is_close_bracket) i - indent_size else i }) def indent_extra: Int = if (prev_span.exists(keywords.is_quasi_command)) indent_size else 0 val indent = if (Token_Markup.Line_Context.before(buffer, current_line).get_context != Scan.Finished) line_indent(current_line) else if (Token_Markup.Line_Context.after(buffer, current_line).structure.blank) 0 else { line_head(current_line) match { case Some(info) => val tok = info.info if (tok.is_begin || keywords.is_before_command(tok) || keywords.is_command(tok, Keyword.theory)) 0 else if (keywords.is_command(tok, Keyword.proof_enclose)) indent_structure + script_indent(info) - indent_offset(tok) else if (keywords.is_command(tok, Keyword.proof)) (indent_structure + script_indent(info) - indent_offset(tok)) max indent_size else if (tok.is_command) indent_structure - indent_offset(tok) else { prev_line_command match { case None => val extra = (keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match { case (true, true) | (false, false) => 0 case (true, false) => - indent_extra case (false, true) => indent_extra } line_indent(prev_line) + indent_brackets + extra - indent_offset(tok) case Some(prev_tok) => indent_structure + indent_brackets + indent_size - indent_offset(tok) - indent_offset(prev_tok) - indent_indent(prev_tok) } } case None => prev_line_command match { case None => val extra = if (head_is_quasi_command(prev_line)) indent_extra else 0 line_indent(prev_line) + indent_brackets + extra case Some(prev_tok) => indent_structure + indent_brackets + indent_size - indent_offset(prev_tok) - indent_indent(prev_tok) } } } actions.clear() actions.add(new IndentAction.AlignOffset(indent max 0)) case None => } } } def line_content(buffer: JEditBuffer, keywords: Keyword.Keywords, range: Text.Range, ctxt: Scan.Line_Context): (List[Token], Scan.Line_Context) = { val text = JEdit_Lib.get_text(buffer, range).getOrElse("") val (toks, ctxt1) = Token.explode_line(keywords, text, ctxt) val toks1 = toks.filterNot(_.is_space) (toks1, ctxt1) } def split_line_content(buffer: JEditBuffer, keywords: Keyword.Keywords, line: Int, caret: Int) : (List[Token], List[Token]) = { val line_range = JEdit_Lib.line_range(buffer, line) val ctxt0 = Token_Markup.Line_Context.before(buffer, line).get_context val (toks1, ctxt1) = line_content(buffer, keywords, Text.Range(line_range.start, caret), ctxt0) val (toks2, _) = line_content(buffer, keywords, Text.Range(caret, line_range.stop), ctxt1) (toks1, toks2) } /* structure matching */ object Matcher extends StructureMatcher { private def find_block( open: Token => Boolean, close: Token => Boolean, reset: Token => Boolean, restrict: Token => Boolean, it: Iterator[Text.Info[Token]]): Option[(Text.Range, Text.Range)] = { val range1 = it.next().range it.takeWhile(info => !info.info.is_command || restrict(info.info)). scanLeft((range1, 1))( { case ((r, d), Text.Info(range, tok)) => if (open(tok)) (range, d + 1) else if (close(tok)) (range, d - 1) else if (reset(tok)) (range, 0) else (r, d) } ).collectFirst({ case (range2, 0) => (range1, range2) }) } private def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] = { val buffer = text_area.getBuffer val caret_line = text_area.getCaretLine val caret = text_area.getCaretPosition Isabelle.buffer_syntax(text_area.getBuffer) match { case Some(syntax) => val keywords = syntax.keywords val nav = new Navigator(syntax, buffer, false) def caret_iterator(): Iterator[Text.Info[Token]] = nav.iterator(caret_line).dropWhile(info => !info.range.touches(caret)) def reverse_caret_iterator(): Iterator[Text.Info[Token]] = nav.reverse_iterator(caret_line).dropWhile(info => !info.range.touches(caret)) nav.iterator(caret_line, 1).find(info => info.range.touches(caret)) match { case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.theory_goal) => find_block( keywords.is_command(_, Keyword.proof_goal), keywords.is_command(_, Keyword.qed), keywords.is_command(_, Keyword.qed_global), t => keywords.is_command(t, Keyword.diag) || keywords.is_command(t, Keyword.proof), caret_iterator()) case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.proof_goal) => find_block( keywords.is_command(_, Keyword.proof_goal), keywords.is_command(_, Keyword.qed), _ => false, t => keywords.is_command(t, Keyword.diag) || keywords.is_command(t, Keyword.proof), caret_iterator()) case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed_global) => reverse_caret_iterator().find(info => keywords.is_command(info.info, Keyword.theory)) match { case Some(Text.Info(range2, tok)) if keywords.is_command(tok, Keyword.theory_goal) => Some((range1, range2)) case _ => None } case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed) => find_block( keywords.is_command(_, Keyword.qed), t => keywords.is_command(t, Keyword.proof_goal) || keywords.is_command(t, Keyword.theory_goal), _ => false, t => keywords.is_command(t, Keyword.diag) || keywords.is_command(t, Keyword.proof) || keywords.is_command(t, Keyword.theory_goal), reverse_caret_iterator()) case Some(Text.Info(range1, tok)) if tok.is_begin => find_block(_.is_begin, _.is_end, _ => false, _ => true, caret_iterator()) case Some(Text.Info(range1, tok)) if tok.is_end => find_block(_.is_end, _.is_begin, _ => false, _ => true, reverse_caret_iterator()) match { case Some((_, range2)) => reverse_caret_iterator(). dropWhile(info => info.range != range2). dropWhile(info => info.range == range2). find(info => info.info.is_command || info.info.is_begin) match { case Some(Text.Info(range3, tok)) => if (keywords.is_command(tok, Keyword.theory_block)) Some((range1, range3)) else Some((range1, range2)) case None => None } case None => None } case _ => None } case None => None } } def getMatch(text_area: TextArea): StructureMatcher.Match = find_pair(text_area) match { case Some((_, range)) => val line = text_area.getBuffer.getLineOfOffset(range.start) new StructureMatcher.Match(Matcher, line, range.start, line, range.stop) case None => null } def selectMatch(text_area: TextArea): Unit = { def get_span(offset: Text.Offset): Option[Text.Range] = for { syntax <- Isabelle.buffer_syntax(text_area.getBuffer) span <- Token_Markup.command_span(syntax, text_area.getBuffer, offset) } yield span.range find_pair(text_area) match { case Some((r1, r2)) => (get_span(r1.start), get_span(r2.start)) match { case (Some(range1), Some(range2)) => val start = range1.start min range2.start val stop = range1.stop max range2.stop text_area.moveCaretPosition(stop, false) if (!text_area.isMultipleSelectionEnabled) text_area.selectNone text_area.addToSelection(new Selection.Range(start, stop)) case _ => } case None => } } } } diff --git a/src/Tools/jEdit/src/theories_dockable.scala b/src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala +++ b/src/Tools/jEdit/src/theories_dockable.scala @@ -1,270 +1,270 @@ /* Title: Tools/jEdit/src/theories_dockable.scala Author: Makarius Dockable window for theories managed by prover. */ package isabelle.jedit import isabelle._ import isabelle.jedit_base.Dockable import scala.swing.{Button, TextArea, Label, ListView, Alignment, ScrollPane, Component, CheckBox, BorderPanel} import scala.swing.event.{ButtonClicked, MouseClicked, MouseMoved} import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension} import javax.swing.{JList, BorderFactory, UIManager} import javax.swing.border.{BevelBorder, SoftBevelBorder} import org.gjt.sp.jedit.{View, jEdit} class Theories_Dockable(view: View, position: String) extends Dockable(view, position) { /* status */ private val status = new ListView(Nil: List[Document.Node.Name]) { background = { // enforce default value val c = UIManager.getDefaults.getColor("Panel.background") new Color(c.getRed, c.getGreen, c.getBlue, c.getAlpha) } listenTo(mouse.clicks) listenTo(mouse.moves) reactions += { case MouseClicked(_, point, _, clicks, _) => val index = peer.locationToIndex(point) if (index >= 0) { if (in_checkbox(peer.indexToLocation(index), point)) { if (clicks == 1) Document_Model.node_required(listData(index), toggle = true) } else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node) } case MouseMoved(_, point, _) => val index = peer.locationToIndex(point) val index_location = peer.indexToLocation(index) if (index >= 0 && in_checkbox(index_location, point)) tooltip = "Mark as required for continuous checking" else if (index >= 0 && in_label(index_location, point)) { val name = listData(index) val st = nodes_status.overall_node_status(name) tooltip = "theory " + quote(name.theory) + (if (st == Document_Status.Overall_Node_Status.ok) "" else " (" + st + ")") } else tooltip = null } } status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP) status.peer.setVisibleRowCount(0) status.selection.intervalMode = ListView.IntervalMode.Single set_content(new ScrollPane(status)) /* controls */ def phase_text(phase: Session.Phase): String = "Prover: " + phase.print private val session_phase = new Label(phase_text(PIDE.session.phase)) session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED) session_phase.tooltip = "Status of prover session" private def handle_phase(phase: Session.Phase): Unit = { GUI_Thread.require {} session_phase.text = " " + phase_text(phase) + " " } private val purge = new Button("Purge") { tooltip = "Restrict document model to theories required for open editor buffers" reactions += { case ButtonClicked(_) => PIDE.editor.purge() } } private val continuous_checking = new Isabelle.Continuous_Checking continuous_checking.focusable = false private val logic = JEdit_Sessions.logic_selector(PIDE.options, true) private val controls = Wrap_Panel(List(purge, continuous_checking, session_phase, logic)) add(controls.peer, BorderLayout.NORTH) /* component state -- owned by GUI thread */ private var nodes_status = Document_Status.Nodes_Status.empty private var nodes_required: Set[Document.Node.Name] = Document_Model.required_nodes() private def in(geometry: Option[(Point, Dimension)], loc0: Point, p: Point): Boolean = geometry match { case Some((loc, size)) => loc0.x + loc.x <= p.x && p.x < loc0.x + size.width && loc0.y + loc.y <= p.y && p.y < loc0.y + size.height case None => false } private def in_checkbox(loc0: Point, p: Point): Boolean = Node_Renderer_Component != null && in(Node_Renderer_Component.checkbox_geometry, loc0, p) private def in_label(loc0: Point, p: Point): Boolean = Node_Renderer_Component != null && in(Node_Renderer_Component.label_geometry, loc0, p) private object Node_Renderer_Component extends BorderPanel { opaque = true border = BorderFactory.createEmptyBorder(2, 2, 2, 2) var node_name = Document.Node.Name.empty var checkbox_geometry: Option[(Point, Dimension)] = None val checkbox = new CheckBox { opaque = false override def paintComponent(gfx: Graphics2D): Unit = { super.paintComponent(gfx) if (location != null && size != null) checkbox_geometry = Some((location, size)) } } var label_geometry: Option[(Point, Dimension)] = None val label = new Label { background = view.getTextArea.getPainter.getBackground foreground = view.getTextArea.getPainter.getForeground opaque = false xAlignment = Alignment.Leading override def paintComponent(gfx: Graphics2D): Unit = { def paint_segment(x: Int, w: Int, color: Color): Unit = { gfx.setColor(color) gfx.fillRect(x, 0, w, size.height) } paint_segment(0, size.width, background) nodes_status.get(node_name) match { case Some(node_status) => val segments = List( (node_status.unprocessed, PIDE.options.color_value("unprocessed1_color")), (node_status.running, PIDE.options.color_value("running_color")), (node_status.warned, PIDE.options.color_value("warning_color")), (node_status.failed, PIDE.options.color_value("error_color")) ).filter(_._1 > 0) - ((size.width - 2) /: segments)({ case (last, (n, color)) => + segments.foldLeft(size.width - 2)({ case (last, (n, color)) => val w = (n * ((size.width - 4) - segments.length) / node_status.total) max 4 paint_segment(last - w, w, color) last - w - 1 }) case None => paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color")) } super.paintComponent(gfx) if (location != null && size != null) label_geometry = Some((location, size)) } } def label_border(name: Document.Node.Name): Unit = { val st = nodes_status.overall_node_status(name) val color = if (st == Document_Status.Overall_Node_Status.failed) PIDE.options.color_value("error_color") else label.foreground val thickness1 = if (st == Document_Status.Overall_Node_Status.pending) 1 else 2 val thickness2 = 3 - thickness1 label.border = BorderFactory.createCompoundBorder( BorderFactory.createLineBorder(color, thickness1), BorderFactory.createEmptyBorder(thickness2, thickness2, thickness2, thickness2)) } layout(checkbox) = BorderPanel.Position.West layout(label) = BorderPanel.Position.Center } private class Node_Renderer extends ListView.Renderer[Document.Node.Name] { def componentFor(list: ListView[_ <: isabelle.Document.Node.Name], isSelected: Boolean, focused: Boolean, name: Document.Node.Name, index: Int): Component = { val component = Node_Renderer_Component component.node_name = name component.checkbox.selected = nodes_required.contains(name) component.label_border(name) component.label.text = name.theory_base_name component } } status.renderer = new Node_Renderer private def handle_update( domain: Option[Set[Document.Node.Name]] = None, trim: Boolean = false): Unit = { GUI_Thread.require {} val snapshot = PIDE.session.snapshot() val (nodes_status_changed, nodes_status1) = nodes_status.update( PIDE.resources, snapshot.state, snapshot.version, domain = domain, trim = trim) nodes_status = nodes_status1 if (nodes_status_changed) { status.listData = (for { (name, node_status) <- nodes_status1.present.iterator if !node_status.is_suppressed && node_status.total > 0 } yield name).toList } } /* main */ private val main = Session.Consumer[Any](getClass.getName) { case phase: Session.Phase => GUI_Thread.later { handle_phase(phase) } case _: Session.Global_Options => GUI_Thread.later { continuous_checking.load() logic.load () nodes_required = Document_Model.required_nodes() status.repaint() } case changed: Session.Commands_Changed => GUI_Thread.later { handle_update(domain = Some(changed.nodes), trim = changed.assignment) } } override def init(): Unit = { PIDE.session.phase_changed += main PIDE.session.global_options += main PIDE.session.commands_changed += main handle_phase(PIDE.session.phase) handle_update() } override def exit(): Unit = { PIDE.session.phase_changed -= main PIDE.session.global_options -= main PIDE.session.commands_changed -= main } } diff --git a/src/Tools/jEdit/src/timing_dockable.scala b/src/Tools/jEdit/src/timing_dockable.scala --- a/src/Tools/jEdit/src/timing_dockable.scala +++ b/src/Tools/jEdit/src/timing_dockable.scala @@ -1,225 +1,225 @@ /* Title: Tools/jEdit/src/timing_dockable.scala Author: Makarius Dockable window for timing information. */ package isabelle.jedit import isabelle._ import isabelle.jedit_base.Dockable import scala.swing.{Label, ListView, Alignment, ScrollPane, Component, TextField} import scala.swing.event.{MouseClicked, ValueChanged} import java.awt.{BorderLayout, Graphics2D, Insets, Color} import javax.swing.{JList, BorderFactory} import javax.swing.border.{BevelBorder, SoftBevelBorder} import org.gjt.sp.jedit.{View, jEdit} class Timing_Dockable(view: View, position: String) extends Dockable(view, position) { /* entry */ private object Entry { object Ordering extends scala.math.Ordering[Entry] { def compare(entry1: Entry, entry2: Entry): Int = entry2.timing compare entry1.timing } object Renderer_Component extends Label { opaque = false xAlignment = Alignment.Leading border = BorderFactory.createEmptyBorder(2, 2, 2, 2) var entry: Entry = null override def paintComponent(gfx: Graphics2D): Unit = { def paint_rectangle(color: Color): Unit = { val size = peer.getSize() val insets = border.getBorderInsets(peer) val x = insets.left val y = insets.top val w = size.width - x - insets.right val h = size.height - y - insets.bottom gfx.setColor(color) gfx.fillRect(x, y, w, h) } entry match { case theory_entry: Theory_Entry if theory_entry.current => paint_rectangle(view.getTextArea.getPainter.getSelectionColor) case _: Command_Entry => paint_rectangle(view.getTextArea.getPainter.getMultipleSelectionColor) case _ => } super.paintComponent(gfx) } } class Renderer extends ListView.Renderer[Entry] { def componentFor(list: ListView[_ <: Timing_Dockable.this.Entry], isSelected: Boolean, focused: Boolean, entry: Entry, index: Int): Component = { val component = Renderer_Component component.entry = entry component.text = entry.print component } } } private abstract class Entry { def timing: Double def print: String def follow(snapshot: Document.Snapshot): Unit } private case class Theory_Entry(name: Document.Node.Name, timing: Double, current: Boolean) extends Entry { def print: String = Time.print_seconds(timing) + "s theory " + quote(name.theory) def follow(snapshot: Document.Snapshot): Unit = PIDE.editor.goto_file(true, view, name.node) } private case class Command_Entry(command: Command, timing: Double) extends Entry { def print: String = " " + Time.print_seconds(timing) + "s command " + quote(command.span.name) def follow(snapshot: Document.Snapshot): Unit = PIDE.editor.hyperlink_command(true, snapshot, command.id).foreach(_.follow(view)) } /* timing view */ private val timing_view = new ListView(Nil: List[Entry]) { listenTo(mouse.clicks) reactions += { case MouseClicked(_, point, _, clicks, _) if clicks == 2 => val index = peer.locationToIndex(point) if (index >= 0) listData(index).follow(PIDE.session.snapshot()) } } timing_view.peer.setLayoutOrientation(JList.VERTICAL_WRAP) timing_view.peer.setVisibleRowCount(0) timing_view.selection.intervalMode = ListView.IntervalMode.Single timing_view.renderer = new Entry.Renderer set_content(new ScrollPane(timing_view)) /* timing threshold */ private var timing_threshold = PIDE.options.real("jedit_timing_threshold") private val threshold_tooltip = "Threshold for timing display (seconds)" private val threshold_label = new Label("Threshold: ") { tooltip = threshold_tooltip } private val threshold_value = new TextField(Time.print_seconds(timing_threshold)) { reactions += { case _: ValueChanged => text match { case Value.Double(x) if x >= 0.0 => timing_threshold = x case _ => } handle_update() } tooltip = threshold_tooltip verifier = ((s: String) => s match { case Value.Double(x) => x >= 0.0 case _ => false }) } private val controls = Wrap_Panel(List(threshold_label, threshold_value)) add(controls.peer, BorderLayout.NORTH) /* component state -- owned by GUI thread */ private var nodes_timing = Map.empty[Document.Node.Name, Document_Status.Overall_Timing] private def make_entries(): List[Entry] = { GUI_Thread.require {} val name = Document_View.get(view.getTextArea) match { case None => Document.Node.Name.empty case Some(doc_view) => doc_view.model.node_name } val timing = nodes_timing.getOrElse(name, Document_Status.Overall_Timing.empty) val theories = (for ((node_name, node_timing) <- nodes_timing.toList if node_timing.command_timings.nonEmpty) yield Theory_Entry(node_name, node_timing.total, false)).sorted(Entry.Ordering) val commands = (for ((command, command_timing) <- timing.command_timings.toList) yield Command_Entry(command, command_timing)).sorted(Entry.Ordering) theories.flatMap(entry => if (entry.name == name) entry.copy(current = true) :: commands else List(entry)) } private def handle_update(restriction: Option[Set[Document.Node.Name]] = None): Unit = { GUI_Thread.require {} val snapshot = PIDE.session.snapshot() - val iterator = - restriction match { + val nodes_timing1 = + (restriction match { case Some(names) => names.iterator.map(name => (name, snapshot.get_node(name))) case None => snapshot.version.nodes.iterator - } - val nodes_timing1 = - (nodes_timing /: iterator)({ case (timing1, (name, node)) => - if (PIDE.resources.session_base.loaded_theory(name)) timing1 - else { - val node_timing = - Document_Status.Overall_Timing.make( - snapshot.state, snapshot.version, node.commands, threshold = timing_threshold) - timing1 + (name -> node_timing) - } }) + .foldLeft(nodes_timing)( + { case (timing1, (name, node)) => + if (PIDE.resources.session_base.loaded_theory(name)) timing1 + else { + val node_timing = + Document_Status.Overall_Timing.make( + snapshot.state, snapshot.version, node.commands, threshold = timing_threshold) + timing1 + (name -> node_timing) + } + }) nodes_timing = nodes_timing1 val entries = make_entries() if (timing_view.listData.toList != entries) timing_view.listData = entries } /* main */ private val main = Session.Consumer[Session.Commands_Changed](getClass.getName) { case changed => GUI_Thread.later { handle_update(Some(changed.nodes)) } } override def init(): Unit = { PIDE.session.commands_changed += main handle_update() } override def exit(): Unit = { PIDE.session.commands_changed -= main } }