1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Pure/Concurrent/simple_thread.scala Mon Aug 23 17:46:13 2010 +0200
1.3 @@ -0,0 +1,37 @@
1.4 +/* Title: Pure/Concurrent/simple_thread.scala
1.5 + Author: Makarius
1.6 +
1.7 +Simplified thread operations.
1.8 +*/
1.9 +
1.10 +package isabelle
1.11 +
1.12 +
1.13 +import java.lang.Thread
1.14 +
1.15 +import scala.actors.Actor
1.16 +
1.17 +
1.18 +object Simple_Thread
1.19 +{
1.20 + /* plain thread */
1.21 +
1.22 + def fork(name: String, daemon: Boolean = false)(body: => Unit): Thread =
1.23 + {
1.24 + val thread = new Thread(name) { override def run = body }
1.25 + thread.setDaemon(daemon)
1.26 + thread.start
1.27 + thread
1.28 + }
1.29 +
1.30 +
1.31 + /* thread as actor */
1.32 +
1.33 + def actor(name: String, daemon: Boolean = false)(body: => Unit): Actor =
1.34 + {
1.35 + val actor = Future.promise[Actor]
1.36 + val thread = fork(name, daemon) { actor.fulfill(Actor.self); body }
1.37 + actor.join
1.38 + }
1.39 +}
1.40 +
2.1 --- a/src/Pure/General/table.ML Mon Aug 23 15:30:42 2010 +0200
2.2 +++ b/src/Pure/General/table.ML Mon Aug 23 17:46:13 2010 +0200
2.3 @@ -392,6 +392,16 @@
2.4 fun merge_list eq = join (fn _ => Library.merge eq);
2.5
2.6
2.7 +(* ML pretty-printing -- requires Poly/ML 5.3.0 or later *)
2.8 +
2.9 +val _ =
2.10 + PolyML.addPrettyPrinter (fn depth => fn pretty => fn tab =>
2.11 + ml_pretty
2.12 + (ML_Pretty.enum "," "{" "}"
2.13 + (ML_Pretty.pair (pretty_ml o PolyML.prettyRepresentation) (pretty_ml o pretty))
2.14 + (dest tab, depth)));
2.15 +
2.16 +
2.17 (*final declarations of this structure!*)
2.18 fun map f = map_table (K f);
2.19 val map' = map_table;
3.1 --- a/src/Pure/IsaMakefile Mon Aug 23 15:30:42 2010 +0200
3.2 +++ b/src/Pure/IsaMakefile Mon Aug 23 17:46:13 2010 +0200
3.3 @@ -32,6 +32,7 @@
3.4 ML-Systems/polyml-5.2.ML \
3.5 ML-Systems/polyml.ML \
3.6 ML-Systems/polyml_common.ML \
3.7 + ML-Systems/pp_dummy.ML \
3.8 ML-Systems/pp_polyml.ML \
3.9 ML-Systems/proper_int.ML \
3.10 ML-Systems/single_assignment.ML \
4.1 --- a/src/Pure/ML-Systems/ml_pretty.ML Mon Aug 23 15:30:42 2010 +0200
4.2 +++ b/src/Pure/ML-Systems/ml_pretty.ML Mon Aug 23 17:46:13 2010 +0200
4.3 @@ -1,7 +1,7 @@
4.4 (* Title: Pure/ML-Systems/ml_pretty.ML
4.5 Author: Makarius
4.6
4.7 -Raw datatype for ML pretty printing.
4.8 +Minimal support for raw ML pretty printing -- for boot-strapping only.
4.9 *)
4.10
4.11 structure ML_Pretty =
4.12 @@ -12,5 +12,20 @@
4.13 String of string * int |
4.14 Break of bool * int;
4.15
4.16 +fun block prts = Block (("", ""), prts, 2);
4.17 +fun str s = String (s, size s);
4.18 +fun brk wd = Break (false, wd);
4.19 +
4.20 +fun pair pretty1 pretty2 ((x, y), depth: int) =
4.21 + block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
4.22 +
4.23 +fun enum sep lpar rpar pretty (args, depth) =
4.24 + let
4.25 + fun elems _ [] = []
4.26 + | elems 0 _ = [str "..."]
4.27 + | elems d [x] = [pretty (x, d)]
4.28 + | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
4.29 + in block (str lpar :: (elems (Int.max (depth, 0)) args @ [str rpar])) end;
4.30 +
4.31 end;
4.32
5.1 --- a/src/Pure/ML-Systems/polyml-5.2.1.ML Mon Aug 23 15:30:42 2010 +0200
5.2 +++ b/src/Pure/ML-Systems/polyml-5.2.1.ML Mon Aug 23 17:46:13 2010 +0200
5.3 @@ -25,4 +25,5 @@
5.4
5.5 use "ML-Systems/compiler_polyml-5.2.ML";
5.6 use "ML-Systems/pp_polyml.ML";
5.7 +use "ML-Systems/pp_dummy.ML";
5.8
6.1 --- a/src/Pure/ML-Systems/polyml-5.2.ML Mon Aug 23 15:30:42 2010 +0200
6.2 +++ b/src/Pure/ML-Systems/polyml-5.2.ML Mon Aug 23 17:46:13 2010 +0200
6.3 @@ -27,4 +27,5 @@
6.4
6.5 use "ML-Systems/compiler_polyml-5.2.ML";
6.6 use "ML-Systems/pp_polyml.ML";
6.7 +use "ML-Systems/pp_dummy.ML";
6.8
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/Pure/ML-Systems/pp_dummy.ML Mon Aug 23 17:46:13 2010 +0200
7.3 @@ -0,0 +1,16 @@
7.4 +(* Title: Pure/ML-Systems/pp_dummy.ML
7.5 +
7.6 +Dummy setup for toplevel pretty printing.
7.7 +*)
7.8 +
7.9 +fun ml_pretty _ = raise Fail "ml_pretty dummy";
7.10 +fun pretty_ml _ = raise Fail "pretty_ml dummy";
7.11 +
7.12 +structure PolyML =
7.13 +struct
7.14 + fun addPrettyPrinter _ = ();
7.15 + fun prettyRepresentation _ =
7.16 + raise Fail "PolyML.prettyRepresentation dummy";
7.17 + open PolyML;
7.18 +end;
7.19 +
8.1 --- a/src/Pure/ML-Systems/smlnj.ML Mon Aug 23 15:30:42 2010 +0200
8.2 +++ b/src/Pure/ML-Systems/smlnj.ML Mon Aug 23 17:46:13 2010 +0200
8.3 @@ -18,6 +18,8 @@
8.4 use "ML-Systems/bash.ML";
8.5 use "ML-Systems/ml_name_space.ML";
8.6 use "ML-Systems/ml_pretty.ML";
8.7 +structure PolyML = struct end;
8.8 +use "ML-Systems/pp_dummy.ML";
8.9 use "ML-Systems/use_context.ML";
8.10
8.11
9.1 --- a/src/Pure/PIDE/command.scala Mon Aug 23 15:30:42 2010 +0200
9.2 +++ b/src/Pure/PIDE/command.scala Mon Aug 23 17:46:13 2010 +0200
9.3 @@ -8,10 +8,6 @@
9.4 package isabelle
9.5
9.6
9.7 -import scala.actors.Actor, Actor._
9.8 -import scala.collection.mutable
9.9 -
9.10 -
9.11 object Command
9.12 {
9.13 /** accumulated results from prover **/
9.14 @@ -40,7 +36,7 @@
9.15
9.16 def accumulate(message: XML.Tree): Command.State =
9.17 message match {
9.18 - case XML.Elem(Markup(Markup.STATUS, _), body) => // FIXME explicit checks!?
9.19 + case XML.Elem(Markup(Markup.STATUS, _), body) => // FIXME explicit body check!?
9.20 copy(status = (for (XML.Elem(markup, _) <- body) yield markup) ::: status)
9.21
9.22 case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
10.1 --- a/src/Pure/ROOT.ML Mon Aug 23 15:30:42 2010 +0200
10.2 +++ b/src/Pure/ROOT.ML Mon Aug 23 17:46:13 2010 +0200
10.3 @@ -179,7 +179,8 @@
10.4 use "ML/ml_syntax.ML";
10.5 use "ML/ml_env.ML";
10.6 use "Isar/runtime.ML";
10.7 -if member (op =) ["polyml-5.2", "polyml-5.2.1", "smlnj-110"] ml_system
10.8 +if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1" orelse
10.9 + String.isPrefix "smlnj" ml_system
10.10 then use "ML/ml_compiler.ML"
10.11 else use "ML/ml_compiler_polyml-5.3.ML";
10.12 use "ML/ml_context.ML";
11.1 --- a/src/Pure/System/isabelle_process.scala Mon Aug 23 15:30:42 2010 +0200
11.2 +++ b/src/Pure/System/isabelle_process.scala Mon Aug 23 17:46:13 2010 +0200
11.3 @@ -155,7 +155,7 @@
11.4 /* raw stdin */
11.5
11.6 private def stdin_actor(name: String, stream: OutputStream): Actor =
11.7 - Library.thread_actor(name) {
11.8 + Simple_Thread.actor(name) {
11.9 val writer = new BufferedWriter(new OutputStreamWriter(stream, Standard_System.charset))
11.10 var finished = false
11.11 while (!finished) {
11.12 @@ -184,7 +184,7 @@
11.13 /* raw stdout */
11.14
11.15 private def stdout_actor(name: String, stream: InputStream): Actor =
11.16 - Library.thread_actor(name) {
11.17 + Simple_Thread.actor(name) {
11.18 val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset))
11.19 var result = new StringBuilder(100)
11.20
11.21 @@ -221,7 +221,7 @@
11.22 /* command input */
11.23
11.24 private def input_actor(name: String, raw_stream: OutputStream): Actor =
11.25 - Library.thread_actor(name) {
11.26 + Simple_Thread.actor(name) {
11.27 val stream = new BufferedOutputStream(raw_stream)
11.28 var finished = false
11.29 while (!finished) {
11.30 @@ -253,7 +253,7 @@
11.31 private class Protocol_Error(msg: String) extends Exception(msg)
11.32
11.33 private def message_actor(name: String, stream: InputStream): Actor =
11.34 - Library.thread_actor(name) {
11.35 + Simple_Thread.actor(name) {
11.36 val default_buffer = new Array[Byte](65536)
11.37 var c = -1
11.38
11.39 @@ -344,7 +344,7 @@
11.40
11.41 /* exit process */
11.42
11.43 - Library.thread_actor("process_exit") {
11.44 + Simple_Thread.actor("process_exit") {
11.45 proc match {
11.46 case None =>
11.47 case Some(p) =>
12.1 --- a/src/Pure/System/session.scala Mon Aug 23 15:30:42 2010 +0200
12.2 +++ b/src/Pure/System/session.scala Mon Aug 23 17:46:13 2010 +0200
12.3 @@ -69,8 +69,8 @@
12.4 private case class Started(timeout: Int, args: List[String])
12.5 private case object Stop
12.6
12.7 - private lazy val session_actor = actor {
12.8 -
12.9 + private val session_actor = Simple_Thread.actor("session_actor", daemon = true)
12.10 + {
12.11 var prover: Isabelle_Process with Isar_Document = null
12.12
12.13
12.14 @@ -199,8 +199,9 @@
12.15
12.16 /* main loop */
12.17
12.18 - loop {
12.19 - react {
12.20 + var finished = false
12.21 + while (!finished) {
12.22 + receive {
12.23 case Started(timeout, args) =>
12.24 if (prover == null) {
12.25 prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
12.26 @@ -211,10 +212,11 @@
12.27 }
12.28 else reply(None)
12.29
12.30 - case Stop => // FIXME clarify; synchronous
12.31 + case Stop => // FIXME synchronous!?
12.32 if (prover != null) {
12.33 prover.kill
12.34 prover = null
12.35 + finished = true
12.36 }
12.37
12.38 case change: Document.Change if prover != null =>
12.39 @@ -235,7 +237,7 @@
12.40
12.41 /** buffered command changes (delay_first discipline) **/
12.42
12.43 - private lazy val command_change_buffer = actor
12.44 + private val command_change_buffer = actor
12.45 //{{{
12.46 {
12.47 import scala.compat.Platform.currentTime
12.48 @@ -286,36 +288,33 @@
12.49
12.50 private case class Edit_Version(edits: List[Document.Node_Text_Edit])
12.51
12.52 - private val editor_history = new Actor
12.53 + @volatile private var history = Document.History.init
12.54 +
12.55 + def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
12.56 + history.snapshot(name, pending_edits, current_state())
12.57 +
12.58 + private val editor_history = actor
12.59 {
12.60 - @volatile private var history = Document.History.init
12.61 + loop {
12.62 + react {
12.63 + case Edit_Version(edits) =>
12.64 + val prev = history.tip.current
12.65 + val result =
12.66 + // FIXME potential denial-of-service concerning worker pool (!?!?)
12.67 + isabelle.Future.fork {
12.68 + val previous = prev.join
12.69 + val former_assignment = current_state().the_assignment(previous).join // FIXME async!?
12.70 + Thy_Syntax.text_edits(Session.this, previous, edits)
12.71 + }
12.72 + val change = new Document.Change(prev, edits, result)
12.73 + history += change
12.74 + change.current.map(_ => session_actor ! change)
12.75 + reply(())
12.76
12.77 - def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
12.78 - history.snapshot(name, pending_edits, current_state())
12.79 -
12.80 - def act
12.81 - {
12.82 - loop {
12.83 - react {
12.84 - case Edit_Version(edits) =>
12.85 - val prev = history.tip.current
12.86 - val result =
12.87 - isabelle.Future.fork {
12.88 - val previous = prev.join
12.89 - val former_assignment = current_state().the_assignment(previous).join // FIXME async!?
12.90 - Thy_Syntax.text_edits(Session.this, previous, edits)
12.91 - }
12.92 - val change = new Document.Change(prev, edits, result)
12.93 - history += change
12.94 - change.current.map(_ => session_actor ! change)
12.95 - reply(())
12.96 -
12.97 - case bad => System.err.println("editor_model: ignoring bad message " + bad)
12.98 - }
12.99 + case bad => System.err.println("editor_model: ignoring bad message " + bad)
12.100 }
12.101 }
12.102 }
12.103 - editor_history.start
12.104
12.105
12.106
12.107 @@ -326,8 +325,5 @@
12.108
12.109 def stop() { session_actor ! Stop }
12.110
12.111 - def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
12.112 - editor_history.snapshot(name, pending_edits)
12.113 -
12.114 def edit_version(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Version(edits) }
12.115 }
13.1 --- a/src/Pure/build-jars Mon Aug 23 15:30:42 2010 +0200
13.2 +++ b/src/Pure/build-jars Mon Aug 23 17:46:13 2010 +0200
13.3 @@ -23,6 +23,7 @@
13.4
13.5 declare -a SOURCES=(
13.6 Concurrent/future.scala
13.7 + Concurrent/simple_thread.scala
13.8 General/exn.scala
13.9 General/linear_set.scala
13.10 General/markup.scala
14.1 --- a/src/Pure/library.scala Mon Aug 23 15:30:42 2010 +0200
14.2 +++ b/src/Pure/library.scala Mon Aug 23 17:46:13 2010 +0200
14.3 @@ -7,11 +7,10 @@
14.4 package isabelle
14.5
14.6
14.7 -import java.lang.{System, Thread}
14.8 +import java.lang.System
14.9 import java.awt.Component
14.10 import javax.swing.JOptionPane
14.11
14.12 -import scala.actors.Actor
14.13 import scala.swing.ComboBox
14.14 import scala.swing.event.SelectionChanged
14.15
14.16 @@ -139,15 +138,4 @@
14.17 ((stop - start).toDouble / 1000000) + "ms elapsed time")
14.18 Exn.release(result)
14.19 }
14.20 -
14.21 -
14.22 - /* thread as actor */
14.23 -
14.24 - def thread_actor(name: String)(body: => Unit): Actor =
14.25 - {
14.26 - val actor = Future.promise[Actor]
14.27 - val thread = new Thread(name) { override def run() = { actor.fulfill(Actor.self); body } }
14.28 - thread.start
14.29 - actor.join
14.30 - }
14.31 }
15.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala Mon Aug 23 15:30:42 2010 +0200
15.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala Mon Aug 23 17:46:13 2010 +0200
15.3 @@ -10,7 +10,6 @@
15.4
15.5 import isabelle._
15.6
15.7 -import scala.actors.Actor, Actor._
15.8 import scala.collection.mutable
15.9
15.10 import org.gjt.sp.jedit.Buffer
15.11 @@ -260,61 +259,63 @@
15.12 // FIXME proper synchronization / thread context (!??)
15.13 val snapshot = Swing_Thread.now { Document_Model.this.snapshot() }
15.14
15.15 - val previous = prev.asInstanceOf[Document_Model.Token_Markup.LineContext]
15.16 - val line = if (prev == null) 0 else previous.line + 1
15.17 - val context = new Document_Model.Token_Markup.LineContext(line, previous)
15.18 + Isabelle.buffer_read_lock(buffer) {
15.19 + val previous = prev.asInstanceOf[Document_Model.Token_Markup.LineContext]
15.20 + val line = if (prev == null) 0 else previous.line + 1
15.21 + val context = new Document_Model.Token_Markup.LineContext(line, previous)
15.22
15.23 - val start = buffer.getLineStartOffset(line)
15.24 - val stop = start + line_segment.count
15.25 - val range = Text.Range(start, stop)
15.26 - val former_range = snapshot.revert(range)
15.27 + val start = buffer.getLineStartOffset(line)
15.28 + val stop = start + line_segment.count
15.29 + val range = Text.Range(start, stop)
15.30 + val former_range = snapshot.revert(range)
15.31
15.32 - /* FIXME
15.33 - for (text_area <- Isabelle.jedit_text_areas(buffer)
15.34 - if Document_View(text_area).isDefined)
15.35 - Document_View(text_area).get.set_styles()
15.36 - */
15.37 + /* FIXME
15.38 + for (text_area <- Isabelle.jedit_text_areas(buffer)
15.39 + if Document_View(text_area).isDefined)
15.40 + Document_View(text_area).get.set_styles()
15.41 + */
15.42
15.43 - def handle_token(style: Byte, offset: Text.Offset, length: Int) =
15.44 - handler.handleToken(line_segment, style, offset, length, context)
15.45 + def handle_token(style: Byte, offset: Text.Offset, length: Int) =
15.46 + handler.handleToken(line_segment, style, offset, length, context)
15.47
15.48 - val syntax = session.current_syntax()
15.49 - val token_markup: PartialFunction[Text.Info[Any], Byte] =
15.50 - {
15.51 - case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
15.52 - if syntax.keyword_kind(name).isDefined =>
15.53 - Document_Model.Token_Markup.command_style(syntax.keyword_kind(name).get)
15.54 + val syntax = session.current_syntax()
15.55 + val token_markup: PartialFunction[Text.Info[Any], Byte] =
15.56 + {
15.57 + case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
15.58 + if syntax.keyword_kind(name).isDefined =>
15.59 + Document_Model.Token_Markup.command_style(syntax.keyword_kind(name).get)
15.60
15.61 - case Text.Info(_, XML.Elem(Markup(name, _), _))
15.62 - if Document_Model.Token_Markup.token_style(name) != Token.NULL =>
15.63 - Document_Model.Token_Markup.token_style(name)
15.64 + case Text.Info(_, XML.Elem(Markup(name, _), _))
15.65 + if Document_Model.Token_Markup.token_style(name) != Token.NULL =>
15.66 + Document_Model.Token_Markup.token_style(name)
15.67 + }
15.68 +
15.69 + var next_x = start
15.70 + for {
15.71 + (command, command_start) <- snapshot.node.command_range(former_range)
15.72 + info <- snapshot.state(command).markup.
15.73 + select((former_range - command_start).restrict(command.range))(token_markup)(Token.NULL)
15.74 + val Text.Range(abs_start, abs_stop) = snapshot.convert(info.range + command_start)
15.75 + if abs_stop > start && abs_start < stop // FIXME abs_range overlaps range (redundant!?)
15.76 + }
15.77 + {
15.78 + val token_start = (abs_start - start) max 0
15.79 + val token_length =
15.80 + (abs_stop - abs_start) -
15.81 + ((start - abs_start) max 0) -
15.82 + ((abs_stop - stop) max 0)
15.83 + if (start + token_start > next_x) // FIXME ??
15.84 + handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x)
15.85 + handle_token(info.info, token_start, token_length)
15.86 + next_x = start + token_start + token_length
15.87 + }
15.88 + if (next_x < stop) // FIXME ??
15.89 + handle_token(Token.COMMENT1, next_x - start, stop - next_x)
15.90 +
15.91 + handle_token(Token.END, line_segment.count, 0)
15.92 + handler.setLineContext(context)
15.93 + context
15.94 }
15.95 -
15.96 - var next_x = start
15.97 - for {
15.98 - (command, command_start) <- snapshot.node.command_range(former_range)
15.99 - info <- snapshot.state(command).markup.
15.100 - select((former_range - command_start).restrict(command.range))(token_markup)(Token.NULL)
15.101 - val Text.Range(abs_start, abs_stop) = snapshot.convert(info.range + command_start)
15.102 - if abs_stop > start && abs_start < stop // FIXME abs_range overlaps range (redundant!?)
15.103 - }
15.104 - {
15.105 - val token_start = (abs_start - start) max 0
15.106 - val token_length =
15.107 - (abs_stop - abs_start) -
15.108 - ((start - abs_start) max 0) -
15.109 - ((abs_stop - stop) max 0)
15.110 - if (start + token_start > next_x) // FIXME ??
15.111 - handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x)
15.112 - handle_token(info.info, token_start, token_length)
15.113 - next_x = start + token_start + token_length
15.114 - }
15.115 - if (next_x < stop) // FIXME ??
15.116 - handle_token(Token.COMMENT1, next_x - start, stop - next_x)
15.117 -
15.118 - handle_token(Token.END, line_segment.count, 0)
15.119 - handler.setLineContext(context)
15.120 - context
15.121 }
15.122 }
15.123
16.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala Mon Aug 23 15:30:42 2010 +0200
16.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Mon Aug 23 17:46:13 2010 +0200
16.3 @@ -106,8 +106,27 @@
16.4 Swing_Thread.now {
16.5 // FIXME cover doc states as well!!?
16.6 val snapshot = model.snapshot()
16.7 - if (changed.exists(snapshot.node.commands.contains))
16.8 - full_repaint(snapshot, changed)
16.9 + val buffer = model.buffer
16.10 + Isabelle.buffer_read_lock(buffer) {
16.11 + if (changed.exists(snapshot.node.commands.contains)) {
16.12 + var visible_change = false
16.13 +
16.14 + for ((command, start) <- snapshot.node.command_starts) {
16.15 + if (changed(command)) {
16.16 + val stop = start + command.length
16.17 + val line1 = buffer.getLineOfOffset(snapshot.convert(start))
16.18 + val line2 = buffer.getLineOfOffset(snapshot.convert(stop))
16.19 + if (line2 >= text_area.getFirstLine &&
16.20 + line1 <= text_area.getFirstLine + text_area.getVisibleLines)
16.21 + visible_change = true
16.22 + text_area.invalidateLineRange(line1, line2)
16.23 + }
16.24 + }
16.25 + if (visible_change) model.buffer.propertiesChanged()
16.26 +
16.27 + overview.repaint() // FIXME paint here!?
16.28 + }
16.29 + }
16.30 }
16.31
16.32 case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
16.33 @@ -115,29 +134,6 @@
16.34 }
16.35 }
16.36
16.37 - def full_repaint(snapshot: Document.Snapshot, changed: Set[Command])
16.38 - {
16.39 - Swing_Thread.require()
16.40 -
16.41 - val buffer = model.buffer
16.42 - var visible_change = false
16.43 -
16.44 - for ((command, start) <- snapshot.node.command_starts) {
16.45 - if (changed(command)) {
16.46 - val stop = start + command.length
16.47 - val line1 = buffer.getLineOfOffset(snapshot.convert(start))
16.48 - val line2 = buffer.getLineOfOffset(snapshot.convert(stop))
16.49 - if (line2 >= text_area.getFirstLine &&
16.50 - line1 <= text_area.getFirstLine + text_area.getVisibleLines)
16.51 - visible_change = true
16.52 - text_area.invalidateLineRange(line1, line2)
16.53 - }
16.54 - }
16.55 - if (visible_change) model.buffer.propertiesChanged()
16.56 -
16.57 - overview.repaint() // FIXME paint here!?
16.58 - }
16.59 -
16.60
16.61 /* text_area_extension */
16.62
16.63 @@ -269,20 +265,23 @@
16.64 override def paintComponent(gfx: Graphics)
16.65 {
16.66 super.paintComponent(gfx)
16.67 + Swing_Thread.assert()
16.68 val buffer = model.buffer
16.69 - val snapshot = model.snapshot()
16.70 - val saved_color = gfx.getColor // FIXME needed!?
16.71 - try {
16.72 - for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
16.73 - val line1 = buffer.getLineOfOffset(snapshot.convert(start))
16.74 - val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
16.75 - val y = line_to_y(line1)
16.76 - val height = HEIGHT * (line2 - line1)
16.77 - gfx.setColor(Document_View.choose_color(snapshot, command))
16.78 - gfx.fillRect(0, y, getWidth - 1, height)
16.79 + Isabelle.buffer_read_lock(buffer) {
16.80 + val snapshot = model.snapshot()
16.81 + val saved_color = gfx.getColor // FIXME needed!?
16.82 + try {
16.83 + for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
16.84 + val line1 = buffer.getLineOfOffset(snapshot.convert(start))
16.85 + val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
16.86 + val y = line_to_y(line1)
16.87 + val height = HEIGHT * (line2 - line1)
16.88 + gfx.setColor(Document_View.choose_color(snapshot, command))
16.89 + gfx.fillRect(0, y, getWidth - 1, height)
16.90 + }
16.91 }
16.92 + finally { gfx.setColor(saved_color) }
16.93 }
16.94 - finally { gfx.setColor(saved_color) }
16.95 }
16.96
16.97 private def line_to_y(line: Int): Int =
17.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Aug 23 15:30:42 2010 +0200
17.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Aug 23 17:46:13 2010 +0200
17.3 @@ -40,6 +40,7 @@
17.4 {
17.5 def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink =
17.6 {
17.7 + // FIXME lock buffer (!??)
17.8 Swing_Thread.assert()
17.9 Document_Model(buffer) match {
17.10 case Some(model) =>
18.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Mon Aug 23 15:30:42 2010 +0200
18.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Mon Aug 23 17:46:13 2010 +0200
18.3 @@ -44,7 +44,7 @@
18.4
18.5 stopped = false
18.6
18.7 - // FIXME lock buffer !??
18.8 + // FIXME lock buffer (!??)
18.9 val data = new SideKickParsedData(buffer.getName)
18.10 val root = data.root
18.11 data.getAsset(root).setEnd(buffer.getLength)
18.12 @@ -66,6 +66,7 @@
18.13
18.14 override def complete(pane: EditPane, caret: Int): SideKickCompletion =
18.15 {
18.16 + // FIXME lock buffer (!?)
18.17 val buffer = pane.getBuffer
18.18
18.19 val line = buffer.getLineOfOffset(caret)
19.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala Mon Aug 23 15:30:42 2010 +0200
19.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala Mon Aug 23 17:46:13 2010 +0200
19.3 @@ -118,6 +118,12 @@
19.4 def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
19.5 jedit_text_areas().filter(_.getBuffer == buffer)
19.6
19.7 + def buffer_read_lock[A](buffer: JEditBuffer)(body: => A): A =
19.8 + {
19.9 + try { buffer.readLock(); body }
19.10 + finally { buffer.readUnlock() }
19.11 + }
19.12 +
19.13
19.14 /* dockable windows */
19.15