--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/simple_thread.scala Mon Aug 23 17:46:13 2010 +0200
@@ -0,0 +1,37 @@
+/* Title: Pure/Concurrent/simple_thread.scala
+ Author: Makarius
+
+Simplified thread operations.
+*/
+
+package isabelle
+
+
+import java.lang.Thread
+
+import scala.actors.Actor
+
+
+object Simple_Thread
+{
+ /* plain thread */
+
+ def fork(name: String, daemon: Boolean = false)(body: => Unit): Thread =
+ {
+ val thread = new Thread(name) { override def run = body }
+ thread.setDaemon(daemon)
+ thread.start
+ thread
+ }
+
+
+ /* thread as actor */
+
+ def actor(name: String, daemon: Boolean = false)(body: => Unit): Actor =
+ {
+ val actor = Future.promise[Actor]
+ val thread = fork(name, daemon) { actor.fulfill(Actor.self); body }
+ actor.join
+ }
+}
+
--- a/src/Pure/General/table.ML Mon Aug 23 15:30:42 2010 +0200
+++ b/src/Pure/General/table.ML Mon Aug 23 17:46:13 2010 +0200
@@ -392,6 +392,16 @@
fun merge_list eq = join (fn _ => Library.merge eq);
+(* ML pretty-printing -- requires Poly/ML 5.3.0 or later *)
+
+val _ =
+ PolyML.addPrettyPrinter (fn depth => fn pretty => fn tab =>
+ ml_pretty
+ (ML_Pretty.enum "," "{" "}"
+ (ML_Pretty.pair (pretty_ml o PolyML.prettyRepresentation) (pretty_ml o pretty))
+ (dest tab, depth)));
+
+
(*final declarations of this structure!*)
fun map f = map_table (K f);
val map' = map_table;
--- a/src/Pure/IsaMakefile Mon Aug 23 15:30:42 2010 +0200
+++ b/src/Pure/IsaMakefile Mon Aug 23 17:46:13 2010 +0200
@@ -32,6 +32,7 @@
ML-Systems/polyml-5.2.ML \
ML-Systems/polyml.ML \
ML-Systems/polyml_common.ML \
+ ML-Systems/pp_dummy.ML \
ML-Systems/pp_polyml.ML \
ML-Systems/proper_int.ML \
ML-Systems/single_assignment.ML \
--- a/src/Pure/ML-Systems/ml_pretty.ML Mon Aug 23 15:30:42 2010 +0200
+++ b/src/Pure/ML-Systems/ml_pretty.ML Mon Aug 23 17:46:13 2010 +0200
@@ -1,7 +1,7 @@
(* Title: Pure/ML-Systems/ml_pretty.ML
Author: Makarius
-Raw datatype for ML pretty printing.
+Minimal support for raw ML pretty printing -- for boot-strapping only.
*)
structure ML_Pretty =
@@ -12,5 +12,20 @@
String of string * int |
Break of bool * int;
+fun block prts = Block (("", ""), prts, 2);
+fun str s = String (s, size s);
+fun brk wd = Break (false, wd);
+
+fun pair pretty1 pretty2 ((x, y), depth: int) =
+ block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
+
+fun enum sep lpar rpar pretty (args, depth) =
+ let
+ fun elems _ [] = []
+ | elems 0 _ = [str "..."]
+ | elems d [x] = [pretty (x, d)]
+ | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
+ in block (str lpar :: (elems (Int.max (depth, 0)) args @ [str rpar])) end;
+
end;
--- a/src/Pure/ML-Systems/polyml-5.2.1.ML Mon Aug 23 15:30:42 2010 +0200
+++ b/src/Pure/ML-Systems/polyml-5.2.1.ML Mon Aug 23 17:46:13 2010 +0200
@@ -25,4 +25,5 @@
use "ML-Systems/compiler_polyml-5.2.ML";
use "ML-Systems/pp_polyml.ML";
+use "ML-Systems/pp_dummy.ML";
--- a/src/Pure/ML-Systems/polyml-5.2.ML Mon Aug 23 15:30:42 2010 +0200
+++ b/src/Pure/ML-Systems/polyml-5.2.ML Mon Aug 23 17:46:13 2010 +0200
@@ -27,4 +27,5 @@
use "ML-Systems/compiler_polyml-5.2.ML";
use "ML-Systems/pp_polyml.ML";
+use "ML-Systems/pp_dummy.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/pp_dummy.ML Mon Aug 23 17:46:13 2010 +0200
@@ -0,0 +1,16 @@
+(* Title: Pure/ML-Systems/pp_dummy.ML
+
+Dummy setup for toplevel pretty printing.
+*)
+
+fun ml_pretty _ = raise Fail "ml_pretty dummy";
+fun pretty_ml _ = raise Fail "pretty_ml dummy";
+
+structure PolyML =
+struct
+ fun addPrettyPrinter _ = ();
+ fun prettyRepresentation _ =
+ raise Fail "PolyML.prettyRepresentation dummy";
+ open PolyML;
+end;
+
--- a/src/Pure/ML-Systems/smlnj.ML Mon Aug 23 15:30:42 2010 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML Mon Aug 23 17:46:13 2010 +0200
@@ -18,6 +18,8 @@
use "ML-Systems/bash.ML";
use "ML-Systems/ml_name_space.ML";
use "ML-Systems/ml_pretty.ML";
+structure PolyML = struct end;
+use "ML-Systems/pp_dummy.ML";
use "ML-Systems/use_context.ML";
--- a/src/Pure/PIDE/command.scala Mon Aug 23 15:30:42 2010 +0200
+++ b/src/Pure/PIDE/command.scala Mon Aug 23 17:46:13 2010 +0200
@@ -8,10 +8,6 @@
package isabelle
-import scala.actors.Actor, Actor._
-import scala.collection.mutable
-
-
object Command
{
/** accumulated results from prover **/
@@ -40,7 +36,7 @@
def accumulate(message: XML.Tree): Command.State =
message match {
- case XML.Elem(Markup(Markup.STATUS, _), body) => // FIXME explicit checks!?
+ case XML.Elem(Markup(Markup.STATUS, _), body) => // FIXME explicit body check!?
copy(status = (for (XML.Elem(markup, _) <- body) yield markup) ::: status)
case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
--- a/src/Pure/ROOT.ML Mon Aug 23 15:30:42 2010 +0200
+++ b/src/Pure/ROOT.ML Mon Aug 23 17:46:13 2010 +0200
@@ -179,7 +179,8 @@
use "ML/ml_syntax.ML";
use "ML/ml_env.ML";
use "Isar/runtime.ML";
-if member (op =) ["polyml-5.2", "polyml-5.2.1", "smlnj-110"] ml_system
+if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1" orelse
+ String.isPrefix "smlnj" ml_system
then use "ML/ml_compiler.ML"
else use "ML/ml_compiler_polyml-5.3.ML";
use "ML/ml_context.ML";
--- a/src/Pure/System/isabelle_process.scala Mon Aug 23 15:30:42 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala Mon Aug 23 17:46:13 2010 +0200
@@ -155,7 +155,7 @@
/* raw stdin */
private def stdin_actor(name: String, stream: OutputStream): Actor =
- Library.thread_actor(name) {
+ Simple_Thread.actor(name) {
val writer = new BufferedWriter(new OutputStreamWriter(stream, Standard_System.charset))
var finished = false
while (!finished) {
@@ -184,7 +184,7 @@
/* raw stdout */
private def stdout_actor(name: String, stream: InputStream): Actor =
- Library.thread_actor(name) {
+ Simple_Thread.actor(name) {
val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset))
var result = new StringBuilder(100)
@@ -221,7 +221,7 @@
/* command input */
private def input_actor(name: String, raw_stream: OutputStream): Actor =
- Library.thread_actor(name) {
+ Simple_Thread.actor(name) {
val stream = new BufferedOutputStream(raw_stream)
var finished = false
while (!finished) {
@@ -253,7 +253,7 @@
private class Protocol_Error(msg: String) extends Exception(msg)
private def message_actor(name: String, stream: InputStream): Actor =
- Library.thread_actor(name) {
+ Simple_Thread.actor(name) {
val default_buffer = new Array[Byte](65536)
var c = -1
@@ -344,7 +344,7 @@
/* exit process */
- Library.thread_actor("process_exit") {
+ Simple_Thread.actor("process_exit") {
proc match {
case None =>
case Some(p) =>
--- a/src/Pure/System/session.scala Mon Aug 23 15:30:42 2010 +0200
+++ b/src/Pure/System/session.scala Mon Aug 23 17:46:13 2010 +0200
@@ -69,8 +69,8 @@
private case class Started(timeout: Int, args: List[String])
private case object Stop
- private lazy val session_actor = actor {
-
+ private val session_actor = Simple_Thread.actor("session_actor", daemon = true)
+ {
var prover: Isabelle_Process with Isar_Document = null
@@ -199,8 +199,9 @@
/* main loop */
- loop {
- react {
+ var finished = false
+ while (!finished) {
+ receive {
case Started(timeout, args) =>
if (prover == null) {
prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
@@ -211,10 +212,11 @@
}
else reply(None)
- case Stop => // FIXME clarify; synchronous
+ case Stop => // FIXME synchronous!?
if (prover != null) {
prover.kill
prover = null
+ finished = true
}
case change: Document.Change if prover != null =>
@@ -235,7 +237,7 @@
/** buffered command changes (delay_first discipline) **/
- private lazy val command_change_buffer = actor
+ private val command_change_buffer = actor
//{{{
{
import scala.compat.Platform.currentTime
@@ -286,36 +288,33 @@
private case class Edit_Version(edits: List[Document.Node_Text_Edit])
- private val editor_history = new Actor
- {
- @volatile private var history = Document.History.init
+ @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())
+ def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
+ history.snapshot(name, pending_edits, current_state())
- def act
- {
- loop {
- react {
- case Edit_Version(edits) =>
- val prev = history.tip.current
- val result =
- 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(())
+ 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)
- }
+ case bad => System.err.println("editor_model: ignoring bad message " + bad)
}
}
}
- editor_history.start
@@ -326,8 +325,5 @@
def stop() { session_actor ! Stop }
- def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
- editor_history.snapshot(name, pending_edits)
-
def edit_version(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Version(edits) }
}
--- a/src/Pure/build-jars Mon Aug 23 15:30:42 2010 +0200
+++ b/src/Pure/build-jars Mon Aug 23 17:46:13 2010 +0200
@@ -23,6 +23,7 @@
declare -a SOURCES=(
Concurrent/future.scala
+ Concurrent/simple_thread.scala
General/exn.scala
General/linear_set.scala
General/markup.scala
--- a/src/Pure/library.scala Mon Aug 23 15:30:42 2010 +0200
+++ b/src/Pure/library.scala Mon Aug 23 17:46:13 2010 +0200
@@ -7,11 +7,10 @@
package isabelle
-import java.lang.{System, Thread}
+import java.lang.System
import java.awt.Component
import javax.swing.JOptionPane
-import scala.actors.Actor
import scala.swing.ComboBox
import scala.swing.event.SelectionChanged
@@ -139,15 +138,4 @@
((stop - start).toDouble / 1000000) + "ms elapsed time")
Exn.release(result)
}
-
-
- /* thread as actor */
-
- def thread_actor(name: String)(body: => Unit): Actor =
- {
- val actor = Future.promise[Actor]
- val thread = new Thread(name) { override def run() = { actor.fulfill(Actor.self); body } }
- thread.start
- actor.join
- }
}
--- a/src/Tools/jEdit/src/jedit/document_model.scala Mon Aug 23 15:30:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Mon Aug 23 17:46:13 2010 +0200
@@ -10,7 +10,6 @@
import isabelle._
-import scala.actors.Actor, Actor._
import scala.collection.mutable
import org.gjt.sp.jedit.Buffer
@@ -260,61 +259,63 @@
// FIXME proper synchronization / thread context (!??)
val snapshot = Swing_Thread.now { Document_Model.this.snapshot() }
- val previous = prev.asInstanceOf[Document_Model.Token_Markup.LineContext]
- val line = if (prev == null) 0 else previous.line + 1
- val context = new Document_Model.Token_Markup.LineContext(line, previous)
+ Isabelle.buffer_read_lock(buffer) {
+ val previous = prev.asInstanceOf[Document_Model.Token_Markup.LineContext]
+ val line = if (prev == null) 0 else previous.line + 1
+ val context = new Document_Model.Token_Markup.LineContext(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)
+ 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)
- if Document_View(text_area).isDefined)
- Document_View(text_area).get.set_styles()
- */
+ /* FIXME
+ for (text_area <- Isabelle.jedit_text_areas(buffer)
+ if Document_View(text_area).isDefined)
+ Document_View(text_area).get.set_styles()
+ */
- def handle_token(style: Byte, offset: Text.Offset, length: Int) =
- handler.handleToken(line_segment, style, offset, length, context)
+ def handle_token(style: Byte, offset: Text.Offset, length: Int) =
+ handler.handleToken(line_segment, style, offset, length, context)
- val syntax = session.current_syntax()
- val token_markup: PartialFunction[Text.Info[Any], Byte] =
- {
- case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
- if syntax.keyword_kind(name).isDefined =>
- Document_Model.Token_Markup.command_style(syntax.keyword_kind(name).get)
+ val syntax = session.current_syntax()
+ val token_markup: PartialFunction[Text.Info[Any], Byte] =
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
+ if syntax.keyword_kind(name).isDefined =>
+ Document_Model.Token_Markup.command_style(syntax.keyword_kind(name).get)
- case Text.Info(_, XML.Elem(Markup(name, _), _))
- if Document_Model.Token_Markup.token_style(name) != Token.NULL =>
- Document_Model.Token_Markup.token_style(name)
- }
+ case Text.Info(_, XML.Elem(Markup(name, _), _))
+ if Document_Model.Token_Markup.token_style(name) != Token.NULL =>
+ 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 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!?)
+ }
+ {
+ 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)
+
+ handle_token(Token.END, line_segment.count, 0)
+ handler.setLineContext(context)
+ context
}
- {
- 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)
-
- handle_token(Token.END, line_segment.count, 0)
- handler.setLineContext(context)
- context
}
}
--- a/src/Tools/jEdit/src/jedit/document_view.scala Mon Aug 23 15:30:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Mon Aug 23 17:46:13 2010 +0200
@@ -106,8 +106,27 @@
Swing_Thread.now {
// FIXME cover doc states as well!!?
val snapshot = model.snapshot()
- if (changed.exists(snapshot.node.commands.contains))
- full_repaint(snapshot, changed)
+ val buffer = model.buffer
+ Isabelle.buffer_read_lock(buffer) {
+ 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)
+ }
+ }
+ if (visible_change) model.buffer.propertiesChanged()
+
+ overview.repaint() // FIXME paint here!?
+ }
+ }
}
case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
@@ -115,29 +134,6 @@
}
}
- def full_repaint(snapshot: Document.Snapshot, changed: Set[Command])
- {
- Swing_Thread.require()
-
- val buffer = model.buffer
- 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)
- }
- }
- if (visible_change) model.buffer.propertiesChanged()
-
- overview.repaint() // FIXME paint here!?
- }
-
/* text_area_extension */
@@ -269,20 +265,23 @@
override def paintComponent(gfx: Graphics)
{
super.paintComponent(gfx)
+ Swing_Thread.assert()
val buffer = model.buffer
- val snapshot = model.snapshot()
- val saved_color = gfx.getColor // FIXME needed!?
- try {
- for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
- val line1 = buffer.getLineOfOffset(snapshot.convert(start))
- val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
- val y = line_to_y(line1)
- val height = HEIGHT * (line2 - line1)
- gfx.setColor(Document_View.choose_color(snapshot, command))
- gfx.fillRect(0, y, getWidth - 1, height)
+ Isabelle.buffer_read_lock(buffer) {
+ val snapshot = model.snapshot()
+ val saved_color = gfx.getColor // FIXME needed!?
+ try {
+ for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
+ val line1 = buffer.getLineOfOffset(snapshot.convert(start))
+ val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
+ val y = line_to_y(line1)
+ val height = HEIGHT * (line2 - line1)
+ gfx.setColor(Document_View.choose_color(snapshot, command))
+ gfx.fillRect(0, y, getWidth - 1, height)
+ }
}
+ finally { gfx.setColor(saved_color) }
}
- finally { gfx.setColor(saved_color) }
}
private def line_to_y(line: Int): Int =
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Aug 23 15:30:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Aug 23 17:46:13 2010 +0200
@@ -40,6 +40,7 @@
{
def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink =
{
+ // FIXME lock buffer (!??)
Swing_Thread.assert()
Document_Model(buffer) match {
case Some(model) =>
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Mon Aug 23 15:30:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Mon Aug 23 17:46:13 2010 +0200
@@ -44,7 +44,7 @@
stopped = false
- // FIXME lock buffer !??
+ // FIXME lock buffer (!??)
val data = new SideKickParsedData(buffer.getName)
val root = data.root
data.getAsset(root).setEnd(buffer.getLength)
@@ -66,6 +66,7 @@
override def complete(pane: EditPane, caret: Int): SideKickCompletion =
{
+ // FIXME lock buffer (!?)
val buffer = pane.getBuffer
val line = buffer.getLineOfOffset(caret)
--- a/src/Tools/jEdit/src/jedit/plugin.scala Mon Aug 23 15:30:42 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Mon Aug 23 17:46:13 2010 +0200
@@ -118,6 +118,12 @@
def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
jedit_text_areas().filter(_.getBuffer == buffer)
+ def buffer_read_lock[A](buffer: JEditBuffer)(body: => A): A =
+ {
+ try { buffer.readLock(); body }
+ finally { buffer.readUnlock() }
+ }
+
/* dockable windows */