# HG changeset patch # User wenzelm # Date 1398464453 -7200 # Node ID 0f5cf342961c6117a151ac3870ef68f6ae74008b # Parent 75f4fdafb285459e7d7348d86dcba839872cbb66# Parent 9923e362789c2d045ba7ade79067d936fd352132 merged diff -r 75f4fdafb285 -r 0f5cf342961c etc/options --- 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" diff -r 75f4fdafb285 -r 0f5cf342961c src/HOL/Record.thy --- 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 diff -r 75f4fdafb285 -r 0f5cf342961c src/HOL/Tools/record.ML --- 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 _ = diff -r 75f4fdafb285 -r 0f5cf342961c src/Pure/Concurrent/future.scala --- 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]) diff -r 75f4fdafb285 -r 0f5cf342961c src/Pure/Concurrent/simple_thread.scala --- 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 }) } diff -r 75f4fdafb285 -r 0f5cf342961c src/Pure/PIDE/markup.ML --- 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")]; diff -r 75f4fdafb285 -r 0f5cf342961c src/Pure/PIDE/markup.scala --- 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")) diff -r 75f4fdafb285 -r 0f5cf342961c src/Pure/PIDE/session.scala --- 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() diff -r 75f4fdafb285 -r 0f5cf342961c src/Pure/System/invoke_scala.scala --- 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 } diff -r 75f4fdafb285 -r 0f5cf342961c src/Pure/System/message_channel.ML --- 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 = diff -r 75f4fdafb285 -r 0f5cf342961c src/Pure/Thy/thy_info.scala --- 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 */ diff -r 75f4fdafb285 -r 0f5cf342961c src/Pure/library.scala --- 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 } diff -r 75f4fdafb285 -r 0f5cf342961c src/Tools/jEdit/etc/settings --- 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="" diff -r 75f4fdafb285 -r 0f5cf342961c src/Tools/jEdit/src/active.scala --- 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 { diff -r 75f4fdafb285 -r 0f5cf342961c src/Tools/jEdit/src/documentation_dockable.scala --- 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 _ => } diff -r 75f4fdafb285 -r 0f5cf342961c src/Tools/jEdit/src/jedit_editor.scala --- 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) } diff -r 75f4fdafb285 -r 0f5cf342961c src/Tools/jEdit/src/pretty_text_area.scala --- 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) } } - })) + }) } }