# HG changeset patch # User wenzelm # Date 1283157508 -7200 # Node ID 0f861635949db38595d852442486512631a2d15a # Parent 23af89f419bbd51889d561d22f5ed835b9690fc8# Parent 35b2d91e88d762db11e8183f893633831c729ca1 merged diff -r 23af89f419bb -r 0f861635949d src/Pure/Concurrent/future.scala --- a/src/Pure/Concurrent/future.scala Mon Aug 30 10:01:25 2010 +0200 +++ b/src/Pure/Concurrent/future.scala Mon Aug 30 10:38:28 2010 +0200 @@ -28,6 +28,7 @@ { def peek: Option[Exn.Result[A]] def is_finished: Boolean = peek.isDefined + def get_finished: A = { require(is_finished); Exn.release(peek.get) } def join: A def map[B](f: A => B): Future[B] = Future.fork { f(join) } diff -r 23af89f419bb -r 0f861635949d src/Pure/Concurrent/volatile.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Concurrent/volatile.scala Mon Aug 30 10:38:28 2010 +0200 @@ -0,0 +1,22 @@ +/* Title: Pure/Concurrent/volatile.scala + Author: Makarius + +Volatile variables. +*/ + +package isabelle + + +class Volatile[A](init: A) +{ + @volatile private var state: A = init + def peek(): A = state + def change(f: A => A) { state = f(state) } + def change_yield[B](f: A => (B, A)): B = + { + val (result, new_state) = f(state) + state = new_state + result + } +} + diff -r 23af89f419bb -r 0f861635949d src/Pure/General/output.ML --- a/src/Pure/General/output.ML Mon Aug 30 10:01:25 2010 +0200 +++ b/src/Pure/General/output.ML Mon Aug 30 10:38:28 2010 +0200 @@ -79,11 +79,8 @@ (* output primitives -- normally NOT used directly!*) -fun std_output s = NAMED_CRITICAL "IO" (fn () => - (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut)); - -fun std_error s = NAMED_CRITICAL "IO" (fn () => - (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr)); +fun std_output s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut); +fun std_error s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr); fun writeln_default "" = () | writeln_default s = std_output (suffix "\n" s); diff -r 23af89f419bb -r 0f861635949d src/Pure/General/xml.scala --- a/src/Pure/General/xml.scala Mon Aug 30 10:01:25 2010 +0200 +++ b/src/Pure/General/xml.scala Mon Aug 30 10:38:28 2010 +0200 @@ -112,7 +112,7 @@ else lookup(x) match { case Some(y) => y - case None => store(x.map(p => (cache_string(p._1), cache_string(p._2)))) + case None => store(x.map(p => (cache_string(p._1).intern, cache_string(p._2)))) } def cache_markup(x: Markup): Markup = lookup(x) match { diff -r 23af89f419bb -r 0f861635949d src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Mon Aug 30 10:01:25 2010 +0200 +++ b/src/Pure/PIDE/document.scala Mon Aug 30 10:38:28 2010 +0200 @@ -116,7 +116,25 @@ } - /* history navigation and persistent snapshots */ + /* history navigation */ + + object History + { + val init = new History(List(Change.init)) + } + + // FIXME pruning, purging of state + class History(val undo_list: List[Change]) + { + require(!undo_list.isEmpty) + + def tip: Change = undo_list.head + def +(change: Change): History = new History(change :: undo_list) + } + + + + /** global state -- document structure, execution process, editing history **/ abstract class Snapshot { @@ -129,54 +147,10 @@ def convert(range: Text.Range): Text.Range = range.map(convert(_)) def revert(i: Text.Offset): Text.Offset def revert(range: Text.Range): Text.Range = range.map(revert(_)) - } - - object History - { - val init = new History(List(Change.init)) + def select_markup[A](range: Text.Range) + (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] } - // FIXME pruning, purging of state - class History(undo_list: List[Change]) - { - require(!undo_list.isEmpty) - - def tip: Change = undo_list.head - def +(ch: Change): History = new History(ch :: undo_list) - - def snapshot(name: String, pending_edits: List[Text.Edit], state_snapshot: State): Snapshot = - { - val found_stable = undo_list.find(change => - change.is_finished && state_snapshot.is_assigned(change.current.join)) - require(found_stable.isDefined) - val stable = found_stable.get - val latest = undo_list.head - - val edits = - (pending_edits /: undo_list.takeWhile(_ != stable))((edits, change) => - (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits) - lazy val reverse_edits = edits.reverse - - new Snapshot - { - val version = stable.current.join - val node = version.nodes(name) - val is_outdated = !(pending_edits.isEmpty && latest == stable) - def lookup_command(id: Command_ID): Option[Command] = state_snapshot.lookup_command(id) - def state(command: Command): Command.State = - try { state_snapshot.command_state(version, command) } - catch { case _: State.Fail => command.empty_state } - - def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i)) - def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i)) - } - } - } - - - - /** global state -- document structure and execution process **/ - object State { class Fail(state: State) extends Exception @@ -189,6 +163,7 @@ private val promise = Future.promise[Map[Command, Exec_ID]] def is_finished: Boolean = promise.is_finished def join: Map[Command, Exec_ID] = promise.join + def get_finished: Map[Command, Exec_ID] = promise.get_finished def assign(command_execs: List[(Command, Exec_ID)]) { promise.fulfill(tmp_assignment ++ command_execs) @@ -202,7 +177,8 @@ val commands: Map[Command_ID, Command.State] = Map(), val execs: Map[Exec_ID, (Command.State, Set[Version])] = Map(), val assignments: Map[Version, State.Assignment] = Map(), - val disposed: Set[ID] = Set()) // FIXME unused!? + val disposed: Set[ID] = Set(), // FIXME unused!? + val history: History = History.init) { private def fail[A]: A = throw new State.Fail(this) @@ -265,11 +241,61 @@ case None => false } - def command_state(version: Version, command: Command): Command.State = + def extend_history(previous: Future[Version], + edits: List[Node_Text_Edit], + result: Future[(List[Edit[Command]], Version)]): (Change, State) = + { + val change = new Change(previous, edits, result) + (change, copy(history = history + change)) + } + + + // persistent user-view + def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot = { - val assgn = the_assignment(version) - require(assgn.is_finished) - the_exec_state(assgn.join.getOrElse(command, fail)) + val found_stable = history.undo_list.find(change => + change.is_finished && is_assigned(change.current.get_finished)) + require(found_stable.isDefined) + val stable = found_stable.get + val latest = history.undo_list.head + + val edits = + (pending_edits /: history.undo_list.takeWhile(_ != stable))((edits, change) => + (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits) + lazy val reverse_edits = edits.reverse + + new Snapshot + { + val version = stable.current.get_finished + val node = version.nodes(name) + val is_outdated = !(pending_edits.isEmpty && latest == stable) + + def lookup_command(id: Command_ID): Option[Command] = State.this.lookup_command(id) + + def state(command: Command): Command.State = + try { the_exec_state(the_assignment(version).get_finished.getOrElse(command, fail)) } + catch { case _: State.Fail => command.empty_state } + + def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i)) + def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i)) + + def select_markup[A](range: Text.Range) + (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] = + { + val former_range = revert(range) + for { + (command, command_start) <- node.command_range(former_range) + Text.Info(r0, x) <- state(command).markup. + select((former_range - command_start).restrict(command.range)) { + case Text.Info(r0, info) + if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) => + result(Text.Info(convert(r0 + command_start), info)) + } { default } + val r = convert(r0 + command_start) + if !r.is_singularity + } yield Text.Info(r, x) + } + } } } } diff -r 23af89f419bb -r 0f861635949d src/Pure/PIDE/markup_tree.scala --- a/src/Pure/PIDE/markup_tree.scala Mon Aug 30 10:01:25 2010 +0200 +++ b/src/Pure/PIDE/markup_tree.scala Mon Aug 30 10:38:28 2010 +0200 @@ -90,7 +90,7 @@ Branches.overlapping(range, branches).toStream def select[A](root_range: Text.Range) - (result: PartialFunction[Text.Info[Any], A])(default: A): Stream[Text.Info[A]] = + (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] = { def stream(last: Text.Offset, stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])]) : Stream[Text.Info[A]] = @@ -122,6 +122,7 @@ } } stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range)))) + .iterator } def swing_tree(parent: DefaultMutableTreeNode) diff -r 23af89f419bb -r 0f861635949d src/Pure/System/event_bus.scala --- a/src/Pure/System/event_bus.scala Mon Aug 30 10:01:25 2010 +0200 +++ b/src/Pure/System/event_bus.scala Mon Aug 30 10:38:28 2010 +0200 @@ -32,4 +32,29 @@ /* event invocation */ def event(x: Event) { synchronized { receivers.foreach(_ ! x) } } + + + /* await global condition -- triggered via bus events */ + + def await(cond: => Boolean) + { + case object Wait + val a = new Actor { + def act { + if (cond) react { case Wait => reply(()); exit(Wait) } + else { + loop { + react { + case trigger if trigger != Wait => + if (cond) { react { case Wait => reply(()); exit(Wait) } } + } + } + } + } + } + this += a + a.start + a !? Wait + this -= a + } } diff -r 23af89f419bb -r 0f861635949d src/Pure/System/session.scala --- a/src/Pure/System/session.scala Mon Aug 30 10:01:25 2010 +0200 +++ b/src/Pure/System/session.scala Mon Aug 30 10:38:28 2010 +0200 @@ -19,6 +19,7 @@ case object Global_Settings case object Perspective + case object Assignment case class Commands_Changed(set: Set[Command]) } @@ -44,6 +45,7 @@ val raw_output = new Event_Bus[Isabelle_Process.Result] val commands_changed = new Event_Bus[Session.Commands_Changed] val perspective = new Event_Bus[Session.Perspective.type] + val assignments = new Event_Bus[Session.Assignment.type] /* unique ids */ @@ -57,17 +59,64 @@ - /** main actor **/ + /** buffered command changes (delay_first discipline) **/ + + private case object Stop + + private val command_change_buffer = Simple_Thread.actor("command_change_buffer", daemon = true) + //{{{ + { + import scala.compat.Platform.currentTime + + var changed: Set[Command] = Set() + var flush_time: Option[Long] = None + + def flush_timeout: Long = + flush_time match { + case None => 5000L + case Some(time) => (time - currentTime) max 0 + } + + def flush() + { + if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed)) + changed = Set() + flush_time = None + } + + def invoke() + { + val now = currentTime + flush_time match { + case None => flush_time = Some(now + output_delay) + case Some(time) => if (now >= time) flush() + } + } + + var finished = false + while (!finished) { + receiveWithin(flush_timeout) { + case command: Command => changed += command; invoke() + case TIMEOUT => flush() + case Stop => finished = true + case bad => System.err.println("command_change_buffer: ignoring bad message " + bad) + } + } + } + //}}} + + + + /** main protocol actor **/ @volatile private var syntax = new Outer_Syntax(system.symbols) def current_syntax(): Outer_Syntax = syntax - @volatile private var global_state = Document.State.init - private def change_state(f: Document.State => Document.State) { global_state = f(global_state) } - def current_state(): Document.State = global_state + private val global_state = new Volatile(Document.State.init) + def current_state(): Document.State = global_state.peek() + private case class Edit_Version(edits: List[Document.Node_Text_Edit]) private case class Started(timeout: Int, args: List[String]) - private case object Stop private val session_actor = Simple_Thread.actor("session_actor", daemon = true) { @@ -79,12 +128,10 @@ def handle_change(change: Document.Change) //{{{ { - require(change.is_finished) + val previous = change.previous.get_finished + val (node_edits, current) = change.result.get_finished - val previous = change.previous.join - val (node_edits, current) = change.result.join - - var former_assignment = current_state().the_assignment(previous).join + var former_assignment = global_state.peek().the_assignment(previous).get_finished for { (name, Some(cmd_edits)) <- node_edits (prev, None) <- cmd_edits @@ -103,8 +150,8 @@ c2 match { case None => None case Some(command) => - if (current_state().lookup_command(command.id).isEmpty) { - change_state(_.define_command(command)) + if (global_state.peek().lookup_command(command.id).isEmpty) { + global_state.change(_.define_command(command)) prover.define_command(command.id, system.symbols.encode(command.source)) } Some(command.id) @@ -113,7 +160,7 @@ } (name -> Some(ids)) } - change_state(_.define_version(current, former_assignment)) + global_state.change(_.define_version(current, former_assignment)) prover.edit_version(previous.id, current.id, id_edits) } //}}} @@ -134,16 +181,18 @@ result.properties match { case Position.Id(state_id) => try { - val (st, state) = global_state.accumulate(state_id, result.message) - global_state = state - indicate_command_change(st.command) + val st = global_state.change_yield(_.accumulate(state_id, result.message)) + command_change_buffer ! st.command } catch { case _: Document.State.Fail => bad_result(result) } case _ => if (result.is_status) { result.body match { case List(Isar_Document.Assign(id, edits)) => - try { change_state(_.assign(id, edits)) } + try { + global_state.change(_.assign(id, edits)) + assignments.event(Session.Assignment) + } catch { case _: Document.State.Fail => bad_result(result) } case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind) case List(Keyword.Keyword_Decl(name)) => syntax += name @@ -202,6 +251,24 @@ var finished = false while (!finished) { receive { + case Edit_Version(edits) => + val previous = global_state.peek().history.tip.current + val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) } + val change = global_state.change_yield(_.extend_history(previous, edits, result)) + + val this_actor = self + change.current.map(_ => { + assignments.await { global_state.peek().is_assigned(previous.get_finished) } + this_actor ! change }) + + reply(()) + + case change: Document.Change if prover != null => + handle_change(change) + + case result: Isabelle_Process.Result => + handle_result(result) + case Started(timeout, args) => if (prover == null) { prover = new Isabelle_Process(system, self, args:_*) with Isar_Document @@ -219,13 +286,7 @@ finished = true } - case change: Document.Change if prover != null => - handle_change(change) - - case result: Isabelle_Process.Result => - handle_result(result) - - case TIMEOUT => // FIXME clarify! + case TIMEOUT => // FIXME clarify case bad if prover != null => System.err.println("session_actor: ignoring bad message " + bad) @@ -235,95 +296,15 @@ - /** buffered command changes (delay_first discipline) **/ - - private val command_change_buffer = actor - //{{{ - { - import scala.compat.Platform.currentTime - - var changed: Set[Command] = Set() - var flush_time: Option[Long] = None - - def flush_timeout: Long = - flush_time match { - case None => 5000L - case Some(time) => (time - currentTime) max 0 - } - - def flush() - { - if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed)) - changed = Set() - flush_time = None - } - - def invoke() - { - val now = currentTime - flush_time match { - case None => flush_time = Some(now + output_delay) - case Some(time) => if (now >= time) flush() - } - } - - loop { - reactWithin(flush_timeout) { - case command: Command => changed += command; invoke() - case TIMEOUT => flush() - case bad => System.err.println("command_change_buffer: ignoring bad message " + bad) - } - } - } - //}}} - - def indicate_command_change(command: Command) - { - command_change_buffer ! command - } - - - - /** editor history **/ - - private case class Edit_Version(edits: List[Document.Node_Text_Edit]) - - @volatile private var history = Document.History.init - - def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot = - history.snapshot(name, pending_edits, current_state()) - - private val editor_history = actor - { - loop { - react { - case Edit_Version(edits) => - val prev = history.tip.current - val result = - // FIXME potential denial-of-service concerning worker pool (!?!?) - isabelle.Future.fork { - val previous = prev.join - val former_assignment = current_state().the_assignment(previous).join // FIXME async!? - Thy_Syntax.text_edits(Session.this, previous, edits) - } - val change = new Document.Change(prev, edits, result) - history += change - change.current.map(_ => session_actor ! change) - reply(()) - - case bad => System.err.println("editor_model: ignoring bad message " + bad) - } - } - } - - - /** main methods **/ def started(timeout: Int, args: List[String]): Option[String] = (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]] - def stop() { session_actor ! Stop } + def stop() { command_change_buffer ! Stop; session_actor ! Stop } + + def edit_version(edits: List[Document.Node_Text_Edit]) { session_actor !? Edit_Version(edits) } - def edit_version(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Version(edits) } + def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot = + global_state.peek().snapshot(name, pending_edits) } diff -r 23af89f419bb -r 0f861635949d src/Pure/System/swing_thread.scala --- a/src/Pure/System/swing_thread.scala Mon Aug 30 10:01:25 2010 +0200 +++ b/src/Pure/System/swing_thread.scala Mon Aug 30 10:38:28 2010 +0200 @@ -23,7 +23,7 @@ def now[A](body: => A): A = { - var result: Option[A] = None + @volatile var result: Option[A] = None if (SwingUtilities.isEventDispatchThread()) { result = Some(body) } else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } }) result.get diff -r 23af89f419bb -r 0f861635949d src/Pure/build-jars --- a/src/Pure/build-jars Mon Aug 30 10:01:25 2010 +0200 +++ b/src/Pure/build-jars Mon Aug 30 10:38:28 2010 +0200 @@ -24,6 +24,7 @@ declare -a SOURCES=( Concurrent/future.scala Concurrent/simple_thread.scala + Concurrent/volatile.scala General/exn.scala General/linear_set.scala General/markup.scala diff -r 23af89f419bb -r 0f861635949d src/Tools/jEdit/dist-template/etc/settings --- a/src/Tools/jEdit/dist-template/etc/settings Mon Aug 30 10:01:25 2010 +0200 +++ b/src/Tools/jEdit/dist-template/etc/settings Mon Aug 30 10:38:28 2010 +0200 @@ -4,8 +4,8 @@ JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit" JEDIT_OPTIONS="-reuseview -noserver -nobackground" -JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss2m -Dactors.corePoolSize=4" -#JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx1024m -Xss4m -Dactors.corePoolSize=8" +JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false" +#JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx1024m -Xss4m -Dactors.corePoolSize=8 -Dactors.enableForkJoin=false" JEDIT_SYSTEM_OPTIONS="-Dapple.laf.useScreenMenuBar=true -Dcom.apple.mrj.application.apple.menu.about.name=Isabelle/jEdit" JEDIT_STYLE_SHEETS="$ISABELLE_HOME/lib/html/isabelle.css:$JEDIT_HOME/etc/isabelle-jedit.css:$ISABELLE_HOME_USER/etc/isabelle.css:$ISABELLE_HOME_USER/etc/isabelle-jedit.css" diff -r 23af89f419bb -r 0f861635949d src/Tools/jEdit/plugin/Isabelle.props --- a/src/Tools/jEdit/plugin/Isabelle.props Mon Aug 30 10:01:25 2010 +0200 +++ b/src/Tools/jEdit/plugin/Isabelle.props Mon Aug 30 10:38:28 2010 +0200 @@ -29,6 +29,8 @@ options.isabelle.relative-font-size=100 options.isabelle.tooltip-font-size.title=Tooltip Font Size options.isabelle.tooltip-font-size=10 +options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global) +options.isabelle.tooltip-dismiss-delay=8000 options.isabelle.startup-timeout=10000 #menu actions diff -r 23af89f419bb -r 0f861635949d src/Tools/jEdit/src/jedit/document_model.scala --- a/src/Tools/jEdit/src/jedit/document_model.scala Mon Aug 30 10:01:25 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/document_model.scala Mon Aug 30 10:38:28 2010 +0200 @@ -57,9 +57,18 @@ /* line context */ - private val rule_set = new ParserRuleSet("isabelle", "MAIN") - class LineContext(val line: Int, prev: LineContext) - extends TokenMarker.LineContext(rule_set, prev) + private val dummy_rules = new ParserRuleSet("isabelle", "MAIN") + + class Line_Context(val line: Int, prev: Line_Context) + extends TokenMarker.LineContext(dummy_rules, prev) + { + override def hashCode: Int = line + override def equals(that: Any) = + that match { + case other: Line_Context => line == other.line + case _ => false + } + } /* mapping to jEdit token types */ @@ -256,18 +265,15 @@ override def markTokens(prev: TokenMarker.LineContext, handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = { - // FIXME proper synchronization / thread context (!??) - val snapshot = Swing_Thread.now { Document_Model.this.snapshot() } + Isabelle.swing_buffer_lock(buffer) { + val snapshot = Document_Model.this.snapshot() - Isabelle.buffer_read_lock(buffer) { - val previous = prev.asInstanceOf[Document_Model.Token_Markup.LineContext] + val previous = prev.asInstanceOf[Document_Model.Token_Markup.Line_Context] val line = if (prev == null) 0 else previous.line + 1 - val context = new Document_Model.Token_Markup.LineContext(line, previous) + val context = new Document_Model.Token_Markup.Line_Context(line, previous) val start = buffer.getLineStartOffset(line) val stop = start + line_segment.count - val range = Text.Range(start, stop) - val former_range = snapshot.revert(range) /* FIXME for (text_area <- Isabelle.jedit_text_areas(buffer) @@ -290,27 +296,16 @@ Document_Model.Token_Markup.token_style(name) } - var next_x = start - for { - (command, command_start) <- snapshot.node.command_range(former_range) - info <- snapshot.state(command).markup. - select((former_range - command_start).restrict(command.range))(token_markup)(Token.NULL) - val Text.Range(abs_start, abs_stop) = snapshot.convert(info.range + command_start) - if abs_stop > start && abs_start < stop // FIXME abs_range overlaps range (redundant!?) + var last = start + for (token <- snapshot.select_markup(Text.Range(start, stop))(token_markup)(Token.NULL)) { + val Text.Range(token_start, token_stop) = token.range + if (last < token_start) + handle_token(Token.COMMENT1, last - start, token_start - last) + handle_token(token.info, token_start - start, token_stop - token_start) + last = token_stop } - { - val token_start = (abs_start - start) max 0 - val token_length = - (abs_stop - abs_start) - - ((start - abs_start) max 0) - - ((abs_stop - stop) max 0) - if (start + token_start > next_x) // FIXME ?? - handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x) - handle_token(info.info, token_start, token_length) - next_x = start + token_start + token_length - } - if (next_x < stop) // FIXME ?? - handle_token(Token.COMMENT1, next_x - start, stop - next_x) + if (last < stop) + handle_token(Token.COMMENT1, last - start, stop - last) handle_token(Token.END, line_segment.count, 0) handler.setLineContext(context) diff -r 23af89f419bb -r 0f861635949d src/Tools/jEdit/src/jedit/document_view.scala --- a/src/Tools/jEdit/src/jedit/document_view.scala Mon Aug 30 10:01:25 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Mon Aug 30 10:38:28 2010 +0200 @@ -103,29 +103,26 @@ loop { react { case Session.Commands_Changed(changed) => - Swing_Thread.now { - // FIXME cover doc states as well!!? + val buffer = model.buffer + Isabelle.swing_buffer_lock(buffer) { val snapshot = model.snapshot() - val buffer = model.buffer - Isabelle.buffer_read_lock(buffer) { - if (changed.exists(snapshot.node.commands.contains)) { - var visible_change = false + if (changed.exists(snapshot.node.commands.contains)) { + var visible_change = false + for ((command, start) <- snapshot.node.command_starts) { + if (changed(command)) { + val stop = start + command.length + val line1 = buffer.getLineOfOffset(snapshot.convert(start)) + val line2 = buffer.getLineOfOffset(snapshot.convert(stop)) + if (line2 >= text_area.getFirstLine && + line1 <= text_area.getFirstLine + text_area.getVisibleLines) + visible_change = true + text_area.invalidateLineRange(line1, line2) + } + } + // FIXME danger of deadlock!? + if (visible_change) model.buffer.propertiesChanged() - for ((command, start) <- snapshot.node.command_starts) { - if (changed(command)) { - val stop = start + command.length - val line1 = buffer.getLineOfOffset(snapshot.convert(start)) - val line2 = buffer.getLineOfOffset(snapshot.convert(stop)) - if (line2 >= text_area.getFirstLine && - line1 <= text_area.getFirstLine + text_area.getVisibleLines) - visible_change = true - text_area.invalidateLineRange(line1, line2) - } - } - if (visible_change) model.buffer.propertiesChanged() - - overview.repaint() // FIXME paint here!? - } + overview.repaint() // FIXME really paint here!? } } @@ -143,69 +140,64 @@ first_line: Int, last_line: Int, physical_lines: Array[Int], start: Array[Int], end: Array[Int], y0: Int, line_height: Int) { - Swing_Thread.assert() + Isabelle.swing_buffer_lock(model.buffer) { + val snapshot = model.snapshot() - val snapshot = model.snapshot() + val command_range: Iterable[(Command, Text.Offset)] = + { + val range = snapshot.node.command_range(snapshot.revert(start(0))) + if (range.hasNext) { + val (cmd0, start0) = range.next + new Iterable[(Command, Text.Offset)] { + def iterator = + Document.Node.command_starts(snapshot.node.commands.iterator(cmd0), start0) + } + } + else Iterable.empty + } - val command_range: Iterable[(Command, Text.Offset)] = - { - val range = snapshot.node.command_range(snapshot.revert(start(0))) - if (range.hasNext) { - val (cmd0, start0) = range.next - new Iterable[(Command, Text.Offset)] { - def iterator = - Document.Node.command_starts(snapshot.node.commands.iterator(cmd0), start0) + val saved_color = gfx.getColor + try { + var y = y0 + for (i <- 0 until physical_lines.length) { + if (physical_lines(i) != -1) { + val line_start = start(i) + val line_end = model.visible_line_end(line_start, end(i)) + + val a = snapshot.revert(line_start) + val b = snapshot.revert(line_end) + val cmds = command_range.iterator. + dropWhile { case (cmd, c) => c + cmd.length <= a } . + takeWhile { case (_, c) => c < b } + + for ((command, command_start) <- cmds if !command.is_ignored) { + val p = + text_area.offsetToXY(line_start max snapshot.convert(command_start)) + val q = + text_area.offsetToXY(line_end min snapshot.convert(command_start + command.length)) + if (p.y != q.y) System.err.println("Unexpected coordinates: " + p + ", " + q) + gfx.setColor(Document_View.choose_color(snapshot, command)) + gfx.fillRect(p.x, y, q.x - p.x, line_height) + } + } + y += line_height } } - else Iterable.empty + finally { gfx.setColor(saved_color) } } - - val saved_color = gfx.getColor - try { - var y = y0 - for (i <- 0 until physical_lines.length) { - if (physical_lines(i) != -1) { - val line_start = start(i) - val line_end = model.visible_line_end(line_start, end(i)) - - val a = snapshot.revert(line_start) - val b = snapshot.revert(line_end) - val cmds = command_range.iterator. - dropWhile { case (cmd, c) => c + cmd.length <= a } . - takeWhile { case (_, c) => c < b } - - for ((command, command_start) <- cmds if !command.is_ignored) { - val p = - text_area.offsetToXY(line_start max snapshot.convert(command_start)) - val q = - text_area.offsetToXY(line_end min snapshot.convert(command_start + command.length)) - assert(p.y == q.y) - gfx.setColor(Document_View.choose_color(snapshot, command)) - gfx.fillRect(p.x, y, q.x - p.x, line_height) - } - } - y += line_height - } - } - finally { gfx.setColor(saved_color) } } override def getToolTipText(x: Int, y: Int): String = { - Swing_Thread.assert() - - val snapshot = model.snapshot() - val offset = snapshot.revert(text_area.xyToOffset(x, y)) - snapshot.node.command_at(offset) match { - case Some((command, command_start)) => - // FIXME Isar_Document.Tooltip extractor - (snapshot.state(command).markup.select(Text.Range(offset, offset + 1) - command_start) { + Isabelle.swing_buffer_lock(model.buffer) { + val snapshot = model.snapshot() + val offset = text_area.xyToOffset(x, y) + val markup = + snapshot.select_markup(Text.Range(offset, offset + 1)) { case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => - val typing = - Pretty.block(XML.Text(command.source(range) + " : ") :: Pretty.Break(1) :: body) - Isabelle.tooltip(Pretty.string_of(List(typing), margin = 40)) - } { null }).head.info - case None => null + Isabelle.tooltip(Pretty.string_of(List(Pretty.block(body)), margin = 40)) + } { null } + if (markup.hasNext) markup.next.info else null } } } @@ -268,7 +260,7 @@ super.paintComponent(gfx) Swing_Thread.assert() val buffer = model.buffer - Isabelle.buffer_read_lock(buffer) { + Isabelle.buffer_lock(buffer) { val snapshot = model.snapshot() val saved_color = gfx.getColor // FIXME needed!? try { diff -r 23af89f419bb -r 0f861635949d src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Aug 30 10:01:25 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Aug 30 10:38:28 2010 +0200 @@ -29,7 +29,8 @@ { override def click(view: View) = { Isabelle.system.source_file(ref_file) match { - case None => System.err.println("Could not find source file " + ref_file) // FIXME ?? + case None => + Library.error_dialog(view, "File not found", "Could not find source file " + ref_file) case Some(file) => jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line)) } @@ -40,27 +41,24 @@ { def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink = { - // FIXME lock buffer (!??) Swing_Thread.assert() - Document_Model(buffer) match { - case Some(model) => - val snapshot = model.snapshot() - val offset = snapshot.revert(buffer_offset) - snapshot.node.command_at(offset) match { - case Some((command, command_start)) => - // FIXME Isar_Document.Hyperlink extractor - (snapshot.state(command).markup.select(Text.Range(offset, offset + 1) - command_start) { + Isabelle.buffer_lock(buffer) { + Document_Model(buffer) match { + case Some(model) => + val snapshot = model.snapshot() + val markup = + snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1)) { + // FIXME Isar_Document.Hyperlink extractor case Text.Info(info_range, XML.Elem(Markup(Markup.ML_REF, _), List(XML.Elem(Markup(Markup.ML_DEF, props), _)))) => - val Text.Range(begin, end) = snapshot.convert(info_range + command_start) + val Text.Range(begin, end) = info_range val line = buffer.getLineOfOffset(begin) - (Position.File.unapply(props), Position.Line.unapply(props)) match { case (Some(ref_file), Some(ref_line)) => new External_Hyperlink(begin, end, line, ref_file, ref_line) case _ => - (Position.Id.unapply(props), Position.Offset.unapply(props)) match { - case (Some(ref_id), Some(ref_offset)) => + (props, props) match { + case (Position.Id(ref_id), Position.Offset(ref_offset)) => snapshot.lookup_command(ref_id) match { case Some(ref_cmd) => snapshot.node.command_start(ref_cmd) match { @@ -74,10 +72,11 @@ case _ => null } } - } { null }).head.info - case None => null - } - case None => null + } { null } + if (markup.hasNext) markup.next.info else null + + case None => null + } } } } diff -r 23af89f419bb -r 0f861635949d src/Tools/jEdit/src/jedit/isabelle_options.scala --- a/src/Tools/jEdit/src/jedit/isabelle_options.scala Mon Aug 30 10:01:25 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala Mon Aug 30 10:38:28 2010 +0200 @@ -17,6 +17,7 @@ private val logic_name = new JComboBox() private val relative_font_size = new JSpinner() private val tooltip_font_size = new JSpinner() + private val tooltip_dismiss_delay = new JSpinner() private class List_Item(val name: String, val descr: String) { def this(name: String) = this(name, name) @@ -46,6 +47,11 @@ tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 10)) tooltip_font_size }) + + addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), { + tooltip_dismiss_delay.setValue(Isabelle.Int_Property("tooltip-dismiss-delay", 8000)) + tooltip_dismiss_delay + }) } override def _save() @@ -58,5 +64,8 @@ Isabelle.Int_Property("tooltip-font-size") = tooltip_font_size.getValue().asInstanceOf[Int] + + Isabelle.Int_Property("tooltip-dismiss-delay") = + tooltip_dismiss_delay.getValue().asInstanceOf[Int] } } diff -r 23af89f419bb -r 0f861635949d src/Tools/jEdit/src/jedit/plugin.scala --- a/src/Tools/jEdit/src/jedit/plugin.scala Mon Aug 30 10:01:25 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/plugin.scala Mon Aug 30 10:38:28 2010 +0200 @@ -81,6 +81,17 @@ Int_Property("tooltip-font-size", 10).toString + "px; \">" + // FIXME proper scaling (!?) HTML.encode(text) + "" + def tooltip_dismiss_delay(): Int = + Int_Property("tooltip-dismiss-delay", 8000) max 500 + + def setup_tooltips() + { + Swing_Thread.now { + val manager = javax.swing.ToolTipManager.sharedInstance + manager.setDismissDelay(tooltip_dismiss_delay()) + } + } + /* settings */ @@ -118,12 +129,15 @@ def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] = jedit_text_areas().filter(_.getBuffer == buffer) - def buffer_read_lock[A](buffer: JEditBuffer)(body: => A): A = + def buffer_lock[A](buffer: JEditBuffer)(body: => A): A = { try { buffer.readLock(); body } finally { buffer.readUnlock() } } + def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A = + Swing_Thread.now { buffer_lock(buffer) { body } } + /* dockable windows */ @@ -240,6 +254,8 @@ Swing_Thread.now { for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined) Document_View(text_area).get.extend_styles() + + Isabelle.setup_tooltips() } Isabelle.session.global_settings.event(Session.Global_Settings) @@ -253,6 +269,8 @@ Isabelle.system = new Isabelle_System Isabelle.system.install_fonts() Isabelle.session = new Session(Isabelle.system) // FIXME dialog!? + + Isabelle.setup_tooltips() } override def stop()