merged
authorwenzelm
Sat Apr 26 00:20:53 2014 +0200 (2014-04-26)
changeset 567360f5cf342961c
parent 56727 75f4fdafb285
parent 56735 9923e362789c
child 56737 e4f363e16bdc
merged
     1.1 --- a/etc/options	Fri Apr 25 22:13:17 2014 +0200
     1.2 +++ b/etc/options	Sat Apr 26 00:20:53 2014 +0200
     1.3 @@ -67,7 +67,7 @@
     1.4  
     1.5  public option threads : int = 0
     1.6    -- "maximum number of worker threads for prover process (0 = hardware max.)"
     1.7 -public option threads_trace : int = 0
     1.8 +option threads_trace : int = 0
     1.9    -- "level of tracing information for multithreading"
    1.10  public option parallel_proofs : int = 2
    1.11    -- "level of parallel proof checking: 0, 1, 2"
     2.1 --- a/src/HOL/Record.thy	Fri Apr 25 22:13:17 2014 +0200
     2.2 +++ b/src/HOL/Record.thy	Sat Apr 26 00:20:53 2014 +0200
     2.3 @@ -454,7 +454,7 @@
     2.4  
     2.5  subsection {* Record package *}
     2.6  
     2.7 -ML_file "Tools/record.ML" setup Record.setup
     2.8 +ML_file "Tools/record.ML"
     2.9  
    2.10  hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
    2.11    iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
     3.1 --- a/src/HOL/Tools/record.ML	Fri Apr 25 22:13:17 2014 +0200
     3.2 +++ b/src/HOL/Tools/record.ML	Sat Apr 26 00:20:53 2014 +0200
     3.3 @@ -50,7 +50,6 @@
     3.4    val updateN: string
     3.5    val ext_typeN: string
     3.6    val extN: string
     3.7 -  val setup: theory -> theory
     3.8  end;
     3.9  
    3.10  
    3.11 @@ -734,12 +733,14 @@
    3.12  
    3.13  in
    3.14  
    3.15 -val parse_translation =
    3.16 - [(@{syntax_const "_record_update"}, K record_update_tr),
    3.17 -  (@{syntax_const "_record"}, record_tr),
    3.18 -  (@{syntax_const "_record_scheme"}, record_scheme_tr),
    3.19 -  (@{syntax_const "_record_type"}, record_type_tr),
    3.20 -  (@{syntax_const "_record_type_scheme"}, record_type_scheme_tr)];
    3.21 +val _ =
    3.22 +  Theory.setup
    3.23 +   (Sign.parse_translation
    3.24 +     [(@{syntax_const "_record_update"}, K record_update_tr),
    3.25 +      (@{syntax_const "_record"}, record_tr),
    3.26 +      (@{syntax_const "_record_scheme"}, record_scheme_tr),
    3.27 +      (@{syntax_const "_record_type"}, record_type_tr),
    3.28 +      (@{syntax_const "_record_type_scheme"}, record_type_scheme_tr)]);
    3.29  
    3.30  end;
    3.31  
    3.32 @@ -1430,6 +1431,10 @@
    3.33      else no_tac
    3.34    end);
    3.35  
    3.36 +val _ =
    3.37 +  Theory.setup
    3.38 +    (map_theory_simpset (fn ctxt => ctxt addsimprocs [simproc, upd_simproc, eq_simproc]));
    3.39 +
    3.40  
    3.41  (* wrapper *)
    3.42  
    3.43 @@ -2312,13 +2317,6 @@
    3.44  end;
    3.45  
    3.46  
    3.47 -(* setup theory *)
    3.48 -
    3.49 -val setup =
    3.50 -  Sign.parse_translation parse_translation #>
    3.51 -  map_theory_simpset (fn ctxt => ctxt addsimprocs [simproc, upd_simproc, eq_simproc]);
    3.52 -
    3.53 -
    3.54  (* outer syntax *)
    3.55  
    3.56  val _ =
     4.1 --- a/src/Pure/Concurrent/future.scala	Fri Apr 25 22:13:17 2014 +0200
     4.2 +++ b/src/Pure/Concurrent/future.scala	Sat Apr 26 00:20:53 2014 +0200
     4.3 @@ -10,16 +10,23 @@
     4.4  
     4.5  
     4.6  import scala.util.{Success, Failure}
     4.7 -import scala.concurrent.{Future => Scala_Future, Promise => Scala_Promise, Await}
     4.8 +import scala.concurrent.{ExecutionContext, ExecutionContextExecutor,
     4.9 +  Future => Scala_Future, Promise => Scala_Promise, Await}
    4.10  import scala.concurrent.duration.Duration
    4.11 -import scala.concurrent.ExecutionContext.Implicits.global
    4.12  
    4.13  
    4.14  object Future
    4.15  {
    4.16 +  lazy val execution_context: ExecutionContextExecutor =
    4.17 +    ExecutionContext.fromExecutorService(Simple_Thread.default_pool)
    4.18 +
    4.19    def value[A](x: A): Future[A] = new Finished_Future(x)
    4.20 -  def fork[A](body: => A): Future[A] = new Pending_Future(Scala_Future[A](body))
    4.21 -  def promise[A]: Promise[A] = new Promise_Future[A](Scala_Promise[A])
    4.22 +
    4.23 +  def fork[A](body: => A): Future[A] =
    4.24 +    new Pending_Future(Scala_Future[A](body)(execution_context))
    4.25 +
    4.26 +  def promise[A]: Promise[A] =
    4.27 +    new Promise_Future[A](Scala_Promise[A])
    4.28  }
    4.29  
    4.30  trait Future[A]
    4.31 @@ -62,7 +69,8 @@
    4.32    override def is_finished: Boolean = future.isCompleted
    4.33  
    4.34    def join: A = Await.result(future, Duration.Inf)
    4.35 -  override def map[B](f: A => B): Future[B] = new Pending_Future[B](future.map(f))
    4.36 +  override def map[B](f: A => B): Future[B] =
    4.37 +    new Pending_Future[B](future.map(f)(Future.execution_context))
    4.38  }
    4.39  
    4.40  private class Promise_Future[A](promise: Scala_Promise[A])
     5.1 --- a/src/Pure/Concurrent/simple_thread.scala	Fri Apr 25 22:13:17 2014 +0200
     5.2 +++ b/src/Pure/Concurrent/simple_thread.scala	Sat Apr 26 00:20:53 2014 +0200
     5.3 @@ -9,6 +9,9 @@
     5.4  
     5.5  
     5.6  import java.lang.Thread
     5.7 +import java.util.concurrent.{Callable, Future => JFuture}
     5.8 +
     5.9 +import scala.collection.parallel.ForkJoinTasks
    5.10  
    5.11  
    5.12  object Simple_Thread
    5.13 @@ -40,5 +43,13 @@
    5.14      val thread = fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
    5.15      (thread, result)
    5.16    }
    5.17 +
    5.18 +
    5.19 +  /* thread pool */
    5.20 +
    5.21 +  lazy val default_pool = ForkJoinTasks.defaultForkJoinPool
    5.22 +
    5.23 +  def submit_task[A](body: => A): JFuture[A] =
    5.24 +    default_pool.submit(new Callable[A] { def call = body })
    5.25  }
    5.26  
     6.1 --- a/src/Pure/PIDE/markup.ML	Fri Apr 25 22:13:17 2014 +0200
     6.2 +++ b/src/Pure/PIDE/markup.ML	Sat Apr 26 00:20:53 2014 +0200
     6.3 @@ -172,7 +172,6 @@
     6.4    val padding_command: Properties.entry
     6.5    val dialogN: string val dialog: serial -> string -> T
     6.6    val functionN: string
     6.7 -  val flush: Properties.T
     6.8    val assign_update: Properties.T
     6.9    val removed_versions: Properties.T
    6.10    val protocol_handler: string -> Properties.T
    6.11 @@ -557,8 +556,6 @@
    6.12  
    6.13  val functionN = "function"
    6.14  
    6.15 -val flush = [(functionN, "flush")];
    6.16 -
    6.17  val assign_update = [(functionN, "assign_update")];
    6.18  val removed_versions = [(functionN, "removed_versions")];
    6.19  
     7.1 --- a/src/Pure/PIDE/markup.scala	Fri Apr 25 22:13:17 2014 +0200
     7.2 +++ b/src/Pure/PIDE/markup.scala	Sat Apr 26 00:20:53 2014 +0200
     7.3 @@ -365,8 +365,6 @@
     7.4    val FUNCTION = "function"
     7.5    val Function = new Properties.String(FUNCTION)
     7.6  
     7.7 -  val Flush: Properties.T = List((FUNCTION, "flush"))
     7.8 -
     7.9    val Assign_Update: Properties.T = List((FUNCTION, "assign_update"))
    7.10    val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
    7.11  
     8.1 --- a/src/Pure/PIDE/session.scala	Fri Apr 25 22:13:17 2014 +0200
     8.2 +++ b/src/Pure/PIDE/session.scala	Sat Apr 26 00:20:53 2014 +0200
     8.3 @@ -261,7 +261,6 @@
     8.4    private case object Stop
     8.5    private case class Cancel_Exec(exec_id: Document_ID.Exec)
     8.6    private case class Protocol_Command(name: String, args: List[String])
     8.7 -  private case class Messages(msgs: List[Prover.Message])
     8.8    private case class Update_Options(options: Options)
     8.9  
    8.10  
    8.11 @@ -300,44 +299,6 @@
    8.12    }
    8.13  
    8.14  
    8.15 -  /* buffered prover messages */
    8.16 -
    8.17 -  private object receiver
    8.18 -  {
    8.19 -    private var buffer = new mutable.ListBuffer[Prover.Message]
    8.20 -
    8.21 -    private def flush(): Unit = synchronized {
    8.22 -      if (!buffer.isEmpty) {
    8.23 -        val msgs = buffer.toList
    8.24 -        manager.send(Messages(msgs))
    8.25 -        buffer = new mutable.ListBuffer[Prover.Message]
    8.26 -      }
    8.27 -    }
    8.28 -
    8.29 -    def invoke(msg: Prover.Message): Unit = synchronized {
    8.30 -      msg match {
    8.31 -        case _: Prover.Input =>
    8.32 -          buffer += msg
    8.33 -        case output: Prover.Protocol_Output if output.properties == Markup.Flush =>
    8.34 -          flush()
    8.35 -        case output: Prover.Output =>
    8.36 -          buffer += msg
    8.37 -          if (output.is_syslog)
    8.38 -            syslog.change(queue =>
    8.39 -              {
    8.40 -                val queue1 = queue.enqueue(output.message)
    8.41 -                if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
    8.42 -              })
    8.43 -      }
    8.44 -    }
    8.45 -
    8.46 -    private val timer = new Timer("receiver", true)
    8.47 -    timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms)
    8.48 -
    8.49 -    def shutdown() { timer.cancel(); flush() }
    8.50 -  }
    8.51 -
    8.52 -
    8.53    /* postponed changes */
    8.54  
    8.55    private object postponed_changes
    8.56 @@ -503,9 +464,9 @@
    8.57                phase = Session.Ready
    8.58  
    8.59              case Markup.Return_Code(rc) if output.is_exit =>
    8.60 -              prover = None
    8.61                if (rc == 0) phase = Session.Inactive
    8.62                else phase = Session.Failed
    8.63 +              prover = None
    8.64  
    8.65              case _ => raw_output_messages.post(output)
    8.66            }
    8.67 @@ -521,10 +482,26 @@
    8.68        case arg: Any =>
    8.69          //{{{
    8.70          arg match {
    8.71 +          case output: Prover.Output =>
    8.72 +            if (output.is_stdout || output.is_stderr) raw_output_messages.post(output)
    8.73 +            else handle_output(output)
    8.74 +            if (output.is_syslog) {
    8.75 +              syslog.change(queue =>
    8.76 +                {
    8.77 +                  val queue1 = queue.enqueue(output.message)
    8.78 +                  if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
    8.79 +                })
    8.80 +              syslog_messages.post(output)
    8.81 +            }
    8.82 +            all_messages.post(output)
    8.83 +
    8.84 +          case input: Prover.Input =>
    8.85 +            all_messages.post(input)
    8.86 +
    8.87            case Start(name, args) if prover.isEmpty =>
    8.88              if (phase == Session.Inactive || phase == Session.Failed) {
    8.89                phase = Session.Startup
    8.90 -              prover = Some(resources.start_prover(receiver.invoke _, name, args))
    8.91 +              prover = Some(resources.start_prover(manager.send(_), name, args))
    8.92              }
    8.93  
    8.94            case Stop =>
    8.95 @@ -555,18 +532,6 @@
    8.96            case Protocol_Command(name, args) if prover.isDefined =>
    8.97              prover.get.protocol_command(name, args:_*)
    8.98  
    8.99 -          case Messages(msgs) =>
   8.100 -            msgs foreach {
   8.101 -              case input: Prover.Input =>
   8.102 -                all_messages.post(input)
   8.103 -
   8.104 -              case output: Prover.Output =>
   8.105 -                if (output.is_stdout || output.is_stderr) raw_output_messages.post(output)
   8.106 -                else handle_output(output)
   8.107 -                if (output.is_syslog) syslog_messages.post(output)
   8.108 -                all_messages.post(output)
   8.109 -            }
   8.110 -
   8.111            case change: Session.Change if prover.isDefined =>
   8.112              if (global_state.value.is_assigned(change.previous))
   8.113                handle_change(change)
   8.114 @@ -586,7 +551,6 @@
   8.115    def stop()
   8.116    {
   8.117      manager.send_wait(Stop)
   8.118 -    receiver.shutdown()
   8.119      change_parser.shutdown()
   8.120      change_buffer.shutdown()
   8.121      manager.shutdown()
     9.1 --- a/src/Pure/System/invoke_scala.scala	Fri Apr 25 22:13:17 2014 +0200
     9.2 +++ b/src/Pure/System/invoke_scala.scala	Sat Apr 26 00:20:53 2014 +0200
     9.3 @@ -8,6 +8,8 @@
     9.4  
     9.5  
     9.6  import java.lang.reflect.{Method, Modifier, InvocationTargetException}
     9.7 +import java.util.concurrent.{Future => JFuture}
     9.8 +
     9.9  import scala.util.matching.Regex
    9.10  
    9.11  
    9.12 @@ -70,7 +72,7 @@
    9.13  
    9.14  class Invoke_Scala extends Session.Protocol_Handler
    9.15  {
    9.16 -  private var futures = Map.empty[String, java.util.concurrent.Future[Unit]]
    9.17 +  private var futures = Map.empty[String, JFuture[Unit]]
    9.18  
    9.19    private def fulfill(prover: Prover, id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit =
    9.20      synchronized
    9.21 @@ -81,7 +83,7 @@
    9.22        }
    9.23      }
    9.24  
    9.25 -  private def cancel(prover: Prover, id: String, future: java.util.concurrent.Future[Unit])
    9.26 +  private def cancel(prover: Prover, id: String, future: JFuture[Unit])
    9.27    {
    9.28      future.cancel(true)
    9.29      fulfill(prover, id, Invoke_Scala.Tag.INTERRUPT, "")
    9.30 @@ -92,11 +94,10 @@
    9.31      msg.properties match {
    9.32        case Markup.Invoke_Scala(name, id) =>
    9.33          futures += (id ->
    9.34 -          default_thread_pool.submit(() =>
    9.35 -            {
    9.36 -              val (tag, result) = Invoke_Scala.method(name, msg.text)
    9.37 -              fulfill(prover, id, tag, result)
    9.38 -            }))
    9.39 +          Simple_Thread.submit_task {
    9.40 +            val (tag, result) = Invoke_Scala.method(name, msg.text)
    9.41 +            fulfill(prover, id, tag, result)
    9.42 +          })
    9.43          true
    9.44        case _ => false
    9.45      }
    10.1 --- a/src/Pure/System/message_channel.ML	Fri Apr 25 22:13:17 2014 +0200
    10.2 +++ b/src/Pure/System/message_channel.ML	Sat Apr 26 00:20:53 2014 +0200
    10.3 @@ -34,14 +34,6 @@
    10.4    List.app (System_Channel.output channel) ss;
    10.5  
    10.6  
    10.7 -(* flush *)
    10.8 -
    10.9 -fun flush channel = ignore (try System_Channel.flush channel);
   10.10 -
   10.11 -val flush_message = message Markup.protocolN Markup.flush [];
   10.12 -fun flush_output channel = (output_message channel flush_message; flush channel);
   10.13 -
   10.14 -
   10.15  (* channel *)
   10.16  
   10.17  datatype T = Message_Channel of {send: message -> unit, shutdown: unit -> unit};
   10.18 @@ -49,15 +41,17 @@
   10.19  fun send (Message_Channel {send, ...}) = send;
   10.20  fun shutdown (Message_Channel {shutdown, ...}) = shutdown ();
   10.21  
   10.22 +fun flush channel = ignore (try System_Channel.flush channel);
   10.23 +
   10.24  fun message_output mbox channel =
   10.25    let
   10.26      fun loop receive =
   10.27        (case receive mbox of
   10.28 -        SOME NONE => flush_output channel
   10.29 +        SOME NONE => flush channel
   10.30        | SOME (SOME msg) =>
   10.31           (output_message channel msg;
   10.32            loop (Mailbox.receive_timeout (seconds 0.02)))
   10.33 -      | NONE => (flush_output channel; loop (SOME o Mailbox.receive)));
   10.34 +      | NONE => (flush channel; loop (SOME o Mailbox.receive)));
   10.35    in fn () => loop (SOME o Mailbox.receive) end;
   10.36  
   10.37  fun make channel =
    11.1 --- a/src/Pure/Thy/thy_info.scala	Fri Apr 25 22:13:17 2014 +0200
    11.2 +++ b/src/Pure/Thy/thy_info.scala	Sat Apr 26 00:20:53 2014 +0200
    11.3 @@ -7,9 +7,6 @@
    11.4  package isabelle
    11.5  
    11.6  
    11.7 -import java.util.concurrent.{Future => JFuture}
    11.8 -
    11.9 -
   11.10  class Thy_Info(resources: Resources)
   11.11  {
   11.12    /* messages */
    12.1 --- a/src/Pure/library.scala	Fri Apr 25 22:13:17 2014 +0200
    12.2 +++ b/src/Pure/library.scala	Sat Apr 26 00:20:53 2014 +0200
    12.3 @@ -10,8 +10,6 @@
    12.4  
    12.5  import scala.collection.mutable
    12.6  
    12.7 -import java.util.concurrent.{Future => JFuture, TimeUnit}
    12.8 -
    12.9  
   12.10  object Library
   12.11  {
   12.12 @@ -159,18 +157,6 @@
   12.13    def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs
   12.14    def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs
   12.15    def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
   12.16 -
   12.17 -
   12.18 -  /* Java futures */
   12.19 -
   12.20 -  def future_value[A](x: A) = new JFuture[A]
   12.21 -  {
   12.22 -    def cancel(may_interrupt: Boolean): Boolean = false
   12.23 -    def isCancelled(): Boolean = false
   12.24 -    def isDone(): Boolean = true
   12.25 -    def get(): A = x
   12.26 -    def get(timeout: Long, time_unit: TimeUnit): A = x
   12.27 -  }
   12.28  }
   12.29  
   12.30  
   12.31 @@ -186,13 +172,4 @@
   12.32    val quote = Library.quote _
   12.33    val commas = Library.commas _
   12.34    val commas_quote = Library.commas_quote _
   12.35 -
   12.36 -
   12.37 -  /* parallel tasks */
   12.38 -
   12.39 -  implicit def function_as_callable[A](f: () => A) =
   12.40 -    new java.util.concurrent.Callable[A] { def call = f() }
   12.41 -
   12.42 -  val default_thread_pool =
   12.43 -    scala.collection.parallel.ForkJoinTasks.defaultForkJoinPool
   12.44  }
    13.1 --- a/src/Tools/jEdit/etc/settings	Fri Apr 25 22:13:17 2014 +0200
    13.2 +++ b/src/Tools/jEdit/etc/settings	Sat Apr 26 00:20:53 2014 +0200
    13.3 @@ -4,9 +4,9 @@
    13.4  JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit"
    13.5  
    13.6  JEDIT_OPTIONS="-reuseview -noserver -nobackground -log=9"
    13.7 -#JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss1m -Dscala.concurrent.context.minThreads=1 -Dscala.concurrent.context.numThreads=x0.5 -Dscala.concurrent.context.maxThreads=8"
    13.8 -JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss2m -Dscala.concurrent.context.minThreads=1 -Dscala.concurrent.context.numThreads=x0.5 -Dscala.concurrent.context.maxThreads=8"
    13.9 -#JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4096m -Xss8m -Dscala.concurrent.context.minThreads=1 -Dscala.concurrent.context.numThreads=x0.5 -Dscala.concurrent.context.maxThreads=8"
   13.10 +#JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss1m"
   13.11 +JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss2m"
   13.12 +#JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4096m -Xss8m"
   13.13  JEDIT_SYSTEM_OPTIONS="-Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle -Dscala.repl.no-threads=true"
   13.14  
   13.15  ISABELLE_JEDIT_OPTIONS=""
    14.1 --- a/src/Tools/jEdit/src/active.scala	Fri Apr 25 22:13:17 2014 +0200
    14.2 +++ b/src/Tools/jEdit/src/active.scala	Sat Apr 26 00:20:53 2014 +0200
    14.3 @@ -30,25 +30,23 @@
    14.4              // FIXME avoid hard-wired stuff
    14.5              elem match {
    14.6                case XML.Elem(Markup(Markup.BROWSER, _), body) =>
    14.7 -                default_thread_pool.submit(() =>
    14.8 -                  {
    14.9 -                    val graph_file = Isabelle_System.tmp_file("graph")
   14.10 -                    File.write(graph_file, XML.content(body))
   14.11 -                    Isabelle_System.bash_env(null,
   14.12 -                      Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)),
   14.13 -                      "\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &")
   14.14 -                  })
   14.15 +                Future.fork {
   14.16 +                  val graph_file = Isabelle_System.tmp_file("graph")
   14.17 +                  File.write(graph_file, XML.content(body))
   14.18 +                  Isabelle_System.bash_env(null,
   14.19 +                    Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)),
   14.20 +                    "\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &")
   14.21 +                }
   14.22  
   14.23                case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
   14.24 -                default_thread_pool.submit(() =>
   14.25 -                  {
   14.26 -                    val graph =
   14.27 -                      Exn.capture {
   14.28 -                        isabelle.graphview.Model.decode_graph(body)
   14.29 -                          .transitive_reduction_acyclic
   14.30 -                      }
   14.31 -                    Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
   14.32 -                  })
   14.33 +                Future.fork {
   14.34 +                  val graph =
   14.35 +                    Exn.capture {
   14.36 +                      isabelle.graphview.Model.decode_graph(body)
   14.37 +                        .transitive_reduction_acyclic
   14.38 +                    }
   14.39 +                  Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
   14.40 +                }
   14.41  
   14.42                case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
   14.43                  props match {
    15.1 --- a/src/Tools/jEdit/src/documentation_dockable.scala	Fri Apr 25 22:13:17 2014 +0200
    15.2 +++ b/src/Tools/jEdit/src/documentation_dockable.scala	Sat Apr 26 00:20:53 2014 +0200
    15.3 @@ -68,13 +68,14 @@
    15.4                  if (path.is_file)
    15.5                    PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
    15.6                  else {
    15.7 -                  default_thread_pool.submit(() =>
    15.8 +                  Future.fork {
    15.9                      try { Doc.view(path) }
   15.10                      catch {
   15.11                        case exn: Throwable =>
   15.12                          GUI.error_dialog(view,
   15.13                            "Documentation error", GUI.scrollable_text(Exn.message(exn)))
   15.14 -                    })
   15.15 +                    }
   15.16 +                  }
   15.17                  }
   15.18                case _ =>
   15.19              }
    16.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Apr 25 22:13:17 2014 +0200
    16.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Sat Apr 26 00:20:53 2014 +0200
    16.3 @@ -162,20 +162,21 @@
    16.4    def hyperlink_url(name: String): Hyperlink =
    16.5      new Hyperlink {
    16.6        val external = true
    16.7 -      def follow(view: View) =
    16.8 -        default_thread_pool.submit(() =>
    16.9 +      def follow(view: View): Unit =
   16.10 +        Future.fork {
   16.11            try { Isabelle_System.open(name) }
   16.12            catch {
   16.13              case exn: Throwable =>
   16.14                GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
   16.15 -          })
   16.16 +          }
   16.17 +        }
   16.18        override def toString: String = "URL " + quote(name)
   16.19      }
   16.20  
   16.21    def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
   16.22      new Hyperlink {
   16.23        val external = false
   16.24 -      def follow(view: View) = goto_file(view, name, line, column)
   16.25 +      def follow(view: View): Unit = goto_file(view, name, line, column)
   16.26        override def toString: String = "file " + quote(name)
   16.27      }
   16.28  
    17.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Apr 25 22:13:17 2014 +0200
    17.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sat Apr 26 00:20:53 2014 +0200
    17.3 @@ -12,6 +12,7 @@
    17.4  
    17.5  import java.awt.{Color, Font, FontMetrics, Toolkit, Window}
    17.6  import java.awt.event.KeyEvent
    17.7 +import java.util.concurrent.{Future => JFuture}
    17.8  
    17.9  import org.gjt.sp.jedit.{jEdit, View, Registers}
   17.10  import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea}
   17.11 @@ -67,7 +68,7 @@
   17.12    private var current_base_results = Command.Results.empty
   17.13    private var current_rendering: Rendering =
   17.14      Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2
   17.15 -  private var future_rendering: Option[java.util.concurrent.Future[Unit]] = None
   17.16 +  private var future_rendering: Option[JFuture[Unit]] = None
   17.17  
   17.18    private val rich_text_area =
   17.19      new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
   17.20 @@ -118,8 +119,8 @@
   17.21        val formatted_body = Pretty.formatted(current_body, margin, metric)
   17.22  
   17.23        future_rendering.map(_.cancel(true))
   17.24 -      future_rendering = Some(default_thread_pool.submit(() =>
   17.25 -        {
   17.26 +      future_rendering =
   17.27 +        Some(Simple_Thread.submit_task {
   17.28            val (text, rendering) =
   17.29              try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) }
   17.30              catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
   17.31 @@ -136,7 +137,7 @@
   17.32                getBuffer.setReadOnly(true)
   17.33              }
   17.34            }
   17.35 -        }))
   17.36 +        })
   17.37      }
   17.38    }
   17.39