# HG changeset patch # User wenzelm # Date 1396091124 -3600 # Node ID 4e589bcab2570256a55ba801fc4641ee1f61d792 # Parent b61fd250700654152f4d3fc229fa12cb6ed5bdb6# Parent 1147854080b4c3d304085cebd37cada32048417b merged diff -r b61fd2507006 -r 4e589bcab257 src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Sat Mar 29 11:41:39 2014 +0100 +++ b/src/Pure/Isar/outer_syntax.scala Sat Mar 29 12:05:24 2014 +0100 @@ -57,13 +57,13 @@ def keyword_kind_files(name: String): Option[(String, List[String])] = keywords.get(name) def keyword_kind(name: String): Option[String] = keyword_kind_files(name).map(_._1) - def thy_load(span: List[Token]): Option[List[String]] = + def load(span: List[Token]): Option[List[String]] = keywords.get(Command.name(span)) match { case Some((Keyword.THY_LOAD, exts)) => Some(exts) case _ => None } - val thy_load_commands: List[(String, List[String])] = + val load_commands: List[(String, List[String])] = (for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax = diff -r b61fd2507006 -r 4e589bcab257 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sat Mar 29 11:41:39 2014 +0100 +++ b/src/Pure/PIDE/document.scala Sat Mar 29 12:05:24 2014 +0100 @@ -189,7 +189,7 @@ final class Commands private(val commands: Linear_Set[Command]) { - lazy val thy_load_commands: List[Command] = + lazy val load_commands: List[Command] = commands.iterator.filter(cmd => !cmd.blobs.isEmpty).toList private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) = @@ -244,7 +244,7 @@ perspective.overlays == other_perspective.overlays def commands: Linear_Set[Command] = _commands.commands - def thy_load_commands: List[Command] = _commands.thy_load_commands + def load_commands: List[Command] = _commands.load_commands def update_commands(new_commands: Linear_Set[Command]): Node = if (new_commands eq _commands.commands) this @@ -290,10 +290,10 @@ def entries: Iterator[(Node.Name, Node)] = graph.entries.map({ case (name, (node, _)) => (name, node) }) - def thy_load_commands(file_name: Node.Name): List[Command] = + def load_commands(file_name: Node.Name): List[Command] = (for { (_, node) <- entries - cmd <- node.thy_load_commands.iterator + cmd <- node.load_commands.iterator name <- cmd.blobs_names.iterator if name == file_name } yield cmd).toList @@ -421,7 +421,7 @@ val node_name: Node.Name val node: Node - val thy_load_commands: List[Command] + val load_commands: List[Command] def is_loaded: Boolean def eq_content(other: Snapshot): Boolean @@ -694,11 +694,11 @@ val node_name = name val node = version.nodes(name) - val thy_load_commands: List[Command] = + val load_commands: List[Command] = if (node_name.is_theory) Nil - else version.nodes.thy_load_commands(node_name) + else version.nodes.load_commands(node_name) - val is_loaded: Boolean = node_name.is_theory || !thy_load_commands.isEmpty + val is_loaded: Boolean = node_name.is_theory || !load_commands.isEmpty def eq_content(other: Snapshot): Boolean = { @@ -713,8 +713,8 @@ !is_outdated && !other.is_outdated && node.commands.size == other.node.commands.size && (node.commands.iterator zip other.node.commands.iterator).forall(eq_commands) && - thy_load_commands.length == other.thy_load_commands.length && - (thy_load_commands zip other.thy_load_commands).forall(eq_commands) + load_commands.length == other.load_commands.length && + (load_commands zip other.load_commands).forall(eq_commands) } @@ -729,7 +729,7 @@ { val former_range = revert(range) val (file_name, command_range_iterator) = - thy_load_commands match { + load_commands match { case command :: _ => (node_name.node, Iterator((command, 0))) case _ => ("", node.command_range(former_range)) } diff -r b61fd2507006 -r 4e589bcab257 src/Pure/PIDE/markup_tree.scala --- a/src/Pure/PIDE/markup_tree.scala Sat Mar 29 11:41:39 2014 +0100 +++ b/src/Pure/PIDE/markup_tree.scala Sat Mar 29 12:05:24 2014 +0100 @@ -118,7 +118,7 @@ private def overlapping(range: Text.Range): Branches.T = if (branches.isEmpty || - (range.contains(branches.firstKey.start) && range.contains(branches.lastKey.stop))) + (range.contains(branches.firstKey.start) && branches.lastKey.stop <= range.stop)) branches else { val start = Text.Range(range.start) diff -r b61fd2507006 -r 4e589bcab257 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Sat Mar 29 11:41:39 2014 +0100 +++ b/src/Pure/PIDE/resources.scala Sat Mar 29 12:05:24 2014 +0100 @@ -51,7 +51,7 @@ /* theory files */ def body_files_test(syntax: Outer_Syntax, text: String): Boolean = - syntax.thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) }) + syntax.load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) }) def body_files(syntax: Outer_Syntax, text: String): List[String] = { @@ -91,15 +91,15 @@ with_thy_text(name, check_thy_text(name, _)) - /* theory text edits */ + /* document changes */ - def text_edits( - reparse_limit: Int, - previous: Document.Version, - doc_blobs: Document.Blobs, - edits: List[Document.Edit_Text]): (Boolean, List[Document.Edit_Command], Document.Version) = - Thy_Syntax.text_edits(this, reparse_limit, previous, doc_blobs, edits) + def parse_change( + reparse_limit: Int, + previous: Document.Version, + doc_blobs: Document.Blobs, + edits: List[Document.Edit_Text]): Session.Change = + Thy_Syntax.parse_change(this, reparse_limit, previous, doc_blobs, edits) - def syntax_changed() { } + def commit(change: Session.Change) { } } diff -r b61fd2507006 -r 4e589bcab257 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Sat Mar 29 11:41:39 2014 +0100 +++ b/src/Pure/PIDE/session.scala Sat Mar 29 12:05:24 2014 +0100 @@ -18,6 +18,17 @@ object Session { + /* change */ + + sealed case class Change( + previous: Document.Version, + doc_blobs: Document.Blobs, + syntax_changed: Boolean, + deps_changed: Boolean, + doc_edits: List[Document.Edit_Command], + version: Document.Version) + + /* events */ //{{{ @@ -179,12 +190,12 @@ case Text_Edits(previous, doc_blobs, text_edits, version_result) => val prev = previous.get_finished - val (syntax_changed, doc_edits, version) = - Timing.timeit("text_edits", timing) { - resources.text_edits(reparse_limit, prev, doc_blobs, text_edits) + val change = + Timing.timeit("parse_change", timing) { + resources.parse_change(reparse_limit, prev, doc_blobs, text_edits) } - version_result.fulfill(version) - sender ! Change(doc_blobs, syntax_changed, doc_edits, prev, version) + version_result.fulfill(change.version) + sender ! change case bad => System.err.println("change_parser: ignoring bad message " + bad) } @@ -249,12 +260,6 @@ private case class Start(args: List[String]) private case class Cancel_Exec(exec_id: Document_ID.Exec) - private case class Change( - doc_blobs: Document.Blobs, - syntax_changed: Boolean, - doc_edits: List[Document.Edit_Command], - previous: Document.Version, - version: Document.Version) private case class Protocol_Command(name: String, args: List[String]) private case class Messages(msgs: List[Isabelle_Process.Message]) private case class Update_Options(options: Options) @@ -367,18 +372,16 @@ /* resulting changes */ - def handle_change(change: Change) + def handle_change(change: Session.Change) //{{{ { - val Change(doc_blobs, syntax_changed, doc_edits, previous, version) = change - def id_command(command: Command) { for { digest <- command.blobs_digests if !global_state().defined_blob(digest) } { - doc_blobs.get(digest) match { + change.doc_blobs.get(digest) match { case Some(blob) => global_state >> (_.define_blob(digest)) prover.get.define_blob(blob) @@ -392,16 +395,15 @@ prover.get.define_command(command) } } - doc_edits foreach { + change.doc_edits foreach { case (_, edit) => edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command } } - val assignment = global_state().the_assignment(previous).check_finished - global_state >> (_.define_version(version, assignment)) - prover.get.update(previous.id, version.id, doc_edits) - - if (syntax_changed) resources.syntax_changed() + val assignment = global_state().the_assignment(change.previous).check_finished + global_state >> (_.define_version(change.version, assignment)) + prover.get.update(change.previous.id, change.version.id, change.doc_edits) + resources.commit(change) } //}}} @@ -556,11 +558,11 @@ all_messages.event(output) } - case change: Change + case change: Session.Change if prover.isDefined && global_state().is_assigned(change.previous) => handle_change(change) - case bad if !bad.isInstanceOf[Change] => + case bad if !bad.isInstanceOf[Session.Change] => System.err.println("session_actor: ignoring bad message " + bad) } } diff -r b61fd2507006 -r 4e589bcab257 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Sat Mar 29 11:41:39 2014 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Sat Mar 29 12:05:24 2014 +0100 @@ -156,7 +156,8 @@ base_syntax: Outer_Syntax, previous: Document.Version, edits: List[Document.Edit_Text]): - ((Outer_Syntax, Boolean), List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) = + (Outer_Syntax, Boolean, Boolean, List[Document.Node.Name], Document.Nodes, + List[Document.Edit_Command]) = { var updated_imports = false var updated_keywords = false @@ -178,7 +179,7 @@ case _ => } - val syntax = + val (syntax, syntax_changed) = if (previous.is_init || updated_keywords) { val syntax = (base_syntax /: nodes.entries) { @@ -193,7 +194,7 @@ nodes.descendants(doc_edits.iterator.map(_._1).toList) else Nil - (syntax, reparse, nodes, doc_edits.toList) + (syntax, syntax_changed, updated_imports, reparse, nodes, doc_edits.toList) } @@ -245,7 +246,7 @@ } def span_files(syntax: Outer_Syntax, span: List[Token]): List[String] = - syntax.thy_load(span) match { + syntax.load(span) match { case Some(exts) => find_file(span) match { case Some(file) => @@ -431,58 +432,59 @@ } } - def text_edits( + def parse_change( resources: Resources, reparse_limit: Int, previous: Document.Version, doc_blobs: Document.Blobs, - edits: List[Document.Edit_Text]) - : (Boolean, List[Document.Edit_Command], Document.Version) = + edits: List[Document.Edit_Text]): Session.Change = { - val ((syntax, syntax_changed), reparse0, nodes0, doc_edits0) = + val (syntax, syntax_changed, deps_changed, reparse0, nodes0, doc_edits0) = header_edits(resources.base_syntax, previous, edits) - if (edits.isEmpty) - (false, Nil, Document.Version.make(syntax, previous.nodes)) - else { - val reparse = - (reparse0 /: nodes0.entries)({ - case (reparse, (name, node)) => - if (node.thy_load_commands.exists(_.blobs_changed(doc_blobs))) - name :: reparse - else reparse - }) - val reparse_set = reparse.toSet + val (doc_edits, version) = + if (edits.isEmpty) (Nil, Document.Version.make(syntax, previous.nodes)) + else { + val reparse = + (reparse0 /: nodes0.entries)({ + case (reparse, (name, node)) => + if (node.load_commands.exists(_.blobs_changed(doc_blobs))) + name :: reparse + else reparse + }) + val reparse_set = reparse.toSet - var nodes = nodes0 - val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0 + var nodes = nodes0 + val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0 - val node_edits = - (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1) - .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]] // FIXME ??? + val node_edits = + (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1) + .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]] // FIXME ??? - node_edits foreach { - case (name, edits) => - val node = nodes(name) - val commands = node.commands + node_edits foreach { + case (name, edits) => + val node = nodes(name) + val commands = node.commands - val node1 = - if (reparse_set(name) && !commands.isEmpty) - node.update_commands( - reparse_spans(resources, syntax, doc_blobs, - name, commands, commands.head, commands.last)) - else node - val node2 = (node1 /: edits)(text_edit(resources, syntax, doc_blobs, reparse_limit, _, _)) + val node1 = + if (reparse_set(name) && !commands.isEmpty) + node.update_commands( + reparse_spans(resources, syntax, doc_blobs, + name, commands, commands.head, commands.last)) + else node + val node2 = + (node1 /: edits)(text_edit(resources, syntax, doc_blobs, reparse_limit, _, _)) - if (!(node.same_perspective(node2.perspective))) - doc_edits += (name -> node2.perspective) + if (!(node.same_perspective(node2.perspective))) + doc_edits += (name -> node2.perspective) - doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands))) + doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands))) - nodes += (name -> node2) + nodes += (name -> node2) + } + (doc_edits.toList, Document.Version.make(syntax, nodes)) } - (syntax_changed, doc_edits.toList, Document.Version.make(syntax, nodes)) - } + Session.Change(previous, doc_blobs, syntax_changed, deps_changed, doc_edits, version) } } diff -r b61fd2507006 -r 4e589bcab257 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Sat Mar 29 11:41:39 2014 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Sat Mar 29 12:05:24 2014 +0100 @@ -115,9 +115,9 @@ } else Nil - val thy_load_ranges = + val load_ranges = for { - cmd <- snapshot.node.thy_load_commands + cmd <- snapshot.node.load_commands blob_name <- cmd.blobs_names blob_buffer <- JEdit_Lib.jedit_buffer(blob_name.node) if !JEdit_Lib.jedit_text_areas(blob_buffer).isEmpty @@ -125,11 +125,11 @@ range = snapshot.convert(cmd.proper_range + start) } yield range - val reparse = snapshot.node.thy_load_commands.exists(_.blobs_changed(doc_blobs)) + val reparse = snapshot.node.load_commands.exists(_.blobs_changed(doc_blobs)) (reparse, Document.Node.Perspective(node_required, - Text.Perspective(document_view_ranges ::: thy_load_ranges), + Text.Perspective(document_view_ranges ::: load_ranges), PIDE.editor.node_overlays(node_name))) } else (false, empty_perspective) diff -r b61fd2507006 -r 4e589bcab257 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Sat Mar 29 11:41:39 2014 +0100 +++ b/src/Tools/jEdit/src/document_view.scala Sat Mar 29 12:05:24 2014 +0100 @@ -210,17 +210,17 @@ if (model.buffer == text_area.getBuffer) { val snapshot = model.snapshot() - val thy_load_changed = - snapshot.thy_load_commands.exists(changed.commands.contains) + val load_changed = + snapshot.load_commands.exists(changed.commands.contains) - if (changed.assignment || thy_load_changed || + if (changed.assignment || load_changed || (changed.nodes.contains(model.node_name) && changed.commands.exists(snapshot.node.commands.contains))) Swing_Thread.later { overview.delay_repaint.invoke() } val visible_lines = text_area.getVisibleLines if (visible_lines > 0) { - if (changed.assignment || thy_load_changed) + if (changed.assignment || load_changed) text_area.invalidateScreenLineRange(0, visible_lines) else { val visible_range = JEdit_Lib.visible_range(text_area).get diff -r b61fd2507006 -r 4e589bcab257 src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Sat Mar 29 11:41:39 2014 +0100 +++ b/src/Tools/jEdit/src/jedit_editor.scala Sat Mar 29 12:05:24 2014 +0100 @@ -85,7 +85,7 @@ case _ => PIDE.document_model(buffer) match { case Some(model) if !model.is_theory => - snapshot.version.nodes.thy_load_commands(model.node_name) match { + snapshot.version.nodes.load_commands(model.node_name) match { case cmd :: _ => Some(cmd) case Nil => None } diff -r b61fd2507006 -r 4e589bcab257 src/Tools/jEdit/src/jedit_resources.scala --- a/src/Tools/jEdit/src/jedit_resources.scala Sat Mar 29 11:41:39 2014 +0100 +++ b/src/Tools/jEdit/src/jedit_resources.scala Sat Mar 29 12:05:24 2014 +0100 @@ -117,7 +117,10 @@ /* theory text edits */ - override def syntax_changed(): Unit = - Swing_Thread.later { jEdit.propertiesChanged() } + override def commit(change: Session.Change) + { + if (change.syntax_changed) Swing_Thread.later { jEdit.propertiesChanged() } + if (change.deps_changed) PIDE.deps_changed() + } } diff -r b61fd2507006 -r 4e589bcab257 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Sat Mar 29 11:41:39 2014 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Sat Mar 29 12:05:24 2014 +0100 @@ -39,6 +39,7 @@ @volatile var session: Session = new Session(new JEdit_Resources(Set.empty, Outer_Syntax.empty)) def options_changed() { plugin.options_changed() } + def deps_changed() { plugin.deps_changed() } def resources(): JEdit_Resources = session.resources.asInstanceOf[JEdit_Resources] @@ -168,13 +169,19 @@ class Plugin extends EBPlugin { - /* options */ + /* global changes */ - def options_changed() { + def options_changed() + { PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value)) Swing_Thread.later { delay_load.invoke() } } + def deps_changed() + { + Swing_Thread.later { delay_load.invoke() } + } + /* theory files */ diff -r b61fd2507006 -r 4e589bcab257 src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Sat Mar 29 11:41:39 2014 +0100 +++ b/src/Tools/jEdit/src/rich_text_area.scala Sat Mar 29 12:05:24 2014 +0100 @@ -10,7 +10,7 @@ import isabelle._ -import java.awt.{Graphics2D, Shape, Color, Point, Toolkit} +import java.awt.{Graphics2D, Shape, Color, Point, Toolkit, Cursor} import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent, FocusAdapter, FocusEvent, WindowEvent, WindowAdapter} import java.awt.font.TextAttribute @@ -100,7 +100,9 @@ /* active areas within the text */ - private class Active_Area[A](rendering: Rendering => Text.Range => Option[Text.Info[A]]) + private class Active_Area[A]( + rendering: Rendering => Text.Range => Option[Text.Info[A]], + cursor: Option[Int]) { private var the_text_info: Option[(String, Text.Info[A])] = None @@ -115,6 +117,12 @@ new_info.map(info => (text_area.getText(info.range.start, info.range.length), info)) if (new_text_info != old_text_info) { + if (cursor.isDefined) { + if (new_text_info.isDefined) + text_area.getPainter.setCursor(Cursor.getPredefinedCursor(cursor.get)) + else + text_area.getPainter.resetCursor + } for { r0 <- JEdit_Lib.visible_range(text_area) opt <- List(old_text_info, new_text_info) @@ -133,10 +141,13 @@ // owned by Swing thread - private val highlight_area = new Active_Area[Color]((r: Rendering) => r.highlight _) + private val highlight_area = + new Active_Area[Color]((r: Rendering) => r.highlight _, None) private val hyperlink_area = - new Active_Area[PIDE.editor.Hyperlink]((r: Rendering) => r.hyperlink _) - private val active_area = new Active_Area[XML.Elem]((r: Rendering) => r.active _) + new Active_Area[PIDE.editor.Hyperlink]( + (r: Rendering) => r.hyperlink _, Some(Cursor.HAND_CURSOR)) + private val active_area = + new Active_Area[XML.Elem]((r: Rendering) => r.active _, Some(Cursor.DEFAULT_CURSOR)) private val active_areas = List((highlight_area, true), (hyperlink_area, true), (active_area, false))