--- 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) }
--- /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
+ }
+}
+
--- 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);
--- 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 {
--- 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)
+ }
+ }
}
}
}
--- 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)
--- 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
+ }
}
--- 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)
}
--- 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
--- 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
--- 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"
--- 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
--- 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)
--- 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 {
--- 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
+ }
}
}
}
--- 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]
}
}
--- 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) + "</pre></html>"
+ 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()