--- a/etc/options Fri Apr 25 22:13:17 2014 +0200
+++ b/etc/options Sat Apr 26 00:20:53 2014 +0200
@@ -67,7 +67,7 @@
public option threads : int = 0
-- "maximum number of worker threads for prover process (0 = hardware max.)"
-public option threads_trace : int = 0
+option threads_trace : int = 0
-- "level of tracing information for multithreading"
public option parallel_proofs : int = 2
-- "level of parallel proof checking: 0, 1, 2"
--- a/src/HOL/Record.thy Fri Apr 25 22:13:17 2014 +0200
+++ b/src/HOL/Record.thy Sat Apr 26 00:20:53 2014 +0200
@@ -454,7 +454,7 @@
subsection {* Record package *}
-ML_file "Tools/record.ML" setup Record.setup
+ML_file "Tools/record.ML"
hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
--- a/src/HOL/Tools/record.ML Fri Apr 25 22:13:17 2014 +0200
+++ b/src/HOL/Tools/record.ML Sat Apr 26 00:20:53 2014 +0200
@@ -50,7 +50,6 @@
val updateN: string
val ext_typeN: string
val extN: string
- val setup: theory -> theory
end;
@@ -734,12 +733,14 @@
in
-val parse_translation =
- [(@{syntax_const "_record_update"}, K record_update_tr),
- (@{syntax_const "_record"}, record_tr),
- (@{syntax_const "_record_scheme"}, record_scheme_tr),
- (@{syntax_const "_record_type"}, record_type_tr),
- (@{syntax_const "_record_type_scheme"}, record_type_scheme_tr)];
+val _ =
+ Theory.setup
+ (Sign.parse_translation
+ [(@{syntax_const "_record_update"}, K record_update_tr),
+ (@{syntax_const "_record"}, record_tr),
+ (@{syntax_const "_record_scheme"}, record_scheme_tr),
+ (@{syntax_const "_record_type"}, record_type_tr),
+ (@{syntax_const "_record_type_scheme"}, record_type_scheme_tr)]);
end;
@@ -1430,6 +1431,10 @@
else no_tac
end);
+val _ =
+ Theory.setup
+ (map_theory_simpset (fn ctxt => ctxt addsimprocs [simproc, upd_simproc, eq_simproc]));
+
(* wrapper *)
@@ -2312,13 +2317,6 @@
end;
-(* setup theory *)
-
-val setup =
- Sign.parse_translation parse_translation #>
- map_theory_simpset (fn ctxt => ctxt addsimprocs [simproc, upd_simproc, eq_simproc]);
-
-
(* outer syntax *)
val _ =
--- a/src/Pure/Concurrent/future.scala Fri Apr 25 22:13:17 2014 +0200
+++ b/src/Pure/Concurrent/future.scala Sat Apr 26 00:20:53 2014 +0200
@@ -10,16 +10,23 @@
import scala.util.{Success, Failure}
-import scala.concurrent.{Future => Scala_Future, Promise => Scala_Promise, Await}
+import scala.concurrent.{ExecutionContext, ExecutionContextExecutor,
+ Future => Scala_Future, Promise => Scala_Promise, Await}
import scala.concurrent.duration.Duration
-import scala.concurrent.ExecutionContext.Implicits.global
object Future
{
+ lazy val execution_context: ExecutionContextExecutor =
+ ExecutionContext.fromExecutorService(Simple_Thread.default_pool)
+
def value[A](x: A): Future[A] = new Finished_Future(x)
- def fork[A](body: => A): Future[A] = new Pending_Future(Scala_Future[A](body))
- def promise[A]: Promise[A] = new Promise_Future[A](Scala_Promise[A])
+
+ def fork[A](body: => A): Future[A] =
+ new Pending_Future(Scala_Future[A](body)(execution_context))
+
+ def promise[A]: Promise[A] =
+ new Promise_Future[A](Scala_Promise[A])
}
trait Future[A]
@@ -62,7 +69,8 @@
override def is_finished: Boolean = future.isCompleted
def join: A = Await.result(future, Duration.Inf)
- override def map[B](f: A => B): Future[B] = new Pending_Future[B](future.map(f))
+ override def map[B](f: A => B): Future[B] =
+ new Pending_Future[B](future.map(f)(Future.execution_context))
}
private class Promise_Future[A](promise: Scala_Promise[A])
--- a/src/Pure/Concurrent/simple_thread.scala Fri Apr 25 22:13:17 2014 +0200
+++ b/src/Pure/Concurrent/simple_thread.scala Sat Apr 26 00:20:53 2014 +0200
@@ -9,6 +9,9 @@
import java.lang.Thread
+import java.util.concurrent.{Callable, Future => JFuture}
+
+import scala.collection.parallel.ForkJoinTasks
object Simple_Thread
@@ -40,5 +43,13 @@
val thread = fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
(thread, result)
}
+
+
+ /* thread pool */
+
+ lazy val default_pool = ForkJoinTasks.defaultForkJoinPool
+
+ def submit_task[A](body: => A): JFuture[A] =
+ default_pool.submit(new Callable[A] { def call = body })
}
--- a/src/Pure/PIDE/markup.ML Fri Apr 25 22:13:17 2014 +0200
+++ b/src/Pure/PIDE/markup.ML Sat Apr 26 00:20:53 2014 +0200
@@ -172,7 +172,6 @@
val padding_command: Properties.entry
val dialogN: string val dialog: serial -> string -> T
val functionN: string
- val flush: Properties.T
val assign_update: Properties.T
val removed_versions: Properties.T
val protocol_handler: string -> Properties.T
@@ -557,8 +556,6 @@
val functionN = "function"
-val flush = [(functionN, "flush")];
-
val assign_update = [(functionN, "assign_update")];
val removed_versions = [(functionN, "removed_versions")];
--- a/src/Pure/PIDE/markup.scala Fri Apr 25 22:13:17 2014 +0200
+++ b/src/Pure/PIDE/markup.scala Sat Apr 26 00:20:53 2014 +0200
@@ -365,8 +365,6 @@
val FUNCTION = "function"
val Function = new Properties.String(FUNCTION)
- val Flush: Properties.T = List((FUNCTION, "flush"))
-
val Assign_Update: Properties.T = List((FUNCTION, "assign_update"))
val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
--- a/src/Pure/PIDE/session.scala Fri Apr 25 22:13:17 2014 +0200
+++ b/src/Pure/PIDE/session.scala Sat Apr 26 00:20:53 2014 +0200
@@ -261,7 +261,6 @@
private case object Stop
private case class Cancel_Exec(exec_id: Document_ID.Exec)
private case class Protocol_Command(name: String, args: List[String])
- private case class Messages(msgs: List[Prover.Message])
private case class Update_Options(options: Options)
@@ -300,44 +299,6 @@
}
- /* buffered prover messages */
-
- private object receiver
- {
- private var buffer = new mutable.ListBuffer[Prover.Message]
-
- private def flush(): Unit = synchronized {
- if (!buffer.isEmpty) {
- val msgs = buffer.toList
- manager.send(Messages(msgs))
- buffer = new mutable.ListBuffer[Prover.Message]
- }
- }
-
- def invoke(msg: Prover.Message): Unit = synchronized {
- msg match {
- case _: Prover.Input =>
- buffer += msg
- case output: Prover.Protocol_Output if output.properties == Markup.Flush =>
- flush()
- case output: Prover.Output =>
- buffer += msg
- if (output.is_syslog)
- syslog.change(queue =>
- {
- val queue1 = queue.enqueue(output.message)
- if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
- })
- }
- }
-
- private val timer = new Timer("receiver", true)
- timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms)
-
- def shutdown() { timer.cancel(); flush() }
- }
-
-
/* postponed changes */
private object postponed_changes
@@ -503,9 +464,9 @@
phase = Session.Ready
case Markup.Return_Code(rc) if output.is_exit =>
- prover = None
if (rc == 0) phase = Session.Inactive
else phase = Session.Failed
+ prover = None
case _ => raw_output_messages.post(output)
}
@@ -521,10 +482,26 @@
case arg: Any =>
//{{{
arg match {
+ case output: Prover.Output =>
+ if (output.is_stdout || output.is_stderr) raw_output_messages.post(output)
+ else handle_output(output)
+ if (output.is_syslog) {
+ syslog.change(queue =>
+ {
+ val queue1 = queue.enqueue(output.message)
+ if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1
+ })
+ syslog_messages.post(output)
+ }
+ all_messages.post(output)
+
+ case input: Prover.Input =>
+ all_messages.post(input)
+
case Start(name, args) if prover.isEmpty =>
if (phase == Session.Inactive || phase == Session.Failed) {
phase = Session.Startup
- prover = Some(resources.start_prover(receiver.invoke _, name, args))
+ prover = Some(resources.start_prover(manager.send(_), name, args))
}
case Stop =>
@@ -555,18 +532,6 @@
case Protocol_Command(name, args) if prover.isDefined =>
prover.get.protocol_command(name, args:_*)
- case Messages(msgs) =>
- msgs foreach {
- case input: Prover.Input =>
- all_messages.post(input)
-
- case output: Prover.Output =>
- if (output.is_stdout || output.is_stderr) raw_output_messages.post(output)
- else handle_output(output)
- if (output.is_syslog) syslog_messages.post(output)
- all_messages.post(output)
- }
-
case change: Session.Change if prover.isDefined =>
if (global_state.value.is_assigned(change.previous))
handle_change(change)
@@ -586,7 +551,6 @@
def stop()
{
manager.send_wait(Stop)
- receiver.shutdown()
change_parser.shutdown()
change_buffer.shutdown()
manager.shutdown()
--- a/src/Pure/System/invoke_scala.scala Fri Apr 25 22:13:17 2014 +0200
+++ b/src/Pure/System/invoke_scala.scala Sat Apr 26 00:20:53 2014 +0200
@@ -8,6 +8,8 @@
import java.lang.reflect.{Method, Modifier, InvocationTargetException}
+import java.util.concurrent.{Future => JFuture}
+
import scala.util.matching.Regex
@@ -70,7 +72,7 @@
class Invoke_Scala extends Session.Protocol_Handler
{
- private var futures = Map.empty[String, java.util.concurrent.Future[Unit]]
+ private var futures = Map.empty[String, JFuture[Unit]]
private def fulfill(prover: Prover, id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit =
synchronized
@@ -81,7 +83,7 @@
}
}
- private def cancel(prover: Prover, id: String, future: java.util.concurrent.Future[Unit])
+ private def cancel(prover: Prover, id: String, future: JFuture[Unit])
{
future.cancel(true)
fulfill(prover, id, Invoke_Scala.Tag.INTERRUPT, "")
@@ -92,11 +94,10 @@
msg.properties match {
case Markup.Invoke_Scala(name, id) =>
futures += (id ->
- default_thread_pool.submit(() =>
- {
- val (tag, result) = Invoke_Scala.method(name, msg.text)
- fulfill(prover, id, tag, result)
- }))
+ Simple_Thread.submit_task {
+ val (tag, result) = Invoke_Scala.method(name, msg.text)
+ fulfill(prover, id, tag, result)
+ })
true
case _ => false
}
--- a/src/Pure/System/message_channel.ML Fri Apr 25 22:13:17 2014 +0200
+++ b/src/Pure/System/message_channel.ML Sat Apr 26 00:20:53 2014 +0200
@@ -34,14 +34,6 @@
List.app (System_Channel.output channel) ss;
-(* flush *)
-
-fun flush channel = ignore (try System_Channel.flush channel);
-
-val flush_message = message Markup.protocolN Markup.flush [];
-fun flush_output channel = (output_message channel flush_message; flush channel);
-
-
(* channel *)
datatype T = Message_Channel of {send: message -> unit, shutdown: unit -> unit};
@@ -49,15 +41,17 @@
fun send (Message_Channel {send, ...}) = send;
fun shutdown (Message_Channel {shutdown, ...}) = shutdown ();
+fun flush channel = ignore (try System_Channel.flush channel);
+
fun message_output mbox channel =
let
fun loop receive =
(case receive mbox of
- SOME NONE => flush_output channel
+ SOME NONE => flush channel
| SOME (SOME msg) =>
(output_message channel msg;
loop (Mailbox.receive_timeout (seconds 0.02)))
- | NONE => (flush_output channel; loop (SOME o Mailbox.receive)));
+ | NONE => (flush channel; loop (SOME o Mailbox.receive)));
in fn () => loop (SOME o Mailbox.receive) end;
fun make channel =
--- a/src/Pure/Thy/thy_info.scala Fri Apr 25 22:13:17 2014 +0200
+++ b/src/Pure/Thy/thy_info.scala Sat Apr 26 00:20:53 2014 +0200
@@ -7,9 +7,6 @@
package isabelle
-import java.util.concurrent.{Future => JFuture}
-
-
class Thy_Info(resources: Resources)
{
/* messages */
--- a/src/Pure/library.scala Fri Apr 25 22:13:17 2014 +0200
+++ b/src/Pure/library.scala Sat Apr 26 00:20:53 2014 +0200
@@ -10,8 +10,6 @@
import scala.collection.mutable
-import java.util.concurrent.{Future => JFuture, TimeUnit}
-
object Library
{
@@ -159,18 +157,6 @@
def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs
def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs
def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
-
-
- /* Java futures */
-
- def future_value[A](x: A) = new JFuture[A]
- {
- def cancel(may_interrupt: Boolean): Boolean = false
- def isCancelled(): Boolean = false
- def isDone(): Boolean = true
- def get(): A = x
- def get(timeout: Long, time_unit: TimeUnit): A = x
- }
}
@@ -186,13 +172,4 @@
val quote = Library.quote _
val commas = Library.commas _
val commas_quote = Library.commas_quote _
-
-
- /* parallel tasks */
-
- implicit def function_as_callable[A](f: () => A) =
- new java.util.concurrent.Callable[A] { def call = f() }
-
- val default_thread_pool =
- scala.collection.parallel.ForkJoinTasks.defaultForkJoinPool
}
--- a/src/Tools/jEdit/etc/settings Fri Apr 25 22:13:17 2014 +0200
+++ b/src/Tools/jEdit/etc/settings Sat Apr 26 00:20:53 2014 +0200
@@ -4,9 +4,9 @@
JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit"
JEDIT_OPTIONS="-reuseview -noserver -nobackground -log=9"
-#JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss1m -Dscala.concurrent.context.minThreads=1 -Dscala.concurrent.context.numThreads=x0.5 -Dscala.concurrent.context.maxThreads=8"
-JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss2m -Dscala.concurrent.context.minThreads=1 -Dscala.concurrent.context.numThreads=x0.5 -Dscala.concurrent.context.maxThreads=8"
-#JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4096m -Xss8m -Dscala.concurrent.context.minThreads=1 -Dscala.concurrent.context.numThreads=x0.5 -Dscala.concurrent.context.maxThreads=8"
+#JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss1m"
+JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss2m"
+#JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4096m -Xss8m"
JEDIT_SYSTEM_OPTIONS="-Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle -Dscala.repl.no-threads=true"
ISABELLE_JEDIT_OPTIONS=""
--- a/src/Tools/jEdit/src/active.scala Fri Apr 25 22:13:17 2014 +0200
+++ b/src/Tools/jEdit/src/active.scala Sat Apr 26 00:20:53 2014 +0200
@@ -30,25 +30,23 @@
// FIXME avoid hard-wired stuff
elem match {
case XML.Elem(Markup(Markup.BROWSER, _), body) =>
- default_thread_pool.submit(() =>
- {
- val graph_file = Isabelle_System.tmp_file("graph")
- File.write(graph_file, XML.content(body))
- Isabelle_System.bash_env(null,
- Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)),
- "\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &")
- })
+ Future.fork {
+ val graph_file = Isabelle_System.tmp_file("graph")
+ File.write(graph_file, XML.content(body))
+ Isabelle_System.bash_env(null,
+ Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)),
+ "\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &")
+ }
case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
- default_thread_pool.submit(() =>
- {
- val graph =
- Exn.capture {
- isabelle.graphview.Model.decode_graph(body)
- .transitive_reduction_acyclic
- }
- Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
- })
+ Future.fork {
+ val graph =
+ Exn.capture {
+ isabelle.graphview.Model.decode_graph(body)
+ .transitive_reduction_acyclic
+ }
+ Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
+ }
case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
props match {
--- a/src/Tools/jEdit/src/documentation_dockable.scala Fri Apr 25 22:13:17 2014 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Sat Apr 26 00:20:53 2014 +0200
@@ -68,13 +68,14 @@
if (path.is_file)
PIDE.editor.goto_file(view, Isabelle_System.platform_path(path))
else {
- default_thread_pool.submit(() =>
+ Future.fork {
try { Doc.view(path) }
catch {
case exn: Throwable =>
GUI.error_dialog(view,
"Documentation error", GUI.scrollable_text(Exn.message(exn)))
- })
+ }
+ }
}
case _ =>
}
--- a/src/Tools/jEdit/src/jedit_editor.scala Fri Apr 25 22:13:17 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala Sat Apr 26 00:20:53 2014 +0200
@@ -162,20 +162,21 @@
def hyperlink_url(name: String): Hyperlink =
new Hyperlink {
val external = true
- def follow(view: View) =
- default_thread_pool.submit(() =>
+ def follow(view: View): Unit =
+ Future.fork {
try { Isabelle_System.open(name) }
catch {
case exn: Throwable =>
GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
- })
+ }
+ }
override def toString: String = "URL " + quote(name)
}
def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
new Hyperlink {
val external = false
- def follow(view: View) = goto_file(view, name, line, column)
+ def follow(view: View): Unit = goto_file(view, name, line, column)
override def toString: String = "file " + quote(name)
}
--- a/src/Tools/jEdit/src/pretty_text_area.scala Fri Apr 25 22:13:17 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Sat Apr 26 00:20:53 2014 +0200
@@ -12,6 +12,7 @@
import java.awt.{Color, Font, FontMetrics, Toolkit, Window}
import java.awt.event.KeyEvent
+import java.util.concurrent.{Future => JFuture}
import org.gjt.sp.jedit.{jEdit, View, Registers}
import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea}
@@ -67,7 +68,7 @@
private var current_base_results = Command.Results.empty
private var current_rendering: Rendering =
Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2
- private var future_rendering: Option[java.util.concurrent.Future[Unit]] = None
+ private var future_rendering: Option[JFuture[Unit]] = None
private val rich_text_area =
new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
@@ -118,8 +119,8 @@
val formatted_body = Pretty.formatted(current_body, margin, metric)
future_rendering.map(_.cancel(true))
- future_rendering = Some(default_thread_pool.submit(() =>
- {
+ future_rendering =
+ Some(Simple_Thread.submit_task {
val (text, rendering) =
try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) }
catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
@@ -136,7 +137,7 @@
getBuffer.setReadOnly(true)
}
}
- }))
+ })
}
}