diff --git a/src/Pure/ML/ml_statistics.scala b/src/Pure/ML/ml_statistics.scala --- a/src/Pure/ML/ml_statistics.scala +++ b/src/Pure/ML/ml_statistics.scala @@ -1,312 +1,313 @@ /* Title: Pure/ML/ml_statistics.scala Author: Makarius ML runtime statistics. */ package isabelle import scala.annotation.tailrec import scala.collection.mutable import scala.collection.immutable.{SortedSet, SortedMap} import scala.swing.{Frame, Component} import org.jfree.data.xy.{XYSeries, XYSeriesCollection} import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory} import org.jfree.chart.plot.PlotOrientation object ML_Statistics { /* properties */ val Now = new Properties.Double("now") def now(props: Properties.T): Double = Now.unapply(props).get /* memory status */ val Heap_Size = new Properties.Long("size_heap") val Heap_Free = new Properties.Long("size_heap_free_last_GC") val GC_Percent = new Properties.Int("GC_percent") sealed case class Memory_Status(heap_size: Long, heap_free: Long, gc_percent: Int) { def heap_used: Long = (heap_size - heap_free) max 0 def heap_used_fraction: Double = if (heap_size == 0) 0.0 else heap_used.toDouble / heap_size def gc_progress: Option[Double] = if (1 <= gc_percent && gc_percent <= 100) Some((gc_percent - 1) * 0.01) else None } def memory_status(props: Properties.T): Memory_Status = { val heap_size = Heap_Size.get(props) val heap_free = Heap_Free.get(props) val gc_percent = GC_Percent.get(props) Memory_Status(heap_size, heap_free, gc_percent) } /* monitor process */ def monitor(pid: Long, stats_dir: String = "", delay: Time = Time.seconds(0.5), consume: Properties.T => Unit = Console.println ): Unit = { def progress_stdout(line: String): Unit = { val props = Library.space_explode(',', line).flatMap(Properties.Eq.unapply) if (props.nonEmpty) consume(props) } val env_prefix = if (stats_dir.isEmpty) "" else "export POLYSTATSDIR=" + Bash.string(stats_dir) + "\n" Bash.process(env_prefix + "\"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " + Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " + ML_Syntax.print_double(delay.seconds)), cwd = Path.ISABELLE_HOME.file) .result(progress_stdout = progress_stdout, strict = false).check } /* protocol handler */ class Handler extends Session.Protocol_Handler { private var session: Session = null private var monitoring: Future[Unit] = Future.value(()) override def init(session: Session): Unit = synchronized { this.session = session } override def exit(): Unit = synchronized { session = null monitoring.cancel() } private def consume(props: Properties.T): Unit = synchronized { if (session != null) { val props1 = (session.cache.props(props ::: Java_Statistics.jvm_statistics())) session.runtime_statistics.post(Session.Runtime_Statistics(props1)) } } private def ml_statistics(msg: Prover.Protocol_Output): Boolean = synchronized { msg.properties match { case Markup.ML_Statistics(pid, stats_dir) => monitoring = Future.thread("ML_statistics") { monitor(pid, stats_dir = stats_dir, consume = consume) } true case _ => false } } - override val functions = List(Markup.ML_Statistics.name -> ml_statistics) + override val functions: Session.Protocol_Functions = + List(Markup.ML_Statistics.name -> ml_statistics) } /* memory fields (mega bytes) */ def mem_print(x: Long): Option[String] = if (x == 0L) None else Some(x.toString + " M") def mem_scale(x: Long): Long = x / 1024 / 1024 def mem_field_scale(name: String, x: Double): Double = if (heap_fields._2.contains(name) || program_fields._2.contains(name)) mem_scale(x.toLong).toDouble else x val CODE_SIZE = "size_code" val STACK_SIZE = "size_stacks" val HEAP_SIZE = "size_heap" /* standard fields */ type Fields = (String, List[String]) val tasks_fields: Fields = ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive", "tasks_urgent", "tasks_total")) val workers_fields: Fields = ("Worker threads", List("workers_total", "workers_active", "workers_waiting")) val GC_fields: Fields = ("GCs", List("partial_GCs", "full_GCs", "share_passes")) val heap_fields: Fields = ("Heap", List(HEAP_SIZE, "size_allocation", "size_allocation_free", "size_heap_free_last_full_GC", "size_heap_free_last_GC")) val program_fields: Fields = ("Program", List("size_code", "size_stacks")) val threads_fields: Fields = ("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar", "threads_wait_IO", "threads_wait_mutex", "threads_wait_signal")) val time_fields: Fields = ("Time", List("time_elapsed", "time_elapsed_GC", "time_CPU", "time_GC")) val speed_fields: Fields = ("Speed", List("speed_CPU", "speed_GC")) private val time_speed = Map("time_CPU" -> "speed_CPU", "time_GC" -> "speed_GC") val java_heap_fields: Fields = ("Java heap", List("java_heap_size", "java_heap_used")) val java_thread_fields: Fields = ("Java threads", List("java_threads_total", "java_workers_total", "java_workers_active")) val main_fields: List[Fields] = List(heap_fields, tasks_fields, workers_fields) val other_fields: List[Fields] = List(threads_fields, GC_fields, program_fields, time_fields, speed_fields, java_heap_fields, java_thread_fields) val all_fields: List[Fields] = main_fields ::: other_fields /* content interpretation */ final case class Entry(time: Double, data: Map[String, Double]) { def get(field: String): Double = data.getOrElse(field, 0.0) } val empty: ML_Statistics = apply(Nil) def apply( ml_statistics0: List[Properties.T], heading: String = "", domain: String => Boolean = _ => true ): ML_Statistics = { require(ml_statistics0.forall(props => Now.unapply(props).isDefined), "missing \"now\" field") val ml_statistics = ml_statistics0.sortBy(now) val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head) val duration = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.last) - time_start val fields = SortedSet.empty[String] ++ (for { props <- ml_statistics.iterator (x, _) <- props.iterator if x != Now.name && domain(x) } yield x) val content = { var last_edge = Map.empty[String, (Double, Double, Double)] val result = new mutable.ListBuffer[ML_Statistics.Entry] for (props <- ml_statistics) { val time = now(props) - time_start // rising edges -- relative speed val speeds = (for { (key, value) <- props.iterator key1 <- time_speed.get(key) if domain(key1) } yield { val (x0, y0, s0) = last_edge.getOrElse(key, (0.0, 0.0, 0.0)) val x1 = time val y1 = java.lang.Double.parseDouble(value) val s1 = if (x1 == x0) 0.0 else (y1 - y0) / (x1 - x0) if (y1 > y0) { last_edge += (key -> (x1, y1, s1)) (key1, s1.toString) } else (key1, s0.toString) }).toList val data = SortedMap.empty[String, Double] ++ (for { (x, y) <- props.iterator ++ speeds.iterator if x != Now.name && domain(x) z = java.lang.Double.parseDouble(y) if z != 0.0 } yield { (x.intern, mem_field_scale(x, z)) }) result += ML_Statistics.Entry(time, data) } result.toList } new ML_Statistics(heading, fields, content, time_start, duration) } } final class ML_Statistics private( val heading: String, val fields: Set[String], val content: List[ML_Statistics.Entry], val time_start: Double, val duration: Double ) { override def toString: String = if (content.isEmpty) "ML_Statistics.empty" else "ML_Statistics(length = " + content.length + ", fields = " + fields.size + ")" /* content */ def maximum(field: String): Double = content.foldLeft(0.0) { case (m, e) => m max e.get(field) } def average(field: String): Double = { @tailrec def sum(t0: Double, list: List[ML_Statistics.Entry], acc: Double): Double = list match { case Nil => acc case e :: es => val t = e.time sum(t, es, (t - t0) * e.get(field) + acc) } content match { case Nil => 0.0 case List(e) => e.get(field) case e :: es => sum(e.time, es, 0.0) / duration } } /* charts */ def update_data(data: XYSeriesCollection, selected_fields: List[String]): Unit = { data.removeAllSeries() for (field <- selected_fields) { val series = new XYSeries(field) content.foreach(entry => series.add(entry.time, entry.get(field))) data.addSeries(series) } } def chart(title: String, selected_fields: List[String]): JFreeChart = { val data = new XYSeriesCollection update_data(data, selected_fields) ChartFactory.createXYLineChart(title, "time", "value", data, PlotOrientation.VERTICAL, true, true, true) } def chart(fields: ML_Statistics.Fields): JFreeChart = chart(fields._1, fields._2) def show_frames(fields: List[ML_Statistics.Fields] = ML_Statistics.main_fields): Unit = fields.map(chart).foreach(c => GUI_Thread.later { new Frame { iconImage = GUI.isabelle_image() title = heading contents = Component.wrap(new ChartPanel(c)) visible = true } }) } diff --git a/src/Pure/PIDE/session.scala b/src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala +++ b/src/Pure/PIDE/session.scala @@ -1,751 +1,752 @@ /* Title: Pure/PIDE/session.scala Author: Makarius Options: :folding=explicit: PIDE editor session, potentially with running prover process. */ package isabelle import scala.collection.immutable.Queue import scala.collection.mutable import scala.annotation.tailrec object Session { /* outlets */ object Consumer { def apply[A](name: String)(consume: A => Unit): Consumer[A] = new Consumer[A](name, consume) } final class Consumer[-A] private(val name: String, val consume: A => Unit) class Outlet[A](dispatcher: Consumer_Thread[() => Unit]) { private val consumers = Synchronized[List[Consumer[A]]](Nil) def += (c: Consumer[A]): Unit = consumers.change(Library.update(c)) def -= (c: Consumer[A]): Unit = consumers.change(Library.remove(c)) def post(a: A): Unit = { for (c <- consumers.value.iterator) { dispatcher.send(() => try { c.consume(a) } catch { case exn: Throwable => Output.error_message("Consumer failed: " + quote(c.name) + "\n" + Exn.message(exn)) }) } } } /* change */ sealed case class Change( previous: Document.Version, syntax_changed: List[Document.Node.Name], deps_changed: Boolean, doc_edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name], version: Document.Version) case object Change_Flush /* events */ //{{{ case class Command_Timing(props: Properties.T) case class Theory_Timing(props: Properties.T) case class Runtime_Statistics(props: Properties.T) case class Task_Statistics(props: Properties.T) case class Global_Options(options: Options) case object Caret_Focus case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String) case class Build_Theories(id: String, master_dir: Path, theories: List[(Options, List[Path])]) case class Commands_Changed( assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command]) sealed abstract class Phase { def print: String = this match { case Terminated(result) => if (result.ok) "finished" else "failed" case _ => Word.lowercase(this.toString) } } case object Inactive extends Phase // stable case object Startup extends Phase // transient case object Ready extends Phase // metastable case object Shutdown extends Phase // transient case class Terminated(result: Process_Result) extends Phase // stable //}}} /* syslog */ private[Session] class Syslog(limit: Int) { private var queue = Queue.empty[XML.Elem] private var length = 0 def += (msg: XML.Elem): Unit = synchronized { queue = queue.enqueue(msg) length += 1 if (length > limit) queue = queue.dequeue._2 } def content: String = synchronized { cat_lines(queue.iterator.map(XML.content)) + (if (length > limit) "\n(A total of " + length + " messages...)" else "") } } /* protocol handlers */ type Protocol_Function = Prover.Protocol_Output => Boolean + type Protocol_Functions = List[(String, Protocol_Function)] abstract class Protocol_Handler extends Isabelle_System.Service { def init(session: Session): Unit = {} def exit(): Unit = {} - def functions: List[(String, Protocol_Function)] = Nil + def functions: Protocol_Functions = Nil def prover_options(options: Options): Options = options } } class Session(_session_options: => Options, val resources: Resources) extends Document.Session { session => val cache: Term.Cache = Term.Cache.make() def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = Command.Blobs_Info.none /* global flags */ @volatile var timing: Boolean = false @volatile var verbose: Boolean = false /* dynamic session options */ def session_options: Options = _session_options def output_delay: Time = session_options.seconds("editor_output_delay") def consolidate_delay: Time = session_options.seconds("editor_consolidate_delay") def prune_delay: Time = session_options.seconds("editor_prune_delay") def prune_size: Int = session_options.int("editor_prune_size") def syslog_limit: Int = session_options.int("editor_syslog_limit") def reparse_limit: Int = session_options.int("editor_reparse_limit") /* dispatcher */ private val dispatcher = Consumer_Thread.fork[() => Unit]("Session.dispatcher", daemon = true) { case e => e(); true } def assert_dispatcher[A](body: => A): A = { assert(dispatcher.check_thread()) body } def require_dispatcher[A](body: => A): A = { require(dispatcher.check_thread(), "not on dispatcher thread") body } def send_dispatcher(body: => Unit): Unit = { if (dispatcher.check_thread()) body else dispatcher.send(() => body) } def send_wait_dispatcher(body: => Unit): Unit = { if (dispatcher.check_thread()) body else dispatcher.send_wait(() => body) } /* outlets */ val finished_theories = new Session.Outlet[Document.Snapshot](dispatcher) val command_timings = new Session.Outlet[Session.Command_Timing](dispatcher) val theory_timings = new Session.Outlet[Session.Theory_Timing](dispatcher) val runtime_statistics = new Session.Outlet[Session.Runtime_Statistics](dispatcher) val task_statistics = new Session.Outlet[Session.Task_Statistics](dispatcher) val global_options = new Session.Outlet[Session.Global_Options](dispatcher) val caret_focus = new Session.Outlet[Session.Caret_Focus.type](dispatcher) val raw_edits = new Session.Outlet[Session.Raw_Edits](dispatcher) val commands_changed = new Session.Outlet[Session.Commands_Changed](dispatcher) val phase_changed = new Session.Outlet[Session.Phase](dispatcher) val syslog_messages = new Session.Outlet[Prover.Output](dispatcher) val raw_output_messages = new Session.Outlet[Prover.Output](dispatcher) val trace_events = new Session.Outlet[Simplifier_Trace.Event.type](dispatcher) val debugger_updates = new Session.Outlet[Debugger.Update.type](dispatcher) val all_messages = new Session.Outlet[Prover.Message](dispatcher) // potential bottle-neck! /** main protocol manager **/ /* internal messages */ private case class Start(start_prover: Prover.Receiver => Prover) private case object Stop private case class Get_State(promise: Promise[Document.State]) private case class Cancel_Exec(exec_id: Document_ID.Exec) private case class Protocol_Command_Raw(name: String, args: List[Bytes]) private case class Protocol_Command_Args(name: String, args: List[String]) private case class Update_Options(options: Options) private case object Consolidate_Execution private case object Prune_History /* phase */ private def post_phase(new_phase: Session.Phase): Session.Phase = { phase_changed.post(new_phase) new_phase } private val _phase = Synchronized[Session.Phase](Session.Inactive) private def phase_=(new_phase: Session.Phase): Unit = _phase.change(_ => post_phase(new_phase)) def phase: Session.Phase = _phase.value def is_ready: Boolean = phase == Session.Ready /* syslog */ private val syslog = new Session.Syslog(syslog_limit) def syslog_content(): String = syslog.content /* pipelined change parsing */ private case class Text_Edits( previous: Future[Document.Version], doc_blobs: Document.Blobs, text_edits: List[Document.Edit_Text], consolidate: List[Document.Node.Name], version_result: Promise[Document.Version]) private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true) { case Text_Edits(previous, doc_blobs, text_edits, consolidate, version_result) => val prev = previous.get_finished val change = Timing.timeit("parse_change", timing) { resources.parse_change(reparse_limit, prev, doc_blobs, text_edits, consolidate) } version_result.fulfill(change.version) manager.send(change) true } /* buffered changes */ private object change_buffer { private var assignment: Boolean = false private var nodes: Set[Document.Node.Name] = Set.empty private var commands: Set[Command] = Set.empty def flush(): Unit = synchronized { if (assignment || nodes.nonEmpty || commands.nonEmpty) commands_changed.post(Session.Commands_Changed(assignment, nodes, commands)) if (nodes.nonEmpty) consolidation.update(nodes) assignment = false nodes = Set.empty commands = Set.empty } private val delay_flush = Delay.first(output_delay) { flush() } def invoke(assign: Boolean, edited_nodes: List[Document.Node.Name], cmds: List[Command]): Unit = synchronized { assignment |= assign for (node <- edited_nodes) { nodes += node } for (command <- cmds) { nodes += command.node_name command.blobs_names.foreach(nodes += _) commands += command } delay_flush.invoke() } def shutdown(): Unit = { delay_flush.revoke() flush() } } /* postponed changes */ private object postponed_changes { private var postponed: List[Session.Change] = Nil def store(change: Session.Change): Unit = synchronized { postponed ::= change } def flush(state: Document.State): List[Session.Change] = synchronized { val (assigned, unassigned) = postponed.partition(change => state.is_assigned(change.previous)) postponed = unassigned assigned.reverse } } /* node consolidation */ private object consolidation { private val delay = Delay.first(consolidate_delay) { manager.send(Consolidate_Execution) } private val init_state: Option[Set[Document.Node.Name]] = Some(Set.empty) private val state = Synchronized(init_state) def exit(): Unit = { delay.revoke() state.change(_ => None) } def update(new_nodes: Set[Document.Node.Name] = Set.empty): Unit = { val active = state.change_result(st => (st.isDefined, st.map(nodes => if (nodes.isEmpty) new_nodes else nodes ++ new_nodes))) if (active) delay.invoke() } def flush(): Set[Document.Node.Name] = state.change_result(st => if (st.isDefined) (st.get, init_state) else (Set.empty, None)) } /* prover process */ private object prover { private val variable = Synchronized[Option[Prover]](None) def defined: Boolean = variable.value.isDefined def get: Prover = variable.value.get def set(p: Prover): Unit = variable.change(_ => Some(p)) def reset: Unit = variable.change(_ => None) def await_reset(): Unit = variable.guarded_access({ case None => Some((), None) case _ => None }) } /* file formats and protocol handlers */ private lazy val file_formats: File_Format.Session = File_Format.registry.start_session(session) private val protocol_handlers = Protocol_Handlers.init(session) def get_protocol_handler[C <: Session.Protocol_Handler](c: Class[C]): Option[C] = protocol_handlers.get(c.getName) match { case Some(h) if Library.is_subclass(h.getClass, c) => Some(h.asInstanceOf[C]) case _ => None } def init_protocol_handler(handler: Session.Protocol_Handler): Unit = protocol_handlers.init(handler) def prover_options(options: Options): Options = protocol_handlers.prover_options(file_formats.prover_options(options)) /* debugger */ private val debugger_handler = new Debugger.Handler(this) init_protocol_handler(debugger_handler) def debugger: Debugger = debugger_handler.debugger /* manager thread */ private val delay_prune = Delay.first(prune_delay) { manager.send(Prune_History) } private val manager: Consumer_Thread[Any] = { /* global state */ val global_state = Synchronized(Document.State.init) /* raw edits */ def handle_raw_edits( doc_blobs: Document.Blobs = Document.Blobs.empty, edits: List[Document.Edit_Text] = Nil, consolidate: List[Document.Node.Name] = Nil): Unit = { //{{{ require(prover.defined, "prover process not defined (handle_raw_edits)") if (edits.nonEmpty) prover.get.discontinue_execution() val previous = global_state.value.history.tip.version val version = Future.promise[Document.Version] global_state.change(_.continue_history(previous, edits, version)) raw_edits.post(Session.Raw_Edits(doc_blobs, edits)) change_parser.send(Text_Edits(previous, doc_blobs, edits, consolidate, version)) //}}} } /* resulting changes */ def handle_change(change: Session.Change): Unit = { //{{{ require(prover.defined, "prover process not defined (handle_change)") // define commands { val id_commands = new mutable.ListBuffer[Command] def id_command(command: Command): Unit = { for { (name, digest) <- command.blobs_defined if !global_state.value.defined_blob(digest) } { change.version.nodes(name).get_blob match { case Some(blob) => global_state.change(_.define_blob(digest)) prover.get.define_blob(digest, blob.bytes) case None => Output.error_message("Missing blob " + quote(name.toString)) } } if (!global_state.value.defined_command(command.id)) { global_state.change(_.define_command(command)) id_commands += command } } for { (_, edit) <- change.doc_edits } { edit.foreach({ case (c1, c2) => c1.foreach(id_command); c2.foreach(id_command) }) } if (id_commands.nonEmpty) { prover.get.define_commands_bulk(resources, id_commands.toList) } } val assignment = global_state.value.the_assignment(change.previous).check_finished global_state.change(_.define_version(change.version, assignment)) prover.get.update(change.previous.id, change.version.id, change.doc_edits, change.consolidate) resources.commit(change) //}}} } /* prover output */ def handle_output(output: Prover.Output): Unit = { //{{{ def bad_output(): Unit = { if (verbose) Output.warning("Ignoring bad prover output: " + output.message.toString) } def change_command(f: Document.State => (Command.State, Document.State)): Unit = { try { val st = global_state.change_result(f) if (!st.command.span.is_theory) { change_buffer.invoke(false, Nil, List(st.command)) } } catch { case _: Document.State.Fail => bad_output() } } output match { case msg: Prover.Protocol_Output => val handled = protocol_handlers.invoke(msg) if (!handled) { msg.properties match { case Protocol.Command_Timing(props, state_id, timing) if prover.defined => command_timings.post(Session.Command_Timing(props)) val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil))) change_command(_.accumulate(state_id, cache.elem(message), cache)) case Markup.Theory_Timing(props) => theory_timings.post(Session.Theory_Timing(props)) case Markup.Task_Statistics(props) => task_statistics.post(Session.Task_Statistics(props)) case Protocol.Export(args) if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined => val id = Value.Long.unapply(args.id.get).get val entry = Export.make_entry("", args, msg.chunk, cache) change_command(_.add_export(id, (args.serial, entry))) case Protocol.Loading_Theory(node_name, id) => val blobs_info = build_blobs_info(node_name) try { global_state.change(_.begin_theory(node_name, id, msg.text, blobs_info)) } catch { case _: Document.State.Fail => bad_output() } case List(Markup.Commands_Accepted.PROPERTY) => msg.text match { case Protocol.Commands_Accepted(ids) => ids.foreach(id => change_command(_.accumulate(id, Protocol.Commands_Accepted.message, cache))) case _ => bad_output() } case List(Markup.Assign_Update.PROPERTY) => msg.text match { case Protocol.Assign_Update(id, edited, update) => try { val (edited_nodes, cmds) = global_state.change_result(_.assign(id, edited, update)) change_buffer.invoke(true, edited_nodes, cmds) manager.send(Session.Change_Flush) } catch { case _: Document.State.Fail => bad_output() } case _ => bad_output() } delay_prune.invoke() case List(Markup.Removed_Versions.PROPERTY) => msg.text match { case Protocol.Removed(removed) => try { global_state.change(_.removed_versions(removed)) manager.send(Session.Change_Flush) } catch { case _: Document.State.Fail => bad_output() } case _ => bad_output() } case _ => bad_output() } } case _ => output.properties match { case Position.Id(state_id) => change_command(_.accumulate(state_id, output.message, cache)) case _ if output.is_init => val init_ok = try { Isabelle_System.make_services(classOf[Session.Protocol_Handler]) .foreach(init_protocol_handler) true } catch { case exn: Throwable => prover.get.protocol_command("Prover.stop", "1", Exn.message(exn)) false } if (init_ok) { prover.get.options(prover_options(session_options)) prover.get.init_session(resources) phase = Session.Ready debugger.ready() } case Markup.Process_Result(result) if output.is_exit => if (prover.defined) protocol_handlers.exit() for (id <- global_state.value.theories.keys) { val snapshot = global_state.change_result(_.end_theory(id)) finished_theories.post(snapshot) } file_formats.stop_session phase = Session.Terminated(result) prover.reset case _ => raw_output_messages.post(output) } } //}}} } /* main thread */ Consumer_Thread.fork[Any]("Session.manager", daemon = true) { case arg: Any => //{{{ arg match { case output: Prover.Output => if (output.is_syslog) { syslog += output.message syslog_messages.post(output) } if (output.is_stdout || output.is_stderr) raw_output_messages.post(output) else handle_output(output) all_messages.post(output) case input: Prover.Input => all_messages.post(input) case Start(start_prover) if !prover.defined => prover.set(start_prover(manager.send(_))) case Stop => consolidation.exit() delay_prune.revoke() if (prover.defined) { global_state.change(_ => Document.State.init) prover.get.terminate() } case Get_State(promise) => promise.fulfill(global_state.value) case Consolidate_Execution => if (prover.defined) { val state = global_state.value state.stable_tip_version match { case None => consolidation.update() case Some(version) => val consolidate = consolidation.flush().iterator.filter(name => !resources.session_base.loaded_theory(name) && !state.node_consolidated(version, name) && state.node_maybe_consolidated(version, name)).toList if (consolidate.nonEmpty) handle_raw_edits(consolidate = consolidate) } } case Prune_History => if (prover.defined) { val old_versions = global_state.change_result(_.remove_versions(prune_size)) if (old_versions.nonEmpty) prover.get.remove_versions(old_versions) } case Update_Options(options) => if (prover.defined && is_ready) { prover.get.options(prover_options(options)) handle_raw_edits() } global_options.post(Session.Global_Options(options)) case Cancel_Exec(exec_id) if prover.defined => prover.get.cancel_exec(exec_id) case Session.Raw_Edits(doc_blobs, edits) if prover.defined => handle_raw_edits(doc_blobs = doc_blobs, edits = edits) case Session.Dialog_Result(id, serial, result) if prover.defined => prover.get.dialog_result(serial, result) handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result))) case Protocol_Command_Raw(name, args) if prover.defined => prover.get.protocol_command_raw(name, args) case Protocol_Command_Args(name, args) if prover.defined => prover.get.protocol_command_args(name, args) case change: Session.Change if prover.defined => val state = global_state.value if (!state.removing_versions && state.is_assigned(change.previous)) handle_change(change) else postponed_changes.store(change) case Session.Change_Flush if prover.defined => val state = global_state.value if (!state.removing_versions) postponed_changes.flush(state).foreach(handle_change) case bad => if (verbose) Output.warning("Ignoring bad message: " + bad.toString) } true //}}} } } /* main operations */ def get_state(): Document.State = { if (manager.is_active()) { val promise = Future.promise[Document.State] manager.send_wait(Get_State(promise)) promise.join } else Document.State.init } def snapshot(name: Document.Node.Name = Document.Node.Name.empty, pending_edits: List[Text.Edit] = Nil): Document.Snapshot = get_state().snapshot(name, pending_edits) def recent_syntax(name: Document.Node.Name): Outer_Syntax = get_state().recent_finished.version.get_finished.nodes(name).syntax getOrElse resources.session_base.overall_syntax @tailrec final def await_stable_snapshot(): Document.Snapshot = { val snapshot = this.snapshot() if (snapshot.is_outdated) { output_delay.sleep() await_stable_snapshot() } else snapshot } def start(start_prover: Prover.Receiver => Prover): Unit = { file_formats _phase.change( { case Session.Inactive => manager.send(Start(start_prover)) post_phase(Session.Startup) case phase => error("Cannot start prover in phase " + quote(phase.print)) }) } def stop(): Process_Result = { val was_ready = _phase.guarded_access( { case Session.Startup | Session.Shutdown => None case Session.Terminated(_) => Some((false, phase)) case Session.Inactive => Some((false, post_phase(Session.Terminated(Process_Result(0))))) case Session.Ready => Some((true, post_phase(Session.Shutdown))) }) if (was_ready) manager.send(Stop) prover.await_reset() change_parser.shutdown() change_buffer.shutdown() manager.shutdown() dispatcher.shutdown() phase match { case Session.Terminated(result) => result case phase => error("Bad session phase after shutdown: " + quote(phase.print)) } } def protocol_command_raw(name: String, args: List[Bytes]): Unit = manager.send(Protocol_Command_Raw(name, args)) def protocol_command_args(name: String, args: List[String]): Unit = manager.send(Protocol_Command_Args(name, args)) def protocol_command(name: String, args: String*): Unit = protocol_command_args(name, args.toList) def cancel_exec(exec_id: Document_ID.Exec): Unit = manager.send(Cancel_Exec(exec_id)) def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]): Unit = if (edits.nonEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits)) def update_options(options: Options): Unit = manager.send_wait(Update_Options(options)) def dialog_result(id: Document_ID.Generic, serial: Long, result: String): Unit = manager.send(Session.Dialog_Result(id, serial, result)) } diff --git a/src/Pure/PIDE/xml.scala b/src/Pure/PIDE/xml.scala --- a/src/Pure/PIDE/xml.scala +++ b/src/Pure/PIDE/xml.scala @@ -1,433 +1,433 @@ /* Title: Pure/PIDE/xml.scala Author: Makarius Untyped XML trees and basic data representation. */ package isabelle object XML { /** XML trees **/ /* datatype representation */ type Attribute = Properties.Entry type Attributes = Properties.T sealed abstract class Tree { override def toString: String = string_of_tree(this) } type Body = List[Tree] case class Elem(markup: Markup, body: Body) extends Tree { private lazy val hash: Int = (markup, body).hashCode() override def hashCode(): Int = hash def name: String = markup.name def update_attributes(more_attributes: Attributes): Elem = if (more_attributes.isEmpty) this else Elem(markup.update_properties(more_attributes), body) def + (att: Attribute): Elem = Elem(markup + att, body) } case class Text(content: String) extends Tree { private lazy val hash: Int = content.hashCode() override def hashCode(): Int = hash } def elem(markup: Markup): XML.Elem = XML.Elem(markup, Nil) def elem(name: String, body: Body): XML.Elem = XML.Elem(Markup(name, Nil), body) def elem(name: String): XML.Elem = XML.Elem(Markup(name, Nil), Nil) val no_text: Text = Text("") val newline: Text = Text("\n") def string(s: String): Body = if (s.isEmpty) Nil else List(Text(s)) def enclose(bg: String, en:String, body: Body): Body = string(bg) ::: body ::: string(en) /* name space */ object Namespace { def apply(prefix: String, target: String): Namespace = new Namespace(prefix, target) } final class Namespace private(prefix: String, target: String) { def apply(name: String): String = prefix + ":" + name val attribute: XML.Attribute = ("xmlns:" + prefix, target) override def toString: String = attribute.toString } /* wrapped elements */ val XML_ELEM = "xml_elem" val XML_NAME = "xml_name" val XML_BODY = "xml_body" object Wrapped_Elem { def apply(markup: Markup, body1: Body, body2: Body): XML.Elem = XML.Elem(Markup(XML_ELEM, (XML_NAME, markup.name) :: markup.properties), XML.Elem(Markup(XML_BODY, Nil), body1) :: body2) def unapply(tree: Tree): Option[(Markup, Body, Body)] = tree match { case XML.Elem(Markup(XML_ELEM, (XML_NAME, name) :: props), XML.Elem(Markup(XML_BODY, Nil), body1) :: body2) => Some(Markup(name, props), body1, body2) case _ => None } } object Root_Elem { def apply(body: Body): XML.Elem = XML.Elem(Markup(XML_ELEM, Nil), body) def unapply(tree: Tree): Option[Body] = tree match { case XML.Elem(Markup(XML_ELEM, Nil), body) => Some(body) case _ => None } } /* traverse text */ def traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A = { def traverse(x: A, t: Tree): A = t match { case XML.Wrapped_Elem(_, _, ts) => ts.foldLeft(x)(traverse) case XML.Elem(_, ts) => ts.foldLeft(x)(traverse) case XML.Text(s) => op(x, s) } body.foldLeft(a)(traverse) } def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length } def symbol_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + Symbol.length(s) } /* text content */ def content(body: Body): String = { val text = new StringBuilder(text_length(body)) traverse_text(body)(()) { case (_, s) => text.append(s) } text.toString } def content(tree: Tree): String = content(List(tree)) /** string representation **/ val header: String = "\n" def output_char(s: StringBuilder, c: Char, permissive: Boolean = false): Unit = { c match { case '<' => s ++= "<" case '>' => s ++= ">" case '&' => s ++= "&" case '"' if !permissive => s ++= """ case '\'' if !permissive => s ++= "'" case _ => s += c } } def output_string(s: StringBuilder, str: String, permissive: Boolean = false): Unit = { if (str == null) s ++= str else str.iterator.foreach(output_char(s, _, permissive = permissive)) } def output_elem(s: StringBuilder, markup: Markup, end: Boolean = false): Unit = { s += '<' s ++= markup.name for ((a, b) <- markup.properties) { s += ' ' s ++= a s += '=' s += '"' output_string(s, b) s += '"' } if (end) s += '/' s += '>' } def output_elem_end(s: StringBuilder, name: String): Unit = { s += '<' s += '/' s ++= name s += '>' } def string_of_body(body: Body): String = { val s = new StringBuilder def tree(t: Tree): Unit = t match { case XML.Elem(markup, Nil) => output_elem(s, markup, end = true) case XML.Elem(markup, ts) => output_elem(s, markup) ts.foreach(tree) output_elem_end(s, markup.name) case XML.Text(txt) => output_string(s, txt) } body.foreach(tree) s.toString } def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree)) def text(s: String): String = string_of_tree(XML.Text(s)) /** cache **/ object Cache { def make( xz: XZ.Cache = XZ.Cache.make(), max_string: Int = isabelle.Cache.default_max_string, initial_size: Int = isabelle.Cache.default_initial_size): Cache = new Cache(xz, max_string, initial_size) val none: Cache = make(XZ.Cache.none, max_string = 0) } class Cache(val xz: XZ.Cache, max_string: Int, initial_size: Int) extends isabelle.Cache(max_string, initial_size) { protected def cache_props(x: Properties.T): Properties.T = { if (x.isEmpty) x else lookup(x) match { case Some(y) => y case None => store(x.map(p => (Library.isolate_substring(p._1).intern, cache_string(p._2)))) } } protected def cache_markup(x: Markup): Markup = { lookup(x) match { case Some(y) => y case None => x match { case Markup(name, props) => store(Markup(cache_string(name), cache_props(props))) } } } protected def cache_tree(x: XML.Tree): XML.Tree = { lookup(x) match { case Some(y) => y case None => x match { case XML.Elem(markup, body) => store(XML.Elem(cache_markup(markup), cache_body(body))) case XML.Text(text) => store(XML.Text(cache_string(text))) } } } protected def cache_body(x: XML.Body): XML.Body = { if (x.isEmpty) x else lookup(x) match { case Some(y) => y case None => x.map(cache_tree) } } // support hash-consing def tree0(x: XML.Tree): XML.Tree = if (no_cache) x else synchronized { lookup(x) getOrElse store(x) } // main methods def props(x: Properties.T): Properties.T = if (no_cache) x else synchronized { cache_props(x) } def markup(x: Markup): Markup = if (no_cache) x else synchronized { cache_markup(x) } def tree(x: XML.Tree): XML.Tree = if (no_cache) x else synchronized { cache_tree(x) } def body(x: XML.Body): XML.Body = if (no_cache) x else synchronized { cache_body(x) } def elem(x: XML.Elem): XML.Elem = if (no_cache) x else synchronized { cache_tree(x).asInstanceOf[XML.Elem] } } /** XML as data representation language **/ abstract class Error(s: String) extends Exception(s) class XML_Atom(s: String) extends Error(s) class XML_Body(body: XML.Body) extends Error("") object Encode { type T[A] = A => XML.Body type V[A] = PartialFunction[A, (List[String], XML.Body)] type P[A] = PartialFunction[A, List[String]] /* atomic values */ def long_atom(i: Long): String = Library.signed_string_of_long(i) def int_atom(i: Int): String = Library.signed_string_of_int(i) def bool_atom(b: Boolean): String = if (b) "1" else "0" def unit_atom(u: Unit) = "" /* structural nodes */ private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts) private def vector(xs: List[String]): XML.Attributes = xs.zipWithIndex.map({ case (x, i) => (int_atom(i), x) }) private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree = XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2) /* representation of standard types */ val tree: T[XML.Tree] = (t => List(t)) val properties: T[Properties.T] = (props => List(XML.Elem(Markup(":", props), Nil))) val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s))) val long: T[Long] = (x => string(long_atom(x))) val int: T[Int] = (x => string(int_atom(x))) val bool: T[Boolean] = (x => string(bool_atom(x))) val unit: T[Unit] = (x => string(unit_atom(x))) def pair[A, B](f: T[A], g: T[B]): T[(A, B)] = (x => List(node(f(x._1)), node(g(x._2)))) def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] = (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3)))) def list[A](f: T[A]): T[List[A]] = (xs => xs.map((x: A) => node(f(x)))) def option[A](f: T[A]): T[Option[A]] = { case None => Nil case Some(x) => List(node(f(x))) } def variant[A](fs: List[V[A]]): T[A] = { case x => val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get List(tagged(tag, f(x))) } } object Decode { type T[A] = XML.Body => A - type V[A] = (List[String], XML.Body) => A + type V[A] = PartialFunction[(List[String], XML.Body), A] type P[A] = PartialFunction[List[String], A] /* atomic values */ def long_atom(s: String): Long = try { java.lang.Long.parseLong(s) } catch { case e: NumberFormatException => throw new XML_Atom(s) } def int_atom(s: String): Int = try { Integer.parseInt(s) } catch { case e: NumberFormatException => throw new XML_Atom(s) } def bool_atom(s: String): Boolean = if (s == "1") true else if (s == "0") false else throw new XML_Atom(s) def unit_atom(s: String): Unit = if (s == "") () else throw new XML_Atom(s) /* structural nodes */ private def node(t: XML.Tree): XML.Body = t match { case XML.Elem(Markup(":", Nil), ts) => ts case _ => throw new XML_Body(List(t)) } private def vector(atts: XML.Attributes): List[String] = atts.iterator.zipWithIndex.map( { case ((a, x), i) => if (int_atom(a) == i) x else throw new XML_Atom(a) }).toList private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) = t match { case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts)) case _ => throw new XML_Body(List(t)) } /* representation of standard types */ val tree: T[XML.Tree] = { case List(t) => t case ts => throw new XML_Body(ts) } val properties: T[Properties.T] = { case List(XML.Elem(Markup(":", props), Nil)) => props case ts => throw new XML_Body(ts) } val string: T[String] = { case Nil => "" case List(XML.Text(s)) => s case ts => throw new XML_Body(ts) } val long: T[Long] = (x => long_atom(string(x))) val int: T[Int] = (x => int_atom(string(x))) val bool: T[Boolean] = (x => bool_atom(string(x))) val unit: T[Unit] = (x => unit_atom(string(x))) def pair[A, B](f: T[A], g: T[B]): T[(A, B)] = { case List(t1, t2) => (f(node(t1)), g(node(t2))) case ts => throw new XML_Body(ts) } def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] = { case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3))) case ts => throw new XML_Body(ts) } def list[A](f: T[A]): T[List[A]] = (ts => ts.map(t => f(node(t)))) def option[A](f: T[A]): T[Option[A]] = { case Nil => None case List(t) => Some(f(node(t))) case ts => throw new XML_Body(ts) } def variant[A](fs: List[V[A]]): T[A] = { case List(t) => val (tag, (xs, ts)) = tagged(t) val f = try { fs(tag) } catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) } f(xs, ts) case ts => throw new XML_Body(ts) } } } diff --git a/src/Pure/System/isabelle_system.scala b/src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala +++ b/src/Pure/System/isabelle_system.scala @@ -1,499 +1,502 @@ /* Title: Pure/System/isabelle_system.scala Author: Makarius Miscellaneous Isabelle system operations. */ package isabelle import java.util.{Map => JMap, HashMap} import java.io.{File => JFile, IOException} import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult, StandardCopyOption, FileSystemException} import java.nio.file.attribute.BasicFileAttributes import scala.jdk.CollectionConverters._ object Isabelle_System { /* settings environment */ def settings(putenv: List[(String, String)] = Nil): JMap[String, String] = { val env0 = isabelle.setup.Environment.settings() if (putenv.isEmpty) env0 else { val env = new HashMap(env0) for ((a, b) <- putenv) env.put(a, b) env } } def getenv(name: String, env: JMap[String, String] = settings()): String = Option(env.get(name)).getOrElse("") def getenv_strict(name: String, env: JMap[String, String] = settings()): String = proper_string(getenv(name, env)) getOrElse error("Undefined Isabelle environment variable: " + quote(name)) /* services */ abstract class Service @volatile private var _services: Option[List[Class[Service]]] = None def services(): List[Class[Service]] = { if (_services.isEmpty) init() // unsynchronized check _services.get } def make_services[C](c: Class[C]): List[C] = for { c1 <- services() if Library.is_subclass(c1, c) } yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C] /* init settings + services */ def make_services(): List[Class[Service]] = { def make(where: String, names: List[String]): List[Class[Service]] = { for (name <- names) yield { def err(msg: String): Nothing = error("Bad Isabelle/Scala service " + quote(name) + " in " + where + "\n" + msg) try { Class.forName(name).asInstanceOf[Class[Service]] } catch { case _: ClassNotFoundException => err("Class not found") case exn: Throwable => err(Exn.message(exn)) } } } def from_env(variable: String): List[Class[Service]] = make(quote(variable), space_explode(':', getenv_strict(variable))) def from_jar(platform_jar: String): List[Class[Service]] = make(quote(platform_jar), isabelle.setup.Build.get_services(JPath.of(platform_jar)).asScala.toList) from_env("ISABELLE_SCALA_SERVICES") ::: Scala.class_path().flatMap(from_jar) } def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = { isabelle.setup.Environment.init(isabelle_root, cygwin_root) synchronized { if (_services.isEmpty) { _services = Some(make_services()) } } } /* getetc -- static distribution parameters */ def getetc(name: String, root: Path = Path.ISABELLE_HOME): Option[String] = { val path = root + Path.basic("etc") + Path.basic(name) if (path.is_file) { Library.trim_split_lines(File.read(path)) match { case Nil => None case List(s) => Some(s) case _ => error("Single line expected in " + path.absolute) } } else None } /* Isabelle distribution identification */ def isabelle_id(root: Path = Path.ISABELLE_HOME): String = getetc("ISABELLE_ID", root = root) orElse Mercurial.archive_id(root) getOrElse { if (Mercurial.is_repository(root)) Mercurial.repository(root).parent() else error("Failed to identify Isabelle distribution " + root.expand) } object Isabelle_Id extends Scala.Fun_String("isabelle_id") { val here = Scala_Project.here def apply(arg: String): String = isabelle_id() } def isabelle_tags(root: Path = Path.ISABELLE_HOME): String = getetc("ISABELLE_TAGS", root = root) orElse Mercurial.archive_tags(root) getOrElse { if (Mercurial.is_repository(root)) { val hg = Mercurial.repository(root) hg.tags(rev = hg.parent()) } else "" } def export_isabelle_identifier(isabelle_identifier: String): String = if (isabelle_identifier == "") "" else "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n" def isabelle_identifier(): Option[String] = proper_string(getenv("ISABELLE_IDENTIFIER")) def isabelle_heading(): String = isabelle_identifier() match { case None => "" case Some(version) => " (" + version + ")" } def isabelle_name(): String = getenv_strict("ISABELLE_NAME") def identification(): String = "Isabelle" + (try { "/" + isabelle_id () } catch { case ERROR(_) => "" }) + isabelle_heading() /** file-system operations **/ /* scala functions */ - private def apply_paths(args: List[String], fun: List[Path] => Unit): List[String] = { + private def apply_paths( + args: List[String], + fun: PartialFunction[List[Path], Unit] + ): List[String] = { fun(args.map(Path.explode)) Nil } private def apply_paths1(args: List[String], fun: Path => Unit): List[String] = - apply_paths(args, { case List(path) => fun(path) case _ => ??? }) + apply_paths(args, { case List(path) => fun(path) }) private def apply_paths2(args: List[String], fun: (Path, Path) => Unit): List[String] = - apply_paths(args, { case List(path1, path2) => fun(path1, path2) case _ => ??? }) + apply_paths(args, { case List(path1, path2) => fun(path1, path2) }) private def apply_paths3(args: List[String], fun: (Path, Path, Path) => Unit): List[String] = - apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) case _ => ??? }) + apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) }) /* permissions */ def chmod(arg: String, path: Path): Unit = bash("chmod " + arg + " " + File.bash_path(path)).check def chown(arg: String, path: Path): Unit = bash("chown " + arg + " " + File.bash_path(path)).check /* directories */ def make_directory(path: Path): Path = { if (!path.is_dir) { try { Files.createDirectories(path.java_path) } catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) } } path } def new_directory(path: Path): Path = if (path.is_dir) error("Directory already exists: " + path.absolute) else make_directory(path) def copy_dir(dir1: Path, dir2: Path): Unit = { val res = bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)) if (!res.ok) { cat_error("Failed to copy directory " + dir1.absolute + " to " + dir2.absolute, res.err) } } def with_copy_dir[A](dir1: Path, dir2: Path)(body: => A): A = { if (dir2.is_file || dir2.is_dir) error("Directory already exists: " + dir2.absolute) else { try { copy_dir(dir1, dir2); body } finally { rm_tree(dir2 ) } } } object Make_Directory extends Scala.Fun_Strings("make_directory") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths1(args, make_directory) } object Copy_Dir extends Scala.Fun_Strings("copy_dir") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths2(args, copy_dir) } /* copy files */ def copy_file(src: JFile, dst: JFile): Unit = { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!File.eq(src, target)) { try { Files.copy(src.toPath, target.toPath, StandardCopyOption.COPY_ATTRIBUTES, StandardCopyOption.REPLACE_EXISTING) } catch { case ERROR(msg) => cat_error("Failed to copy file " + File.path(src).absolute + " to " + File.path(dst).absolute, msg) } } } def copy_file(src: Path, dst: Path): Unit = copy_file(src.file, dst.file) def copy_file_base(base_dir: Path, src: Path, target_dir: Path): Unit = { val src1 = src.expand val src1_dir = src1.dir if (!src1.starts_basic) error("Illegal path specification " + src1 + " beyond base directory") copy_file(base_dir + src1, Isabelle_System.make_directory(target_dir + src1_dir)) } object Copy_File extends Scala.Fun_Strings("copy_file") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths2(args, copy_file) } object Copy_File_Base extends Scala.Fun_Strings("copy_file_base") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths3(args, copy_file_base) } /* move files */ def move_file(src: JFile, dst: JFile): Unit = { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!File.eq(src, target)) Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING) } def move_file(src: Path, dst: Path): Unit = move_file(src.file, dst.file) /* symbolic link */ def symlink(src: Path, dst: Path, force: Boolean = false, native: Boolean = false): Unit = { val src_file = src.file val dst_file = dst.file val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file if (force) target.delete def cygwin_link(): Unit = { if (native) { error("Failed to create native symlink on Windows: " + quote(src_file.toString) + "\n(but it could work as Administrator)") } else isabelle.setup.Environment.cygwin_link(File.standard_path(src), target) } try { Files.createSymbolicLink(target.toPath, src_file.toPath) } catch { case _: UnsupportedOperationException if Platform.is_windows => cygwin_link() case _: FileSystemException if Platform.is_windows => cygwin_link() } } /* tmp files */ def isabelle_tmp_prefix(): JFile = { val path = Path.explode("$ISABELLE_TMP_PREFIX") path.file.mkdirs // low-level mkdirs to avoid recursion via Isabelle environment File.platform_file(path) } def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile = { val suffix = if (ext == "") "" else "." + ext val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile file.deleteOnExit() file } def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A = { val file = tmp_file(name, ext) try { body(File.path(file)) } finally { file.delete } } /* tmp dirs */ def rm_tree(root: JFile): Unit = { root.delete if (root.isDirectory) { Files.walkFileTree(root.toPath, new SimpleFileVisitor[JPath] { override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult = { try { Files.deleteIfExists(file) } catch { case _: IOException => } FileVisitResult.CONTINUE } override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult = { if (e == null) { try { Files.deleteIfExists(dir) } catch { case _: IOException => } FileVisitResult.CONTINUE } else throw e } } ) } } def rm_tree(root: Path): Unit = rm_tree(root.file) object Rm_Tree extends Scala.Fun_Strings("rm_tree") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths1(args, rm_tree) } def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile = { val dir = Files.createTempDirectory(base_dir.toPath, name).toFile dir.deleteOnExit() dir } def with_tmp_dir[A](name: String)(body: Path => A): A = { val dir = tmp_dir(name) try { body(File.path(dir)) } finally { rm_tree(dir) } } /* quasi-atomic update of directory */ def update_directory(dir: Path, f: Path => Unit): Unit = { val new_dir = dir.ext("new") val old_dir = dir.ext("old") rm_tree(new_dir) rm_tree(old_dir) f(new_dir) if (dir.is_dir) move_file(dir, old_dir) move_file(new_dir, dir) rm_tree(old_dir) } /** external processes **/ /* GNU bash */ def bash(script: String, description: String = "", cwd: JFile = null, env: JMap[String, String] = settings(), redirect: Boolean = false, input: String = "", progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), watchdog: Option[Bash.Watchdog] = None, strict: Boolean = true, cleanup: () => Unit = () => () ): Process_Result = { Bash.process(script, description = description, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup). result(input = input, progress_stdout = progress_stdout, progress_stderr = progress_stderr, watchdog = watchdog, strict = strict) } /* command-line tools */ def require_command(cmd: String, test: String = "--version"): Unit = { if (!bash(Bash.string(cmd) + " " + test).ok) error("Missing system command: " + quote(cmd)) } private lazy val gnutar_check: Boolean = try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") } catch { case ERROR(_) => false } def gnutar( args: String, dir: Path = Path.current, original_owner: Boolean = false, strip: Int = 0, redirect: Boolean = false ): Process_Result = { val options = (if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") + (if (original_owner) "" else "--owner=root --group=staff ") + (if (strip <= 0) "" else "--strip-components=" + strip + " ") if (gnutar_check) bash("tar " + options + args, redirect = redirect) else error("Expected to find GNU tar executable") } def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = { with_tmp_file("patch") { patch => Isabelle_System.bash( "diff -ru " + diff_options + " -- " + File.bash_path(src) + " " + File.bash_path(dst) + " > " + File.bash_path(patch), cwd = base_dir.file).check_rc(_ <= 1) File.read(patch) } } def hostname(): String = bash("hostname -s").check.out def open(arg: String): Unit = bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &") def pdf_viewer(arg: Path): Unit = bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &") def open_external_file(name: String): Boolean = { val ext = Library.take_suffix((c: Char) => c != '.', name.toList)._2.mkString val external = ext.nonEmpty && Library.space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext) if (external) { if (ext == "pdf" && Path.is_wellformed(name)) pdf_viewer(Path.explode(name)) else open(name) } external } /** Isabelle resources **/ /* repository clone with Admin */ def admin(): Boolean = Path.explode("~~/Admin").is_dir /* default logic */ def default_logic(args: String*): String = { args.find(_ != "") match { case Some(logic) => logic case None => getenv_strict("ISABELLE_LOGIC") } } /* download file */ def download(url_name: String, progress: Progress = new Progress): HTTP.Content = { val url = Url(url_name) progress.echo("Getting " + quote(url_name)) try { HTTP.Client.get(url) } catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) } } def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit = Bytes.write(file, download(url_name, progress = progress).bytes) object Download extends Scala.Fun("download", thread = true) { val here = Scala_Project.here override def invoke(args: List[Bytes]): List[Bytes] = - args match { case List(url) => List(download(url.text).bytes) case _ => ??? } + args.map(url => download(url.text).bytes) } /* repositories */ val isabelle_repository: Mercurial.Server = Mercurial.Server("https://isabelle.sketis.net/repos/isabelle") val afp_repository: Mercurial.Server = Mercurial.Server("https://isabelle.sketis.net/repos/afp-devel") def official_releases(): List[String] = Library.trim_split_lines( isabelle_repository.read_file(Path.explode("Admin/Release/official"))) } diff --git a/src/Pure/System/scala.scala b/src/Pure/System/scala.scala --- a/src/Pure/System/scala.scala +++ b/src/Pure/System/scala.scala @@ -1,262 +1,323 @@ /* Title: Pure/System/scala.scala Author: Makarius Support for Scala at runtime. */ package isabelle import java.io.{File => JFile, StringWriter, PrintWriter} import scala.tools.nsc.{GenericRunnerSettings, ConsoleWriter, NewLinePrintWriter} import scala.tools.nsc.interpreter.{IMain, Results} import scala.tools.nsc.interpreter.shell.ReplReporterImpl object Scala { /** registered functions **/ abstract class Fun(val name: String, val thread: Boolean = false) { override def toString: String = name def multi: Boolean = true def position: Properties.T = here.position def here: Scala_Project.Here def invoke(args: List[Bytes]): List[Bytes] } abstract class Fun_Strings(name: String, thread: Boolean = false) extends Fun(name, thread = thread) { override def invoke(args: List[Bytes]): List[Bytes] = apply(args.map(_.text)).map(Bytes.apply) def apply(args: List[String]): List[String] } abstract class Fun_String(name: String, thread: Boolean = false) extends Fun_Strings(name, thread = thread) { override def multi: Boolean = false override def apply(args: List[String]): List[String] = List(apply(Library.the_single(args))) def apply(arg: String): String } class Functions(val functions: Fun*) extends Isabelle_System.Service lazy val functions: List[Fun] = Isabelle_System.make_services(classOf[Functions]).flatMap(_.functions) /** demo functions **/ object Echo extends Fun_String("echo") { val here = Scala_Project.here def apply(arg: String): String = arg } object Sleep extends Fun_String("sleep") { val here = Scala_Project.here def apply(seconds: String): String = { val t = seconds match { case Value.Double(s) => Time.seconds(s) case _ => error("Malformed argument: " + quote(seconds)) } val t0 = Time.now() t.sleep() val t1 = Time.now() (t1 - t0).toString } } /** compiler **/ def class_path(): List[String] = for { prop <- List("isabelle.scala.classpath", "java.class.path") elems = System.getProperty(prop, "") if elems.nonEmpty elem <- space_explode(JFile.pathSeparatorChar, elems) if elem.nonEmpty } yield elem object Compiler { + def default_print_writer: PrintWriter = + new NewLinePrintWriter(new ConsoleWriter, true) + def context( + print_writer: PrintWriter = default_print_writer, error: String => Unit = Exn.error, - jar_dirs: List[JFile] = Nil + jar_dirs: List[JFile] = Nil, + class_loader: Option[ClassLoader] = None ): Context = { def find_jars(dir: JFile): List[String] = File.find_files(dir, file => file.getName.endsWith(".jar")). map(File.absolute_name) val settings = new GenericRunnerSettings(error) settings.classpath.value = (class_path() ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator) - new Context(settings) + new Context(settings, print_writer, class_loader) } - def default_print_writer: PrintWriter = - new NewLinePrintWriter(new ConsoleWriter, true) - - class Context private [Compiler](val settings: GenericRunnerSettings) { + class Context private [Compiler]( + val settings: GenericRunnerSettings, + val print_writer: PrintWriter, + val class_loader: Option[ClassLoader] + ) { override def toString: String = settings.toString - def interpreter( - print_writer: PrintWriter = default_print_writer, - class_loader: ClassLoader = null - ): IMain = { + val interp: IMain = new IMain(settings, new ReplReporterImpl(settings, print_writer)) { override def parentClassLoader: ClassLoader = - if (class_loader == null) super.parentClassLoader - else class_loader + class_loader getOrElse super.parentClassLoader } - } + } - def toplevel(interpret: Boolean, source: String): List[String] = { - val out = new StringWriter - val interp = interpreter(new PrintWriter(out)) - val marker = '\u000b' - val ok = - interp.withLabel(marker.toString) { - if (interpret) interp.interpret(source) == Results.Success - else (new interp.ReadEvalPrint).compile(source) - } - out.close() + def toplevel(interpret: Boolean, source: String): List[String] = { + val out = new StringWriter + val interp = Compiler.context(print_writer = new PrintWriter(out)).interp + val marker = '\u000b' + val ok = + interp.withLabel(marker.toString) { + if (interpret) interp.interpret(source) == Results.Success + else (new interp.ReadEvalPrint).compile(source) + } + out.close() - val Error = """(?s)^\S* error: (.*)$""".r - val errors = - space_explode(marker, Library.strip_ansi_color(out.toString)). - collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) }) + val Error = """(?s)^\S* error: (.*)$""".r + val errors = + space_explode(marker, Library.strip_ansi_color(out.toString)). + collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) }) - if (!ok && errors.isEmpty) List("Error") else errors - } + if (!ok && errors.isEmpty) List("Error") else errors } } object Toplevel extends Fun_String("scala_toplevel") { val here = Scala_Project.here def apply(arg: String): String = { val (interpret, source) = YXML.parse_body(arg) match { case Nil => (false, "") case List(XML.Text(source)) => (false, source) case body => import XML.Decode._; pair(bool, string)(body) } val errors = - try { Compiler.context().toplevel(interpret, source) } + try { Compiler.toplevel(interpret, source) } catch { case ERROR(msg) => List(msg) } locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) } } } + /** interpreter thread **/ + + object Interpreter { + /* requests */ + + sealed abstract class Request + case class Execute(command: Compiler.Context => Unit) extends Request + case object Shutdown extends Request + + + /* known interpreters */ + + private val known = Synchronized(Set.empty[Interpreter]) + + def add(interpreter: Interpreter): Unit = known.change(_ + interpreter) + def del(interpreter: Interpreter): Unit = known.change(_ - interpreter) + + def get[A](which: PartialFunction[Interpreter, A]): Option[A] = + known.value.collectFirst(which) + } + + class Interpreter(context: Compiler.Context) { + interpreter => + + private val running = Synchronized[Option[Thread]](None) + def running_thread(thread: Thread): Boolean = running.value.contains(thread) + def interrupt_thread(): Unit = running.change({ opt => opt.foreach(_.interrupt()); opt }) + + private lazy val thread: Consumer_Thread[Interpreter.Request] = + Consumer_Thread.fork("Scala.Interpreter") { + case Interpreter.Execute(command) => + try { + running.change(_ => Some(Thread.currentThread())) + command(context) + } + finally { + running.change(_ => None) + Exn.Interrupt.dispose() + } + true + case Interpreter.Shutdown => + Interpreter.del(interpreter) + false + } + + def shutdown(): Unit = { + thread.send(Interpreter.Shutdown) + interrupt_thread() + thread.shutdown() + } + + def execute(command: Compiler.Context => Unit): Unit = + thread.send(Interpreter.Execute(command)) + + Interpreter.add(interpreter) + thread + } + + + /** invoke Scala functions from ML **/ /* invoke function */ object Tag extends Enumeration { val NULL, OK, ERROR, FAIL, INTERRUPT = Value } def function_thread(name: String): Boolean = functions.find(fun => fun.name == name) match { case Some(fun) => fun.thread case None => false } def function_body(name: String, args: List[Bytes]): (Tag.Value, List[Bytes]) = functions.find(fun => fun.name == name) match { case Some(fun) => Exn.capture { fun.invoke(args) } match { case Exn.Res(null) => (Tag.NULL, Nil) case Exn.Res(res) => (Tag.OK, res) case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, Nil) case Exn.Exn(e) => (Tag.ERROR, List(Bytes(Exn.message(e)))) } case None => (Tag.FAIL, List(Bytes("Unknown Isabelle/Scala function: " + quote(name)))) } /* protocol handler */ class Handler extends Session.Protocol_Handler { private var session: Session = null private var futures = Map.empty[String, Future[Unit]] override def init(session: Session): Unit = synchronized { this.session = session } override def exit(): Unit = synchronized { for ((id, future) <- futures) cancel(id, future) futures = Map.empty } private def result(id: String, tag: Scala.Tag.Value, res: List[Bytes]): Unit = synchronized { if (futures.isDefinedAt(id)) { session.protocol_command_raw("Scala.result", Bytes(id) :: Bytes(tag.id.toString) :: res) futures -= id } } private def cancel(id: String, future: Future[Unit]): Unit = { future.cancel() result(id, Scala.Tag.INTERRUPT, Nil) } private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized { msg.properties match { case Markup.Invoke_Scala(name, id) => - def body: Unit = { + def body(): Unit = { val (tag, res) = Scala.function_body(name, msg.chunks) result(id, tag, res) } val future = if (Scala.function_thread(name)) { - Future.thread(name = Isabelle_Thread.make_name(base = "invoke_scala"))(body) + Future.thread(name = Isabelle_Thread.make_name(base = "invoke_scala"))(body()) } - else Future.fork(body) + else Future.fork(body()) futures += (id -> future) true case _ => false } } private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized { msg.properties match { case Markup.Cancel_Scala(id) => futures.get(id) match { case Some(future) => cancel(id, future) case None => } true case _ => false } } - override val functions = + override val functions: Session.Protocol_Functions = List( Markup.Invoke_Scala.name -> invoke_scala, Markup.Cancel_Scala.name -> cancel_scala) } } class Scala_Functions extends Scala.Functions( Scala.Echo, Scala.Sleep, Scala.Toplevel, Bytes.Decode_Base64, Bytes.Encode_Base64, Doc.Doc_Names, Bibtex.Check_Database, Isabelle_System.Make_Directory, Isabelle_System.Copy_Dir, Isabelle_System.Copy_File, Isabelle_System.Copy_File_Base, Isabelle_System.Rm_Tree, Isabelle_System.Download, Isabelle_System.Isabelle_Id, Isabelle_Tool.Isabelle_Tools, isabelle.atp.SystemOnTPTP.List_Systems, isabelle.atp.SystemOnTPTP.Run_System) diff --git a/src/Pure/Thy/export_theory.scala b/src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala +++ b/src/Pure/Thy/export_theory.scala @@ -1,779 +1,778 @@ /* Title: Pure/Thy/export_theory.scala Author: Makarius Export foundational theory content. */ package isabelle import scala.collection.immutable.SortedMap object Export_Theory { /** session content **/ sealed case class Session(name: String, theory_graph: Graph[String, Option[Theory]]) { override def toString: String = name def theory(theory_name: String): Option[Theory] = if (theory_graph.defined(theory_name)) theory_graph.get_node(theory_name) else None def theories: List[Theory] = theory_graph.topological_order.flatMap(theory) } def read_session( store: Sessions.Store, sessions_structure: Sessions.Structure, session_name: String, progress: Progress = new Progress, cache: Term.Cache = Term.Cache.make()): Session = { val thys = sessions_structure.build_requirements(List(session_name)).flatMap(session => using(store.open_database(session)) { db => db.transaction { for (theory <- Export.read_theory_names(db, session)) yield { progress.echo("Reading theory " + theory) val provider = Export.Provider.database(db, store.cache, session, theory) read_theory(provider, session, theory, cache = cache) } } }) val graph0 = thys.foldLeft(Graph.string[Option[Theory]]) { case (g, thy) => g.default_node(thy.name, Some(thy)) } val graph1 = thys.foldLeft(graph0) { case (g0, thy) => thy.parents.foldLeft(g0) { case (g1, parent) => g1.default_node(parent, None).add_edge_acyclic(parent, thy.name) } } Session(session_name, graph1) } /** theory content **/ sealed case class Theory(name: String, parents: List[String], types: List[Entity[Type]], consts: List[Entity[Const]], axioms: List[Entity[Axiom]], thms: List[Entity[Thm]], classes: List[Entity[Class]], locales: List[Entity[Locale]], locale_dependencies: List[Entity[Locale_Dependency]], classrel: List[Classrel], arities: List[Arity], constdefs: List[Constdef], typedefs: List[Typedef], datatypes: List[Datatype], spec_rules: List[Spec_Rule], others: Map[String, List[Entity[Other]]] ) { override def toString: String = name def entity_iterator: Iterator[Entity[No_Content]] = types.iterator.map(_.no_content) ++ consts.iterator.map(_.no_content) ++ axioms.iterator.map(_.no_content) ++ thms.iterator.map(_.no_content) ++ classes.iterator.map(_.no_content) ++ locales.iterator.map(_.no_content) ++ locale_dependencies.iterator.map(_.no_content) ++ (for { (_, xs) <- others; x <- xs.iterator } yield x.no_content) def cache(cache: Term.Cache): Theory = Theory(cache.string(name), parents.map(cache.string), types.map(_.cache(cache)), consts.map(_.cache(cache)), axioms.map(_.cache(cache)), thms.map(_.cache(cache)), classes.map(_.cache(cache)), locales.map(_.cache(cache)), locale_dependencies.map(_.cache(cache)), classrel.map(_.cache(cache)), arities.map(_.cache(cache)), constdefs.map(_.cache(cache)), typedefs.map(_.cache(cache)), datatypes.map(_.cache(cache)), spec_rules.map(_.cache(cache)), (for ((k, xs) <- others.iterator) yield cache.string(k) -> xs.map(_.cache(cache))).toMap) } def read_theory_parents(provider: Export.Provider, theory_name: String): Option[List[String]] = { if (theory_name == Thy_Header.PURE) Some(Nil) else { provider(Export.THEORY_PREFIX + "parents") .map(entry => split_lines(entry.uncompressed.text)) } } def no_theory: Theory = Theory("", Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Map.empty) def read_theory( provider: Export.Provider, session_name: String, theory_name: String, cache: Term.Cache = Term.Cache.none ): Theory = { val parents = read_theory_parents(provider, theory_name) getOrElse error("Missing theory export in session " + quote(session_name) + ": " + quote(theory_name)) val theory = Theory(theory_name, parents, read_types(provider), read_consts(provider), read_axioms(provider), read_thms(provider), read_classes(provider), read_locales(provider), read_locale_dependencies(provider), read_classrel(provider), read_arities(provider), read_constdefs(provider), read_typedefs(provider), read_datatypes(provider), read_spec_rules(provider), read_others(provider)) if (cache.no_cache) theory else theory.cache(cache) } def read_pure[A](store: Sessions.Store, read: (Export.Provider, String, String) => A): A = { val session_name = Thy_Header.PURE val theory_name = Thy_Header.PURE using(store.open_database(session_name)) { db => db.transaction { val provider = Export.Provider.database(db, store.cache, session_name, theory_name) read(provider, session_name, theory_name) } } } def read_pure_theory(store: Sessions.Store, cache: Term.Cache = Term.Cache.none): Theory = read_pure(store, read_theory(_, _, _, cache = cache)) def read_pure_proof( store: Sessions.Store, id: Thm_Id, cache: Term.Cache = Term.Cache.none): Option[Proof] = read_pure(store, (provider, _, _) => read_proof(provider, id, cache = cache)) /* entities */ object Kind { val TYPE = "type" val CONST = "const" val THM = "thm" val PROOF = "proof" val LOCALE_DEPENDENCY = "locale_dependency" val DOCUMENT_HEADING = "document_heading" val DOCUMENT_TEXT = "document_text" val PROOF_TEXT = "proof_text" } def export_kind(kind: String): String = if (kind == Markup.TYPE_NAME) Kind.TYPE else if (kind == Markup.CONSTANT) Kind.CONST else kind def export_kind_name(kind: String, name: String): String = name + "|" + export_kind(kind) abstract class Content[T] { def cache(cache: Term.Cache): T } sealed case class No_Content() extends Content[No_Content] { def cache(cache: Term.Cache): No_Content = this } sealed case class Entity[A <: Content[A]]( kind: String, name: String, xname: String, pos: Position.T, id: Option[Long], serial: Long, content: Option[A] ) { val kname: String = export_kind_name(kind, name) val range: Symbol.Range = Position.Range.unapply(pos).getOrElse(Text.Range.offside) def export_kind: String = Export_Theory.export_kind(kind) override def toString: String = export_kind + " " + quote(name) def the_content: A = if (content.isDefined) content.get else error("No content for " + toString) def no_content: Entity[No_Content] = copy(content = None) def cache(cache: Term.Cache): Entity[A] = Entity( cache.string(kind), cache.string(name), cache.string(xname), cache.position(pos), id, serial, content.map(_.cache(cache))) } def read_entities[A <: Content[A]]( provider: Export.Provider, export_name: String, kind: String, decode: XML.Decode.T[A] ): List[Entity[A]] = { def decode_entity(tree: XML.Tree): Entity[A] = { def err(): Nothing = throw new XML.XML_Body(List(tree)) tree match { case XML.Elem(Markup(Markup.ENTITY, props), body) => val name = Markup.Name.unapply(props) getOrElse err() val xname = Markup.XName.unapply(props) getOrElse err() val pos = props.filter(p => Markup.position_property(p) && p._1 != Markup.ID) val id = Position.Id.unapply(props) val serial = Markup.Serial.unapply(props) getOrElse err() val content = if (body.isEmpty) None else Some(decode(body)) Entity(kind, name, xname, pos, id, serial, content) case _ => err() } } provider.uncompressed_yxml(export_name).map(decode_entity) } /* approximative syntax */ object Assoc extends Enumeration { val NO_ASSOC, LEFT_ASSOC, RIGHT_ASSOC = Value } sealed abstract class Syntax case object No_Syntax extends Syntax case class Prefix(delim: String) extends Syntax case class Infix(assoc: Assoc.Value, delim: String, pri: Int) extends Syntax def decode_syntax: XML.Decode.T[Syntax] = XML.Decode.variant(List( - { case (Nil, Nil) => No_Syntax case _ => ??? }, - { case (List(delim), Nil) => Prefix(delim) case _ => ??? }, + { case (Nil, Nil) => No_Syntax }, + { case (List(delim), Nil) => Prefix(delim) }, { case (Nil, body) => import XML.Decode._ val (ass, delim, pri) = triple(int, string, int)(body) - Infix(Assoc(ass), delim, pri) - case _ => ??? })) + Infix(Assoc(ass), delim, pri) })) /* types */ sealed case class Type(syntax: Syntax, args: List[String], abbrev: Option[Term.Typ]) extends Content[Type] { override def cache(cache: Term.Cache): Type = Type( syntax, args.map(cache.string), abbrev.map(cache.typ)) } def read_types(provider: Export.Provider): List[Entity[Type]] = read_entities(provider, Export.THEORY_PREFIX + "types", Markup.TYPE_NAME, { body => import XML.Decode._ val (syntax, args, abbrev) = triple(decode_syntax, list(string), option(Term_XML.Decode.typ))(body) Type(syntax, args, abbrev) }) /* consts */ sealed case class Const( syntax: Syntax, typargs: List[String], typ: Term.Typ, abbrev: Option[Term.Term], propositional: Boolean ) extends Content[Const] { override def cache(cache: Term.Cache): Const = Const( syntax, typargs.map(cache.string), cache.typ(typ), abbrev.map(cache.term), propositional) } def read_consts(provider: Export.Provider): List[Entity[Const]] = read_entities(provider, Export.THEORY_PREFIX + "consts", Markup.CONSTANT, { body => import XML.Decode._ val (syntax, (typargs, (typ, (abbrev, propositional)))) = pair(decode_syntax, pair(list(string), pair(Term_XML.Decode.typ, pair(option(Term_XML.Decode.term), bool))))(body) Const(syntax, typargs, typ, abbrev, propositional) }) /* axioms */ sealed case class Prop( typargs: List[(String, Term.Sort)], args: List[(String, Term.Typ)], term: Term.Term ) extends Content[Prop] { override def cache(cache: Term.Cache): Prop = Prop( typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }), args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }), cache.term(term)) } def decode_prop(body: XML.Body): Prop = { val (typargs, args, t) = { import XML.Decode._ import Term_XML.Decode._ triple(list(pair(string, sort)), list(pair(string, typ)), term)(body) } Prop(typargs, args, t) } sealed case class Axiom(prop: Prop) extends Content[Axiom] { override def cache(cache: Term.Cache): Axiom = Axiom(prop.cache(cache)) } def read_axioms(provider: Export.Provider): List[Entity[Axiom]] = read_entities(provider, Export.THEORY_PREFIX + "axioms", Markup.AXIOM, body => Axiom(decode_prop(body))) /* theorems */ sealed case class Thm_Id(serial: Long, theory_name: String) { def pure: Boolean = theory_name == Thy_Header.PURE } sealed case class Thm( prop: Prop, deps: List[String], proof: Term.Proof) extends Content[Thm] { override def cache(cache: Term.Cache): Thm = Thm( prop.cache(cache), deps.map(cache.string), cache.proof(proof)) } def read_thms(provider: Export.Provider): List[Entity[Thm]] = read_entities(provider, Export.THEORY_PREFIX + "thms", Kind.THM, { body => import XML.Decode._ import Term_XML.Decode._ val (prop, deps, prf) = triple(decode_prop, list(string), proof)(body) Thm(prop, deps, prf) }) sealed case class Proof( typargs: List[(String, Term.Sort)], args: List[(String, Term.Typ)], term: Term.Term, proof: Term.Proof ) { def prop: Prop = Prop(typargs, args, term) def cache(cache: Term.Cache): Proof = Proof( typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }), args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }), cache.term(term), cache.proof(proof)) } def read_proof( provider: Export.Provider, id: Thm_Id, cache: Term.Cache = Term.Cache.none ): Option[Proof] = { for { entry <- provider.focus(id.theory_name)(Export.PROOFS_PREFIX + id.serial) } yield { val body = entry.uncompressed_yxml val (typargs, (args, (prop_body, proof_body))) = { import XML.Decode._ import Term_XML.Decode._ pair(list(pair(string, sort)), pair(list(pair(string, typ)), pair(x => x, x => x)))(body) } val env = args.toMap val prop = Term_XML.Decode.term_env(env)(prop_body) val proof = Term_XML.Decode.proof_env(env)(proof_body) val result = Proof(typargs, args, prop, proof) if (cache.no_cache) result else result.cache(cache) } } def read_proof_boxes( store: Sessions.Store, provider: Export.Provider, proof: Term.Proof, suppress: Thm_Id => Boolean = _ => false, cache: Term.Cache = Term.Cache.none ): List[(Thm_Id, Proof)] = { var seen = Set.empty[Long] var result = SortedMap.empty[Long, (Thm_Id, Proof)] def boxes(context: Option[(Long, Term.Proof)], prf: Term.Proof): Unit = { prf match { case Term.Abst(_, _, p) => boxes(context, p) case Term.AbsP(_, _, p) => boxes(context, p) case Term.Appt(p, _) => boxes(context, p) case Term.AppP(p, q) => boxes(context, p); boxes(context, q) case thm: Term.PThm if !seen(thm.serial) => seen += thm.serial val id = Thm_Id(thm.serial, thm.theory_name) if (!suppress(id)) { val read = if (id.pure) Export_Theory.read_pure_proof(store, id, cache = cache) else Export_Theory.read_proof(provider, id, cache = cache) read match { case Some(p) => result += (thm.serial -> (id -> p)) boxes(Some((thm.serial, p.proof)), p.proof) case None => error("Missing proof " + thm.serial + " (theory " + quote (thm.theory_name) + ")" + (context match { case None => "" case Some((i, p)) => " in proof " + i + ":\n" + p })) } } case _ => } } boxes(None, proof) result.iterator.map(_._2).toList } /* type classes */ sealed case class Class(params: List[(String, Term.Typ)], axioms: List[Prop]) extends Content[Class] { override def cache(cache: Term.Cache): Class = Class( params.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }), axioms.map(_.cache(cache))) } def read_classes(provider: Export.Provider): List[Entity[Class]] = read_entities(provider, Export.THEORY_PREFIX + "classes", Markup.CLASS, { body => import XML.Decode._ import Term_XML.Decode._ val (params, axioms) = pair(list(pair(string, typ)), list(decode_prop))(body) Class(params, axioms) }) /* locales */ sealed case class Locale( typargs: List[(String, Term.Sort)], args: List[((String, Term.Typ), Syntax)], axioms: List[Prop] ) extends Content[Locale] { override def cache(cache: Term.Cache): Locale = Locale( typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }), args.map({ case ((name, typ), syntax) => ((cache.string(name), cache.typ(typ)), syntax) }), axioms.map(_.cache(cache))) } def read_locales(provider: Export.Provider): List[Entity[Locale]] = read_entities(provider, Export.THEORY_PREFIX + "locales", Markup.LOCALE, { body => import XML.Decode._ import Term_XML.Decode._ val (typargs, args, axioms) = triple(list(pair(string, sort)), list(pair(pair(string, typ), decode_syntax)), list(decode_prop))(body) Locale(typargs, args, axioms) }) /* locale dependencies */ sealed case class Locale_Dependency( source: String, target: String, prefix: List[(String, Boolean)], subst_types: List[((String, Term.Sort), Term.Typ)], subst_terms: List[((String, Term.Typ), Term.Term)] ) extends Content[Locale_Dependency] { override def cache(cache: Term.Cache): Locale_Dependency = Locale_Dependency( cache.string(source), cache.string(target), prefix.map({ case (name, mandatory) => (cache.string(name), mandatory) }), subst_types.map({ case ((a, s), ty) => ((cache.string(a), cache.sort(s)), cache.typ(ty)) }), subst_terms.map({ case ((x, ty), t) => ((cache.string(x), cache.typ(ty)), cache.term(t)) })) def is_inclusion: Boolean = subst_types.isEmpty && subst_terms.isEmpty } def read_locale_dependencies(provider: Export.Provider): List[Entity[Locale_Dependency]] = read_entities(provider, Export.THEORY_PREFIX + "locale_dependencies", Kind.LOCALE_DEPENDENCY, { body => import XML.Decode._ import Term_XML.Decode._ val (source, (target, (prefix, (subst_types, subst_terms)))) = pair(string, pair(string, pair(list(pair(string, bool)), pair(list(pair(pair(string, sort), typ)), list(pair(pair(string, typ), term))))))(body) Locale_Dependency(source, target, prefix, subst_types, subst_terms) }) /* sort algebra */ sealed case class Classrel(class1: String, class2: String, prop: Prop) { def cache(cache: Term.Cache): Classrel = Classrel(cache.string(class1), cache.string(class2), prop.cache(cache)) } def read_classrel(provider: Export.Provider): List[Classrel] = { val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "classrel") val classrel = { import XML.Decode._ list(pair(decode_prop, pair(string, string)))(body) } for ((prop, (c1, c2)) <- classrel) yield Classrel(c1, c2, prop) } sealed case class Arity( type_name: String, domain: List[Term.Sort], codomain: String, prop: Prop ) { def cache(cache: Term.Cache): Arity = Arity(cache.string(type_name), domain.map(cache.sort), cache.string(codomain), prop.cache(cache)) } def read_arities(provider: Export.Provider): List[Arity] = { val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "arities") val arities = { import XML.Decode._ import Term_XML.Decode._ list(pair(decode_prop, triple(string, list(sort), string)))(body) } for ((prop, (a, b, c)) <- arities) yield Arity(a, b, c, prop) } /* Pure constdefs */ sealed case class Constdef(name: String, axiom_name: String) { def cache(cache: Term.Cache): Constdef = Constdef(cache.string(name), cache.string(axiom_name)) } def read_constdefs(provider: Export.Provider): List[Constdef] = { val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "constdefs") val constdefs = { import XML.Decode._ list(pair(string, string))(body) } for ((name, axiom_name) <- constdefs) yield Constdef(name, axiom_name) } /* HOL typedefs */ sealed case class Typedef( name: String, rep_type: Term.Typ, abs_type: Term.Typ, rep_name: String, abs_name: String, axiom_name: String ) { def cache(cache: Term.Cache): Typedef = Typedef(cache.string(name), cache.typ(rep_type), cache.typ(abs_type), cache.string(rep_name), cache.string(abs_name), cache.string(axiom_name)) } def read_typedefs(provider: Export.Provider): List[Typedef] = { val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "typedefs") val typedefs = { import XML.Decode._ import Term_XML.Decode._ list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body) } for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs } yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name) } /* HOL datatypes */ sealed case class Datatype( pos: Position.T, name: String, co: Boolean, typargs: List[(String, Term.Sort)], typ: Term.Typ, constructors: List[(Term.Term, Term.Typ)] ) { def id: Option[Long] = Position.Id.unapply(pos) def cache(cache: Term.Cache): Datatype = Datatype( cache.position(pos), cache.string(name), co, typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }), cache.typ(typ), constructors.map({ case (term, typ) => (cache.term(term), cache.typ(typ)) })) } def read_datatypes(provider: Export.Provider): List[Datatype] = { val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "datatypes") val datatypes = { import XML.Decode._ import Term_XML.Decode._ list(pair(properties, pair(string, pair(bool, pair(list(pair(string, sort)), pair(typ, list(pair(term, typ))))))))(body) } for ((pos, (name, (co, (typargs, (typ, constructors))))) <- datatypes) yield Datatype(pos, name, co, typargs, typ, constructors) } /* Pure spec rules */ sealed abstract class Recursion { def cache(cache: Term.Cache): Recursion = this match { case Primrec(types) => Primrec(types.map(cache.string)) case Primcorec(types) => Primcorec(types.map(cache.string)) case _ => this } } case class Primrec(types: List[String]) extends Recursion case object Recdef extends Recursion case class Primcorec(types: List[String]) extends Recursion case object Corec extends Recursion case object Unknown_Recursion extends Recursion val decode_recursion: XML.Decode.T[Recursion] = { import XML.Decode._ variant(List( - { case (Nil, a) => Primrec(list(string)(a)) case _ => ??? }, - { case (Nil, Nil) => Recdef case _ => ??? }, - { case (Nil, a) => Primcorec(list(string)(a)) case _ => ??? }, - { case (Nil, Nil) => Corec case _ => ??? }, - { case (Nil, Nil) => Unknown_Recursion case _ => ??? })) + { case (Nil, a) => Primrec(list(string)(a)) }, + { case (Nil, Nil) => Recdef }, + { case (Nil, a) => Primcorec(list(string)(a)) }, + { case (Nil, Nil) => Corec }, + { case (Nil, Nil) => Unknown_Recursion })) } sealed abstract class Rough_Classification { def is_equational: Boolean = this.isInstanceOf[Equational] def is_inductive: Boolean = this == Inductive def is_co_inductive: Boolean = this == Co_Inductive def is_relational: Boolean = is_inductive || is_co_inductive def is_unknown: Boolean = this == Unknown def cache(cache: Term.Cache): Rough_Classification = this match { case Equational(recursion) => Equational(recursion.cache(cache)) case _ => this } } case class Equational(recursion: Recursion) extends Rough_Classification case object Inductive extends Rough_Classification case object Co_Inductive extends Rough_Classification case object Unknown extends Rough_Classification val decode_rough_classification: XML.Decode.T[Rough_Classification] = { import XML.Decode._ variant(List( - { case (Nil, a) => Equational(decode_recursion(a)) case _ => ??? }, - { case (Nil, Nil) => Inductive case _ => ??? }, - { case (Nil, Nil) => Co_Inductive case _ => ??? }, - { case (Nil, Nil) => Unknown case _ => ??? })) + { case (Nil, a) => Equational(decode_recursion(a)) }, + { case (Nil, Nil) => Inductive }, + { case (Nil, Nil) => Co_Inductive }, + { case (Nil, Nil) => Unknown })) } sealed case class Spec_Rule( pos: Position.T, name: String, rough_classification: Rough_Classification, typargs: List[(String, Term.Sort)], args: List[(String, Term.Typ)], terms: List[(Term.Term, Term.Typ)], rules: List[Term.Term] ) { def id: Option[Long] = Position.Id.unapply(pos) def cache(cache: Term.Cache): Spec_Rule = Spec_Rule( cache.position(pos), cache.string(name), rough_classification.cache(cache), typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }), args.map({ case (name, typ) => (cache.string(name), cache.typ(typ)) }), terms.map({ case (term, typ) => (cache.term(term), cache.typ(typ)) }), rules.map(cache.term)) } def read_spec_rules(provider: Export.Provider): List[Spec_Rule] = { val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "spec_rules") val spec_rules = { import XML.Decode._ import Term_XML.Decode._ list( pair(properties, pair(string, pair(decode_rough_classification, pair(list(pair(string, sort)), pair(list(pair(string, typ)), pair(list(pair(term, typ)), list(term))))))))(body) } for ((pos, (name, (rough_classification, (typargs, (args, (terms, rules)))))) <- spec_rules) yield Spec_Rule(pos, name, rough_classification, typargs, args, terms, rules) } /* other entities */ sealed case class Other() extends Content[Other] { override def cache(cache: Term.Cache): Other = this } def read_others(provider: Export.Provider): Map[String, List[Entity[Other]]] = { val kinds = provider(Export.THEORY_PREFIX + "other_kinds") match { case Some(entry) => split_lines(entry.uncompressed.text) case None => Nil } val other = Other() def read_other(kind: String): List[Entity[Other]] = read_entities(provider, Export.THEORY_PREFIX + "other/" + kind, kind, _ => other) kinds.map(kind => kind -> read_other(kind)).toMap } } diff --git a/src/Pure/Tools/build_job.scala b/src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala +++ b/src/Pure/Tools/build_job.scala @@ -1,536 +1,536 @@ /* Title: Pure/Tools/build_job.scala Author: Makarius Build job running prover process, with rudimentary PIDE session. */ package isabelle import java.util.HashMap import scala.collection.mutable object Build_Job { /* theory markup/messages from database */ def read_theory( db_context: Sessions.Database_Context, session_hierarchy: List[String], theory: String, unicode_symbols: Boolean = false ): Option[Command] = { def read(name: String): Export.Entry = db_context.get_export(session_hierarchy, theory, name) def read_xml(name: String): XML.Body = YXML.parse_body( Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).uncompressed)), cache = db_context.cache) (read(Export.DOCUMENT_ID).text, split_lines(read(Export.FILES).text)) match { case (Value.Long(id), thy_file :: blobs_files) => val node_name = Resources.file_node(Path.explode(thy_file), theory = theory) val results = Command.Results.make( for (elem @ XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES)) yield i -> elem) val blobs = blobs_files.map { file => val path = Path.explode(file) val name = Resources.file_node(path) val src_path = File.relative_path(node_name.master_dir_path, path).getOrElse(path) Command.Blob(name, src_path, None) } val blobs_xml = for (i <- (1 to blobs.length).toList) yield read_xml(Export.MARKUP + i) val blobs_info = Command.Blobs_Info( for { (Command.Blob(name, src_path, _), xml) <- blobs zip blobs_xml } yield { val text = XML.content(xml) val chunk = Symbol.Text_Chunk(text) val digest = SHA1.digest(Symbol.encode(text)) Exn.Res(Command.Blob(name, src_path, Some((digest, chunk)))) }) val thy_xml = read_xml(Export.MARKUP) val thy_source = XML.content(thy_xml) val markups_index = Command.Markup_Index.markup :: blobs.map(Command.Markup_Index.blob) val markups = Command.Markups.make( for ((index, xml) <- markups_index.zip(thy_xml :: blobs_xml)) yield index -> Markup_Tree.from_XML(xml)) val command = Command.unparsed(thy_source, theory = true, id = id, node_name = node_name, blobs_info = blobs_info, results = results, markups = markups) Some(command) case _ => None } } /* print messages */ def print_log( options: Options, session_name: String, theories: List[String] = Nil, verbose: Boolean = false, progress: Progress = new Progress, margin: Double = Pretty.default_margin, breakgain: Double = Pretty.default_breakgain, metric: Pretty.Metric = Symbol.Metric, unicode_symbols: Boolean = false ): Unit = { val store = Sessions.store(options) val session = new Session(options, Resources.empty) using(store.open_database_context()) { db_context => val result = db_context.input_database(session_name) { (db, _) => val theories = store.read_theories(db, session_name) val errors = store.read_errors(db, session_name) store.read_build(db, session_name).map(info => (theories, errors, info.return_code)) } result match { case None => error("Missing build database for session " + quote(session_name)) case Some((used_theories, errors, rc)) => theories.filterNot(used_theories.toSet) match { case Nil => case bad => error("Unknown theories " + commas_quote(bad)) } val print_theories = if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet) for (thy <- print_theories) { val thy_heading = "\nTheory " + quote(thy) + ":" read_theory(db_context, List(session_name), thy, unicode_symbols = unicode_symbols) match { case None => progress.echo(thy_heading + " MISSING") case Some(command) => val snapshot = Document.State.init.snippet(command) val rendering = new Rendering(snapshot, options, session) val messages = rendering.text_messages(Text.Range.full) .filter(message => verbose || Protocol.is_exported(message.info)) if (messages.nonEmpty) { val line_document = Line.Document(command.source) progress.echo(thy_heading) for (Text.Info(range, elem) <- messages) { val line = line_document.position(range.start).line1 val pos = Position.Line_File(line, command.node_name.node) progress.echo( Protocol.message_text(elem, heading = true, pos = pos, margin = margin, breakgain = breakgain, metric = metric)) } } } } if (errors.nonEmpty) { val msg = Symbol.output(unicode_symbols, cat_lines(errors)) progress.echo("\nBuild errors:\n" + Output.error_message_text(msg)) } if (rc != Process_Result.RC.ok) { progress.echo("\n" + Process_Result.RC.print_long(rc)) } } } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("log", "print messages from build database", Scala_Project.here, { args => /* arguments */ var unicode_symbols = false var theories: List[String] = Nil var margin = Pretty.default_margin var options = Options.init() var verbose = false val getopts = Getopts(""" Usage: isabelle log [OPTIONS] SESSION Options are: -T NAME restrict to given theories (multiple options possible) -U output Unicode symbols -m MARGIN margin for pretty printing (default: """ + margin + """) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v print all messages, including information etc. Print messages from the build database of the given session, without any checks against current sources: results from a failed build can be printed as well. """, "T:" -> (arg => theories = theories ::: List(arg)), "U" -> (_ => unicode_symbols = true), "m:" -> (arg => margin = Value.Double.parse(arg)), "o:" -> (arg => options = options + arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) val session_name = more_args match { case List(session_name) => session_name case _ => getopts.usage() } val progress = new Console_Progress() print_log(options, session_name, theories = theories, verbose = verbose, margin = margin, progress = progress, unicode_symbols = unicode_symbols) }) } class Build_Job(progress: Progress, session_name: String, val info: Sessions.Info, deps: Sessions.Deps, store: Sessions.Store, do_store: Boolean, log: Logger, session_setup: (String, Session) => Unit, val numa_node: Option[Int], command_timings0: List[Properties.T] ) { val options: Options = NUMA.policy_options(info.options, numa_node) private val sessions_structure = deps.sessions_structure private val future_result: Future[Process_Result] = Future.thread("build", uninterruptible = true) { val parent = info.parent.getOrElse("") val base = deps(parent) val result_base = deps(session_name) val env = new HashMap(Isabelle_System.settings()) env.put("ISABELLE_ML_DEBUGGER", options.bool("ML_debugger").toString) val is_pure = Sessions.is_pure(session_name) val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil val eval_store = if (do_store) { (if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) ::: List("ML_Heap.save_child " + ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name)))) } else Nil val resources = new Resources(sessions_structure, base, log = log, command_timings = command_timings0) val session = new Session(options, resources) { override val cache: Term.Cache = store.cache override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = { result_base.load_commands.get(name.expand) match { case Some(spans) => val syntax = result_base.theory_syntax(name) Command.build_blobs_info(syntax, name, spans) case None => Command.Blobs_Info.none } } } object Build_Session_Errors { private val promise: Promise[List[String]] = Future.promise def result: Exn.Result[List[String]] = promise.join_result def cancel(): Unit = promise.cancel() def apply(errs: List[String]): Unit = { try { promise.fulfill(errs) } catch { case _: IllegalStateException => } } } val export_consumer = Export.consumer(store.open_database(session_name, output = true), store.cache, progress = progress) val stdout = new StringBuilder(1000) val stderr = new StringBuilder(1000) val command_timings = new mutable.ListBuffer[Properties.T] val theory_timings = new mutable.ListBuffer[Properties.T] val session_timings = new mutable.ListBuffer[Properties.T] val runtime_statistics = new mutable.ListBuffer[Properties.T] val task_statistics = new mutable.ListBuffer[Properties.T] def fun( name: String, acc: mutable.ListBuffer[Properties.T], unapply: Properties.T => Option[Properties.T] ): (String, Session.Protocol_Function) = { name -> ((msg: Prover.Protocol_Output) => unapply(msg.properties) match { case Some(props) => acc += props; true case _ => false }) } session.init_protocol_handler(new Session.Protocol_Handler { override def exit(): Unit = Build_Session_Errors.cancel() private def build_session_finished(msg: Prover.Protocol_Output): Boolean = { val (rc, errors) = try { val (rc, errs) = { import XML.Decode._ pair(int, list(x => x))(Symbol.decode_yxml(msg.text)) } val errors = for (err <- errs) yield { val prt = Protocol_Message.expose_no_reports(err) Pretty.string_of(prt, metric = Symbol.Metric) } (rc, errors) } catch { case ERROR(err) => (Process_Result.RC.failure, List(err)) } session.protocol_command("Prover.stop", rc.toString) Build_Session_Errors(errors) true } private def loading_theory(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Markup.Loading_Theory(Markup.Name(name)) => progress.theory(Progress.Theory(name, session = session_name)) false case _ => false } private def export_(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Protocol.Export(args) => export_consumer(session_name, args, msg.chunk) true case _ => false } - override val functions = + override val functions: Session.Protocol_Functions = List( Markup.Build_Session_Finished.name -> build_session_finished, Markup.Loading_Theory.name -> loading_theory, Markup.EXPORT -> export_, fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply), fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply), fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply)) }) session.command_timings += Session.Consumer("command_timings") { case Session.Command_Timing(props) => for { elapsed <- Markup.Elapsed.unapply(props) elapsed_time = Time.seconds(elapsed) if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold") } command_timings += props.filter(Markup.command_timing_property) } session.runtime_statistics += Session.Consumer("ML_statistics") { case Session.Runtime_Statistics(props) => runtime_statistics += props } session.finished_theories += Session.Consumer[Document.Snapshot]("finished_theories") { case snapshot => if (!progress.stopped) { val rendering = new Rendering(snapshot, options, session) def export_(name: String, xml: XML.Body, compress: Boolean = true): Unit = { if (!progress.stopped) { val theory_name = snapshot.node_name.theory val args = Protocol.Export.Args(theory_name = theory_name, name = name, compress = compress) val bytes = Bytes(Symbol.encode(YXML.string_of_body(xml))) if (!bytes.is_empty) export_consumer(session_name, args, bytes) } } def export_text(name: String, text: String, compress: Boolean = true): Unit = export_(name, List(XML.Text(text)), compress = compress) for (command <- snapshot.snippet_command) { export_text(Export.DOCUMENT_ID, command.id.toString, compress = false) } export_text(Export.FILES, cat_lines(snapshot.node_files.map(_.symbolic.node)), compress = false) for (((_, xml), i) <- snapshot.xml_markup_blobs().zipWithIndex) { export_(Export.MARKUP + (i + 1), xml) } export_(Export.MARKUP, snapshot.xml_markup()) export_(Export.MESSAGES, snapshot.messages.map(_._1)) val citations = Library.distinct(rendering.citations(Text.Range.full).map(_.info)) export_text(Export.DOCUMENT_CITATIONS, cat_lines(citations)) } } session.all_messages += Session.Consumer[Any]("build_session_output") { case msg: Prover.Output => val message = msg.message if (msg.is_system) resources.log(Protocol.message_text(message)) if (msg.is_stdout) { stdout ++= Symbol.encode(XML.content(message)) } else if (msg.is_stderr) { stderr ++= Symbol.encode(XML.content(message)) } else if (msg.is_exit) { val err = "Prover terminated" + (msg.properties match { case Markup.Process_Result(result) => ": " + result.print_rc case _ => "" }) Build_Session_Errors(List(err)) } case _ => } session_setup(session_name, session) val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store) val process = Isabelle_Process.start(session, options, sessions_structure, store, logic = parent, raw_ml_system = is_pure, use_prelude = use_prelude, eval_main = eval_main, cwd = info.dir.file, env = env) val build_errors = Isabelle_Thread.interrupt_handler(_ => process.terminate()) { Exn.capture { process.await_startup() } match { case Exn.Res(_) => val resources_yxml = resources.init_session_yxml val encode_options: XML.Encode.T[Options] = options => session.prover_options(options).encode val args_yxml = YXML.string_of_body( { import XML.Encode._ pair(string, list(pair(encode_options, list(pair(string, properties)))))( (session_name, info.theories)) }) session.protocol_command("build_session", resources_yxml, args_yxml) Build_Session_Errors.result case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn))) } } val process_result = Isabelle_Thread.interrupt_handler(_ => process.terminate()) { process.await_shutdown() } session.stop() val export_errors = export_consumer.shutdown(close = true).map(Output.error_message_text) val (document_output, document_errors) = try { if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) { using(store.open_database_context()) { db_context => val documents = Document_Build.build_documents( Document_Build.context(session_name, deps, db_context, progress = progress), output_sources = info.document_output, output_pdf = info.document_output) db_context.output_database(session_name)(db => documents.foreach(_.write(db, session_name))) (documents.flatMap(_.log_lines), Nil) } } else (Nil, Nil) } catch { case exn: Document_Build.Build_Error => (exn.log_lines, List(exn.message)) case Exn.Interrupt.ERROR(msg) => (Nil, List(msg)) } val result = { val theory_timing = - theory_timings.iterator.map( + theory_timings.iterator.flatMap( { - case props @ Markup.Name(name) => name -> props - case _ => ??? + case props @ Markup.Name(name) => Some(name -> props) + case _ => None }).toMap val used_theory_timings = for { (name, _) <- deps(session_name).used_theories } yield theory_timing.getOrElse(name.theory, Markup.Name(name.theory)) val more_output = Library.trim_line(stdout.toString) :: command_timings.toList.map(Protocol.Command_Timing_Marker.apply) ::: used_theory_timings.map(Protocol.Theory_Timing_Marker.apply) ::: session_timings.toList.map(Protocol.Session_Timing_Marker.apply) ::: runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) ::: task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) ::: document_output process_result.output(more_output) .error(Library.trim_line(stderr.toString)) .errors_rc(export_errors ::: document_errors) } build_errors match { case Exn.Res(build_errs) => val errs = build_errs ::: document_errors if (errs.nonEmpty) { result.error_rc.output( errs.flatMap(s => split_lines(Output.error_message_text(s))) ::: errs.map(Protocol.Error_Message_Marker.apply)) } else if (progress.stopped && result.ok) result.copy(rc = Process_Result.RC.interrupt) else result case Exn.Exn(Exn.Interrupt()) => if (result.ok) result.copy(rc = Process_Result.RC.interrupt) else result case Exn.Exn(exn) => throw exn } } def terminate(): Unit = future_result.cancel() def is_finished: Boolean = future_result.is_finished private val timeout_request: Option[Event_Timer.Request] = { if (info.timeout_ignored) None else Some(Event_Timer.request(Time.now() + info.timeout) { terminate() }) } def join: (Process_Result, Option[String]) = { val result1 = future_result.join val was_timeout = timeout_request match { case None => false case Some(request) => !request.cancel() } val result2 = if (result1.ok) result1 else if (was_timeout) result1.error(Output.error_message_text("Timeout")).timeout_rc else if (result1.interrupted) result1.error(Output.error_message_text("Interrupt")) else result1 val heap_digest = if (result2.ok && do_store && store.output_heap(session_name).is_file) Some(Sessions.write_heap_digest(store.output_heap(session_name))) else None (result2, heap_digest) } } diff --git a/src/Pure/Tools/debugger.scala b/src/Pure/Tools/debugger.scala --- a/src/Pure/Tools/debugger.scala +++ b/src/Pure/Tools/debugger.scala @@ -1,273 +1,273 @@ /* Title: Pure/Tools/debugger.scala Author: Makarius Interactive debugger for Isabelle/ML. */ package isabelle import scala.collection.immutable.SortedMap object Debugger { /* thread context */ case object Update sealed case class Debug_State(pos: Position.T, function: String) type Threads = SortedMap[String, List[Debug_State]] sealed case class Context(thread_name: String, debug_states: List[Debug_State], index: Int = 0) { def size: Int = debug_states.length + 1 def reset: Context = copy(index = 0) def select(i: Int): Context = copy(index = i + 1) def thread_state: Option[Debug_State] = debug_states.headOption def stack_state: Option[Debug_State] = if (1 <= index && index <= debug_states.length) Some(debug_states(index - 1)) else None def debug_index: Option[Int] = if (stack_state.isDefined) Some(index - 1) else if (debug_states.nonEmpty) Some(0) else None def debug_state: Option[Debug_State] = stack_state orElse thread_state def debug_position: Option[Position.T] = debug_state.map(_.pos) override def toString: String = stack_state match { case None => thread_name case Some(d) => d.function } } /* debugger state */ sealed case class State( active: Int = 0, // active views break: Boolean = false, // break at next possible breakpoint active_breakpoints: Set[Long] = Set.empty, // explicit breakpoint state threads: Threads = SortedMap.empty, // thread name ~> stack of debug states focus: Map[String, Context] = Map.empty, // thread name ~> focus output: Map[String, Command.Results] = Map.empty // thread name ~> output messages ) { def set_break(b: Boolean): State = copy(break = b) def is_active: Boolean = active > 0 def inc_active: State = copy(active = active + 1) def dec_active: State = copy(active = active - 1) def toggle_breakpoint(breakpoint: Long): (Boolean, State) = { val active_breakpoints1 = if (active_breakpoints(breakpoint)) active_breakpoints - breakpoint else active_breakpoints + breakpoint (active_breakpoints1(breakpoint), copy(active_breakpoints = active_breakpoints1)) } def get_thread(thread_name: String): List[Debug_State] = threads.getOrElse(thread_name, Nil) def update_thread(thread_name: String, debug_states: List[Debug_State]): State = { val threads1 = if (debug_states.nonEmpty) threads + (thread_name -> debug_states) else threads - thread_name val focus1 = focus.get(thread_name) match { case Some(c) if debug_states.nonEmpty => focus + (thread_name -> Context(thread_name, debug_states)) case _ => focus - thread_name } copy(threads = threads1, focus = focus1) } def set_focus(c: Context): State = copy(focus = focus + (c.thread_name -> c)) def get_output(thread_name: String): Command.Results = output.getOrElse(thread_name, Command.Results.empty) def add_output(thread_name: String, entry: Command.Results.Entry): State = copy(output = output + (thread_name -> (get_output(thread_name) + entry))) def clear_output(thread_name: String): State = copy(output = output - thread_name) } /* protocol handler */ class Handler(session: Session) extends Session.Protocol_Handler { val debugger: Debugger = new Debugger(session) private def debugger_state(msg: Prover.Protocol_Output): Boolean = { msg.properties match { case Markup.Debugger_State(thread_name) => val msg_body = Symbol.decode_yxml_failsafe(msg.text) val debug_states = { import XML.Decode._ list(pair(properties, string))(msg_body).map({ case (pos, function) => Debug_State(pos, function) }) } debugger.update_thread(thread_name, debug_states) true case _ => false } } private def debugger_output(msg: Prover.Protocol_Output): Boolean = { msg.properties match { case Markup.Debugger_Output(thread_name) => Symbol.decode_yxml_failsafe(msg.text) match { case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) => val message = XML.Elem(Markup(Markup.message(name), props), body) debugger.add_output(thread_name, i -> session.cache.elem(message)) true case _ => false } case _ => false } } - override val functions = + override val functions: Session.Protocol_Functions = List( Markup.DEBUGGER_STATE -> debugger_state, Markup.DEBUGGER_OUTPUT -> debugger_output) } } class Debugger private(session: Session) { /* debugger state */ private val state = Synchronized(Debugger.State()) private val delay_update = Delay.first(session.output_delay) { session.debugger_updates.post(Debugger.Update) } /* protocol commands */ def update_thread(thread_name: String, debug_states: List[Debugger.Debug_State]): Unit = { state.change(_.update_thread(thread_name, debug_states)) delay_update.invoke() } def add_output(thread_name: String, entry: Command.Results.Entry): Unit = { state.change(_.add_output(thread_name, entry)) delay_update.invoke() } def is_active(): Boolean = session.is_ready && state.value.is_active def ready(): Unit = { if (is_active()) session.protocol_command("Debugger.init") } def init(): Unit = state.change { st => val st1 = st.inc_active if (session.is_ready && !st.is_active && st1.is_active) session.protocol_command("Debugger.init") st1 } def exit(): Unit = state.change { st => val st1 = st.dec_active if (session.is_ready && st.is_active && !st1.is_active) session.protocol_command("Debugger.exit") st1 } def is_break(): Boolean = state.value.break def set_break(b: Boolean): Unit = { state.change { st => val st1 = st.set_break(b) session.protocol_command("Debugger.break", b.toString) st1 } delay_update.invoke() } def active_breakpoint_state(breakpoint: Long): Option[Boolean] = { val st = state.value if (st.is_active) Some(st.active_breakpoints(breakpoint)) else None } def breakpoint_state(breakpoint: Long): Boolean = state.value.active_breakpoints(breakpoint) def toggle_breakpoint(command: Command, breakpoint: Long): Unit = { state.change { st => val (breakpoint_state, st1) = st.toggle_breakpoint(breakpoint) session.protocol_command( "Debugger.breakpoint", Symbol.encode(command.node_name.node), Document_ID(command.id), Value.Long(breakpoint), Value.Boolean(breakpoint_state)) st1 } } def status(focus: Option[Debugger.Context]): (Debugger.Threads, List[XML.Tree]) = { val st = state.value val output = focus match { case None => Nil case Some(c) => (for { (thread_name, results) <- st.output if thread_name == c.thread_name (_, tree) <- results.iterator } yield tree).toList } (st.threads, output) } def focus(): List[Debugger.Context] = state.value.focus.toList.map(_._2) def set_focus(c: Debugger.Context): Unit = { state.change(_.set_focus(c)) delay_update.invoke() } def input(thread_name: String, msg: String*): Unit = session.protocol_command_args("Debugger.input", thread_name :: msg.toList) def continue(thread_name: String): Unit = input(thread_name, "continue") def step(thread_name: String): Unit = input(thread_name, "step") def step_over(thread_name: String): Unit = input(thread_name, "step_over") def step_out(thread_name: String): Unit = input(thread_name, "step_out") def clear_output(thread_name: String): Unit = { state.change(_.clear_output(thread_name)) delay_update.invoke() } def eval(c: Debugger.Context, SML: Boolean, context: String, expression: String): Unit = { state.change { st => input(c.thread_name, "eval", c.debug_index.getOrElse(0).toString, SML.toString, Symbol.encode(context), Symbol.encode(expression)) st.clear_output(c.thread_name) } delay_update.invoke() } def print_vals(c: Debugger.Context, SML: Boolean, context: String): Unit = { require(c.debug_index.isDefined) state.change { st => input(c.thread_name, "print_vals", c.debug_index.getOrElse(0).toString, SML.toString, Symbol.encode(context)) st.clear_output(c.thread_name) } delay_update.invoke() } } diff --git a/src/Pure/Tools/print_operation.scala b/src/Pure/Tools/print_operation.scala --- a/src/Pure/Tools/print_operation.scala +++ b/src/Pure/Tools/print_operation.scala @@ -1,39 +1,40 @@ /* Title: Pure/Tools/print_operation.scala Author: Makarius Print operations as asynchronous query. */ package isabelle object Print_Operation { def get(session: Session): List[(String, String)] = session.get_protocol_handler(classOf[Handler]) match { case Some(h) => h.get case _ => Nil } /* protocol handler */ class Handler extends Session.Protocol_Handler { private val print_operations = Synchronized[List[(String, String)]](Nil) def get: List[(String, String)] = print_operations.value override def init(session: Session): Unit = session.protocol_command(Markup.PRINT_OPERATIONS) private def put(msg: Prover.Protocol_Output): Boolean = { val ops = { import XML.Decode._ list(pair(string, string))(Symbol.decode_yxml(msg.text)) } print_operations.change(_ => ops) true } - override val functions = List(Markup.PRINT_OPERATIONS -> put) + override val functions: Session.Protocol_Functions = + List(Markup.PRINT_OPERATIONS -> put) } } diff --git a/src/Pure/Tools/simplifier_trace.scala b/src/Pure/Tools/simplifier_trace.scala --- a/src/Pure/Tools/simplifier_trace.scala +++ b/src/Pure/Tools/simplifier_trace.scala @@ -1,318 +1,319 @@ /* Title: Pure/Tools/simplifier_trace.scala Author: Lars Hupel Interactive Simplifier trace. */ package isabelle import scala.annotation.tailrec import scala.collection.immutable.SortedMap object Simplifier_Trace { /* trace items from the prover */ val TEXT = "text" val Text = new Properties.String(TEXT) val PARENT = "parent" val Parent = new Properties.Long(PARENT) val SUCCESS = "success" val Success = new Properties.Boolean(SUCCESS) val MEMORY = "memory" val Memory = new Properties.Boolean(MEMORY) object Item { case class Data( serial: Long, markup: String, text: String, parent: Long, props: Properties.T, content: XML.Body ) { def memory: Boolean = Memory.unapply(props) getOrElse true } def unapply(tree: XML.Tree): Option[(String, Data)] = tree match { case XML.Elem(Markup(Markup.RESULT, Markup.Serial(serial)), List(XML.Elem(Markup(markup, props), content))) if markup.startsWith("simp_trace_") => // FIXME proper comparison of string constants (props, props) match { case (Text(text), Parent(parent)) => Some((markup, Data(serial, markup, text, parent, props, content))) case _ => None } case _ => None } } /* replies to the prover */ case class Answer private[Simplifier_Trace](val name: String, val string: String) object Answer { object step { val skip = Answer("skip", "Skip") val continue = Answer("continue", "Continue") val continue_trace = Answer("continue_trace", "Continue (with full trace)") val continue_passive = Answer("continue_passive", "Continue (without asking)") val continue_disable = Answer("continue_disable", "Continue (without any trace)") val all = List(continue, continue_trace, continue_passive, continue_disable, skip) } object hint_fail { val exit = Answer("exit", "Exit") val redo = Answer("redo", "Redo") val all = List(redo, exit) } } val all_answers: List[Answer] = Answer.step.all ::: Answer.hint_fail.all /* GUI interaction */ case object Event /* manager thread */ private case class Handle_Results( session: Session, id: Document_ID.Command, results: Command.Results, slot: Promise[Context]) private case class Generate_Trace(results: Command.Results, slot: Promise[Trace]) private case class Cancel(serial: Long) private object Clear_Memory case class Reply(session: Session, serial: Long, answer: Answer) case class Question(data: Item.Data, answers: List[Answer]) case class Context( last_serial: Long = 0L, questions: SortedMap[Long, Question] = SortedMap.empty ) { def +(q: Question): Context = copy(questions = questions + ((q.data.serial, q))) def -(s: Long): Context = copy(questions = questions - s) def with_serial(s: Long): Context = copy(last_serial = Math.max(last_serial, s)) } case class Trace(entries: List[Item.Data]) case class Index(text: String, content: XML.Body) object Index { def of_data(data: Item.Data): Index = Index(data.text, data.content) } def handle_results( session: Session, id: Document_ID.Command, results: Command.Results ): Context = { val slot = Future.promise[Context] the_manager(session).send(Handle_Results(session, id, results, slot)) slot.join } def generate_trace(session: Session, results: Command.Results): Trace = { val slot = Future.promise[Trace] the_manager(session).send(Generate_Trace(results, slot)) slot.join } def clear_memory(session: Session): Unit = the_manager(session).send(Clear_Memory) def send_reply(session: Session, serial: Long, answer: Answer): Unit = the_manager(session).send(Reply(session, serial, answer)) def make_manager: Consumer_Thread[Any] = { var contexts = Map.empty[Document_ID.Command, Context] var memory_children = Map.empty[Long, Set[Long]] var memory = Map.empty[Index, Answer] def find_question(serial: Long): Option[(Document_ID.Command, Question)] = contexts collectFirst { case (id, context) if context.questions contains serial => (id, context.questions(serial)) } def do_cancel(serial: Long, id: Document_ID.Command): Unit = { // To save memory, we could try to remove empty contexts at this point. // However, if a new serial gets attached to the same command_id after we deleted // its context, its last_serial counter will start at 0 again, and we'll think the // old serials are actually new contexts += (id -> (contexts(id) - serial)) } def do_reply(session: Session, serial: Long, answer: Answer): Unit = { session.protocol_command( "Simplifier_Trace.reply", Value.Long(serial), answer.name) } Consumer_Thread.fork[Any]("Simplifier_Trace.manager", daemon = true)( consume = { (arg: Any) => arg match { case Handle_Results(session, id, results, slot) => var new_context = contexts.getOrElse(id, Context()) var new_serial = new_context.last_serial for ((serial, result) <- results.iterator if serial > new_context.last_serial) { result match { case Item(markup, data) => memory_children += (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial)) markup match { case Markup.SIMP_TRACE_STEP => val index = Index.of_data(data) memory.get(index) match { case Some(answer) if data.memory => do_reply(session, serial, answer) case _ => new_context += Question(data, Answer.step.all) } case Markup.SIMP_TRACE_HINT => data.props match { case Success(false) => results.get(data.parent) match { case Some(Item(Markup.SIMP_TRACE_STEP, _)) => new_context += Question(data, Answer.hint_fail.all) case _ => // unknown, better send a default reply do_reply(session, data.serial, Answer.hint_fail.exit) } case _ => } case Markup.SIMP_TRACE_IGNORE => // At this point, we know that the parent of this 'IGNORE' entry is a 'STEP' // entry, and that that 'STEP' entry is about to be replayed. Hence, we need // to selectively purge the replies which have been memorized, going down from // the parent to all leaves. @tailrec def purge(queue: Vector[Long]): Unit = queue match { case s +: rest => for (Item(Markup.SIMP_TRACE_STEP, data) <- results.get(s)) memory -= Index.of_data(data) val children = memory_children.getOrElse(s, Set.empty) memory_children -= s purge(rest ++ children.toVector) case _ => } purge(Vector(data.parent)) case _ => } case _ => } new_serial = serial } new_context = new_context.with_serial(new_serial) contexts += (id -> new_context) slot.fulfill(new_context) case Generate_Trace(results, slot) => // Since there are potentially lots of trace messages, we do not cache them here again. // Instead, everytime the trace is being requested, we re-assemble it based on the // current results. val items = results.iterator.collect { case (_, Item(_, data)) => data }.toList slot.fulfill(Trace(items)) case Cancel(serial) => find_question(serial) match { case Some((id, _)) => do_cancel(serial, id) case None => } case Clear_Memory => memory_children = Map.empty memory = Map.empty case Reply(session, serial, answer) => find_question(serial) match { case Some((id, Question(data, _))) => if (data.markup == Markup.SIMP_TRACE_STEP && data.memory) { val index = Index.of_data(data) memory += (index -> answer) } do_cancel(serial, id) case None => Output.warning("send_reply: unknown serial " + serial) } do_reply(session, serial, answer) session.trace_events.post(Event) } true }, finish = () => contexts = Map.empty ) } private val managers = Synchronized(Map.empty[Session, Consumer_Thread[Any]]) def the_manager(session: Session): Consumer_Thread[Any] = managers.value.get(session) match { case Some(thread) if thread.is_active() => thread case _ => error("Bad Simplifier_Trace.manager thread") } /* protocol handler */ class Handler extends Session.Protocol_Handler { private var the_session: Session = null override def init(session: Session): Unit = { try { the_manager(session) } catch { case ERROR(_) => managers.change(map => map + (session -> make_manager)) } the_session = session } override def exit(): Unit = { val session = the_session if (session != null) { val manager = the_manager(session) manager.send(Clear_Memory) manager.shutdown() managers.change(map => map - session) the_session = null } } private def cancel(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Markup.Simp_Trace_Cancel(serial) => the_manager(the_session).send(Cancel(serial)) true case _ => false } - override val functions = List(Markup.SIMP_TRACE_CANCEL -> cancel) + override val functions: Session.Protocol_Functions = + List(Markup.SIMP_TRACE_CANCEL -> cancel) } } diff --git a/src/Pure/term_xml.scala b/src/Pure/term_xml.scala --- a/src/Pure/term_xml.scala +++ b/src/Pure/term_xml.scala @@ -1,101 +1,101 @@ /* Title: Pure/term_xml.scala Author: Makarius XML data representation of lambda terms. */ package isabelle object Term_XML { import Term._ object Encode { import XML.Encode._ val indexname: P[Indexname] = { case Indexname(a, 0) => List(a) case Indexname(a, b) => List(a, int_atom(b)) } val sort: T[Sort] = list(string) def typ: T[Typ] = variant[Typ](List( { case Type(a, b) => (List(a), list(typ)(b)) }, { case TFree(a, b) => (List(a), sort(b)) }, { case TVar(a, b) => (indexname(a), sort(b)) })) val typ_body: T[Typ] = (t: Typ) => if (t == dummyT) Nil else typ(t) def term: T[Term] = variant[Term](List( { case Const(a, b) => (List(a), list(typ)(b)) }, { case Free(a, b) => (List(a), typ_body(b)) }, { case Var(a, b) => (indexname(a), typ_body(b)) }, { case Bound(a) => (Nil, int(a)) }, { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) }, { case App(a, b) => (Nil, pair(term, term)(a, b)) })) } object Decode { import XML.Decode._ val indexname: P[Indexname] = { case List(a) => Indexname(a, 0) case List(a, b) => Indexname(a, int_atom(b)) } val sort: T[Sort] = list(string) def typ: T[Typ] = variant[Typ](List( - { case (List(a), b) => Type(a, list(typ)(b)) case _ => ??? }, - { case (List(a), b) => TFree(a, sort(b)) case _ => ??? }, + { case (List(a), b) => Type(a, list(typ)(b)) }, + { case (List(a), b) => TFree(a, sort(b)) }, { case (a, b) => TVar(indexname(a), sort(b)) })) val typ_body: T[Typ] = { case Nil => dummyT case body => typ(body) } def term: T[Term] = variant[Term](List( - { case (List(a), b) => Const(a, list(typ)(b)) case _ => ??? }, - { case (List(a), b) => Free(a, typ_body(b)) case _ => ??? }, + { case (List(a), b) => Const(a, list(typ)(b)) }, + { case (List(a), b) => Free(a, typ_body(b)) }, { case (a, b) => Var(indexname(a), typ_body(b)) }, - { case (Nil, a) => Bound(int(a)) case _ => ??? }, - { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) case _ => ??? }, - { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) case _ => ??? })) + { case (Nil, a) => Bound(int(a)) }, + { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) }, + { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) })) def term_env(env: Map[String, Typ]): T[Term] = { def env_type(x: String, t: Typ): Typ = if (t == dummyT && env.isDefinedAt(x)) env(x) else t def term: T[Term] = variant[Term](List( - { case (List(a), b) => Const(a, list(typ)(b)) case _ => ??? }, - { case (List(a), b) => Free(a, env_type(a, typ_body(b))) case _ => ??? }, + { case (List(a), b) => Const(a, list(typ)(b)) }, + { case (List(a), b) => Free(a, env_type(a, typ_body(b))) }, { case (a, b) => Var(indexname(a), typ_body(b)) }, - { case (Nil, a) => Bound(int(a)) case _ => ??? }, - { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) case _ => ??? }, - { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) case _ => ??? })) + { case (Nil, a) => Bound(int(a)) }, + { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) }, + { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) })) term } def proof_env(env: Map[String, Typ]): T[Proof] = { val term = term_env(env) def proof: T[Proof] = variant[Proof](List( - { case (Nil, Nil) => MinProof case _ => ??? }, - { case (Nil, a) => PBound(int(a)) case _ => ??? }, - { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) case _ => ??? }, - { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) case _ => ??? }, - { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) case _ => ??? }, - { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) case _ => ??? }, - { case (Nil, a) => Hyp(term(a)) case _ => ??? }, - { case (List(a), b) => PAxm(a, list(typ)(b)) case _ => ??? }, - { case (List(a), b) => PClass(typ(b), a) case _ => ??? }, - { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) case _ => ??? }, - { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) case _ => ??? })) + { case (Nil, Nil) => MinProof }, + { case (Nil, a) => PBound(int(a)) }, + { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) }, + { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) }, + { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) }, + { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) }, + { case (Nil, a) => Hyp(term(a)) }, + { case (List(a), b) => PAxm(a, list(typ)(b)) }, + { case (List(a), b) => PClass(typ(b), a) }, + { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) }, + { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) })) proof } val proof: T[Proof] = proof_env(Map.empty) } } diff --git a/src/Tools/Graphview/layout.scala b/src/Tools/Graphview/layout.scala --- a/src/Tools/Graphview/layout.scala +++ b/src/Tools/Graphview/layout.scala @@ -1,422 +1,422 @@ /* Title: Tools/Graphview/layout.scala Author: Markus Kaiser, TU Muenchen Author: Makarius DAG layout according to: Georg Sander, "Graph Layout through the VCG Tool", in: Graph Drawing, DIMACS International Workshop (GD'94), Springer LNCS 894, 1995. https://doi.org/10.1007/3-540-58950-3_371 ftp://ftp.cs.uni-sb.de/pub/graphics/vcg/doc/tr-A03-94.ps.gz */ package isabelle.graphview import isabelle._ object Layout { /* graph structure */ object Vertex { object Ordering extends scala.math.Ordering[Vertex] { def compare(v1: Vertex, v2: Vertex): Int = (v1, v2) match { case (Node(a), Node(b)) => Graph_Display.Node.Ordering.compare(a, b) case (Dummy(a1, a2, i), Dummy(b1, b2, j)) => Graph_Display.Node.Ordering.compare(a1, b1) match { case 0 => Graph_Display.Node.Ordering.compare(a2, b2) match { case 0 => i compare j case ord => ord } case ord => ord } case (Node(a), Dummy(b, _, _)) => Graph_Display.Node.Ordering.compare(a, b) match { case 0 => -1 case ord => ord } case (Dummy(a, _, _), Node(b)) => Graph_Display.Node.Ordering.compare(a, b) match { case 0 => 1 case ord => ord } } } } sealed abstract class Vertex case class Node(node: Graph_Display.Node) extends Vertex case class Dummy(node1: Graph_Display.Node, node2: Graph_Display.Node, index: Int) extends Vertex sealed case class Info( x: Double, y: Double, width2: Double, height2: Double, lines: List[String] ) { def left: Double = x - width2 def right: Double = x + width2 def width: Double = 2 * width2 def height: Double = 2 * height2 } type Graph = isabelle.Graph[Vertex, Info] def make_graph(entries: List[((Vertex, Info), List[Vertex])]): Graph = isabelle.Graph.make(entries)(Vertex.Ordering) val empty_graph: Graph = make_graph(Nil) /* vertex x coordinate */ private def vertex_left(graph: Graph, v: Vertex) = graph.get_node(v).left private def vertex_right(graph: Graph, v: Vertex) = graph.get_node(v).right private def move_vertex(graph: Graph, v: Vertex, dx: Double): Graph = if (dx == 0.0) graph else graph.map_node(v, info => info.copy(x = info.x + dx)) /* layout */ val empty: Layout = new Layout(Metrics.default, Graph_Display.empty_graph, empty_graph) private type Levels = Map[Vertex, Int] private val empty_levels: Levels = Map.empty def make( options: Options, metrics: Metrics, node_text: (Graph_Display.Node, XML.Body) => String, input_graph: Graph_Display.Graph ): Layout = { if (input_graph.is_empty) empty else { /* initial graph */ val initial_graph = make_graph( input_graph.iterator.map( { case (a, (content, (_, bs))) => val lines = split_lines(node_text(a, content)) val w2 = metrics.node_width2(lines) val h2 = metrics.node_height2(lines.length) ((Node(a), Info(0.0, 0.0, w2, h2, lines)), bs.toList.map(Node.apply)) }).toList) val initial_levels: Levels = initial_graph.topological_order.foldLeft(empty_levels) { case (levels, vertex) => val level = 1 + initial_graph.imm_preds(vertex).foldLeft(-1) { case (m, v) => m max levels(v) } levels + (vertex -> level) } /* graph with dummies */ val dummy_info = Info(0.0, 0.0, metrics.dummy_size2, metrics.dummy_size2, Nil) val (dummy_graph, dummy_levels) = input_graph.edges_iterator.foldLeft((initial_graph, initial_levels)) { case ((graph, levels), (node1, node2)) => val v1 = Node(node1); val l1 = levels(v1) val v2 = Node(node2); val l2 = levels(v2) if (l2 - l1 <= 1) (graph, levels) else { val dummies_levels = (for { (l, i) <- ((l1 + 1) until l2).iterator.zipWithIndex } yield (Dummy(node1, node2, i), l)).toList val dummies = dummies_levels.map(_._1) val levels1 = dummies_levels.foldLeft(levels)(_ + _) val graph1 = - (v1 :: dummies ::: List(v2)).sliding(2).map(_.toList). - foldLeft(dummies.foldLeft(graph)(_.new_node(_, dummy_info)).del_edge(v1, v2)) { - case (g, List(a, b)) => g.add_edge(a, b) - case _ => ??? + (v1 :: dummies ::: List(v2)).sliding(2) + .foldLeft(dummies.foldLeft(graph)(_.new_node(_, dummy_info)).del_edge(v1, v2)) { + case (g, Seq(a, b)) => g.add_edge(a, b) + case (g, _) => g } (graph1, levels1) } } /* minimize edge crossings and initial coordinates */ val levels = minimize_crossings(options, dummy_graph, level_list(dummy_levels)) val levels_graph: Graph = levels.foldLeft((dummy_graph, 0.0)) { case ((graph, y), level) => val num_lines = level.foldLeft(0) { case (n, v) => n max graph.get_node(v).lines.length } val num_edges = level.foldLeft(0) { case (n, v) => n + graph.imm_succs(v).size } val y1 = y + metrics.node_height2(num_lines) val graph1 = level.foldLeft((graph, 0.0)) { case ((g, x), v) => val info = g.get_node(v) val g1 = g.map_node(v, _ => info.copy(x = x + info.width2, y = y1)) val x1 = x + info.width + metrics.gap (g1, x1) }._1 val y2 = y1 + metrics.level_height2(num_lines, num_edges) (graph1, y2) }._1 /* pendulum/rubberband layout */ val output_graph = rubberband(options, metrics, levels, pendulum(options, metrics, levels, levels_graph)) new Layout(metrics, input_graph, output_graph) } } /** edge crossings **/ private type Level = List[Vertex] private def minimize_crossings( options: Options, graph: Graph, levels: List[Level] ): List[Level] = { def resort(parent: Level, child: Level, top_down: Boolean): Level = child.map({ v => val ps = if (top_down) graph.imm_preds(v) else graph.imm_succs(v) val weight = ps.foldLeft(0.0) { case (w, p) => w + (0 max parent.indexOf(p)) } / (ps.size max 1) (v, weight) }).sortBy(_._2).map(_._1) (1 to (2 * options.int("graphview_iterations_minimize_crossings"))). foldLeft((levels, count_crossings(graph, levels))) { case ((old_levels, old_crossings), iteration) => val top_down = (iteration % 2 == 1) val new_levels = if (top_down) { old_levels.tail.foldLeft(List(old_levels.head)) { case (tops, bot) => resort(tops.head, bot, top_down) :: tops }.reverse } else { val rev_old_levels = old_levels.reverse rev_old_levels.tail.foldLeft(List(rev_old_levels.head)) { case (bots, top) => resort(bots.head, top, top_down) :: bots } } val new_crossings = count_crossings(graph, new_levels) if (new_crossings < old_crossings) (new_levels, new_crossings) else (old_levels, old_crossings) }._1 } private def level_list(levels: Levels): List[Level] = { val max_lev = levels.foldLeft(-1) { case (m, (_, l)) => m max l } val buckets = new Array[Level](max_lev + 1) for (l <- 0 to max_lev) { buckets(l) = Nil } for ((v, l) <- levels) { buckets(l) = v :: buckets(l) } buckets.iterator.map(_.sorted(Vertex.Ordering)).toList } private def count_crossings(graph: Graph, levels: List[Level]): Int = - levels.iterator.sliding(2).map(_.toList).map { - case List(top, bot) => + levels.iterator.sliding(2).map { + case Seq(top, bot) => top.iterator.zipWithIndex.map { case (outer_parent, outer_parent_index) => graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_)).map(outer_child => (0 until outer_parent_index).iterator.map(inner_parent => graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_)) .count(inner_child => outer_child < inner_child)).sum).sum }.sum case _ => 0 }.sum /** pendulum method **/ /*This is an auxiliary class which is used by the layout algorithm when calculating coordinates with the "pendulum method". A "region" is a group of vertices which "stick together".*/ private class Region(val content: List[Vertex]) { def distance(metrics: Metrics, graph: Graph, that: Region): Double = vertex_left(graph, that.content.head) - vertex_right(graph, this.content.last) - metrics.gap def deflection(graph: Graph, top_down: Boolean): Double = ((for (a <- content.iterator) yield { val x = graph.get_node(a).x val bs = if (top_down) graph.imm_preds(a) else graph.imm_succs(a) bs.iterator.map(graph.get_node(_).x - x).sum / (bs.size max 1) }).sum / content.length).round.toDouble def move(graph: Graph, dx: Double): Graph = if (dx == 0.0) graph else content.foldLeft(graph)(move_vertex(_, _, dx)) def combine(that: Region): Region = new Region(content ::: that.content) } private def pendulum( options: Options, metrics: Metrics, levels: List[Level], levels_graph: Graph ): Graph = { def combine_regions(graph: Graph, top_down: Boolean, level: List[Region]): List[Region] = level match { case r1 :: rest => val rest1 = combine_regions(graph, top_down, rest) rest1 match { case r2 :: rest2 => val d1 = r1.deflection(graph, top_down) val d2 = r2.deflection(graph, top_down) if (// Do regions touch? r1.distance(metrics, graph, r2) <= 0.0 && // Do they influence each other? (d1 <= 0.0 && d2 < d1 || d2 > 0.0 && d1 > d2 || d1 > 0.0 && d2 < 0.0)) r1.combine(r2) :: rest2 else r1 :: rest1 case _ => r1 :: rest1 } case _ => level } def deflect(level: List[Region], top_down: Boolean, graph: Graph): (Graph, Boolean) = { level.indices.foldLeft((graph, false)) { case ((graph, moved), i) => val r = level(i) val d = r.deflection(graph, top_down) val dx = if (d < 0.0 && i > 0) { - (level(i - 1).distance(metrics, graph, r) min (- d)) } else if (d >= 0.0 && i < level.length - 1) { r.distance(metrics, graph, level(i + 1)) min d } else d (r.move(graph, dx), moved || d != 0.0) } } val initial_regions = levels.map(level => level.map(l => new Region(List(l)))) (1 to (2 * options.int("graphview_iterations_pendulum"))). foldLeft((levels_graph, initial_regions, true)) { case ((graph, regions, moved), iteration) => val top_down = (iteration % 2 == 1) if (moved) { val (graph1, regions1, moved1) = (if (top_down) regions else regions.reverse). foldLeft((graph, List.empty[List[Region]], false)) { case ((graph, tops, moved), bot) => val bot1 = combine_regions(graph, top_down, bot) val (graph1, moved1) = deflect(bot1, top_down, graph) (graph1, bot1 :: tops, moved || moved1) } (graph1, regions1.reverse, moved1) } else (graph, regions, moved) }._1 } /** rubberband method **/ private def force_weight(graph: Graph, v: Vertex): Double = { val preds = graph.imm_preds(v) val succs = graph.imm_succs(v) val n = preds.size + succs.size if (n == 0) 0.0 else { val x = graph.get_node(v).x ((preds.iterator ++ succs.iterator).map(w => graph.get_node(w).x - x)).sum / n } } private def rubberband( options: Options, metrics: Metrics, levels: List[Level], graph: Graph ): Graph = { val gap = metrics.gap (1 to (2 * options.int("graphview_iterations_rubberband"))).foldLeft(graph) { case (graph, _) => levels.foldLeft(graph) { case (graph, level) => val m = level.length - 1 level.iterator.zipWithIndex.foldLeft(graph) { case (g, (v, i)) => val d = force_weight(g, v) if (d < 0.0 && (i == 0 || vertex_right(g, level(i - 1)) + gap < vertex_left(g, v) + d) || d > 0.0 && (i == m || vertex_left(g, level(i + 1)) - gap > vertex_right(g, v) + d)) move_vertex(g, v, d.round.toDouble) else g } } } } } final class Layout private( val metrics: Metrics, val input_graph: Graph_Display.Graph, val output_graph: Layout.Graph ) { /* vertex coordinates */ def translate_vertex(v: Layout.Vertex, dx: Double, dy: Double): Layout = { if ((dx == 0.0 && dy == 0.0) || !output_graph.defined(v)) this else { val output_graph1 = output_graph.map_node(v, info => info.copy(x = info.x + dx, y = info.y + dy)) new Layout(metrics, input_graph, output_graph1) } } /* regular nodes */ def get_node(node: Graph_Display.Node): Layout.Info = output_graph.get_node(Layout.Node(node)) def nodes_iterator: Iterator[Layout.Info] = for ((_: Layout.Node, (info, _)) <- output_graph.iterator) yield info /* dummies */ def dummies_iterator: Iterator[Layout.Info] = for ((_: Layout.Dummy, (info, _)) <- output_graph.iterator) yield info def dummies_iterator(edge: Graph_Display.Edge): Iterator[Layout.Info] = new Iterator[Layout.Info] { private var index = 0 def hasNext: Boolean = output_graph.defined(Layout.Dummy(edge._1, edge._2, index)) def next(): Layout.Info = { val info = output_graph.get_node(Layout.Dummy(edge._1, edge._2, index)) index += 1 info } } } diff --git a/src/Tools/Graphview/shapes.scala b/src/Tools/Graphview/shapes.scala --- a/src/Tools/Graphview/shapes.scala +++ b/src/Tools/Graphview/shapes.scala @@ -1,215 +1,215 @@ /* Title: Tools/Graphview/shapes.scala Author: Markus Kaiser, TU Muenchen Author: Makarius Drawable shapes. */ package isabelle.graphview import isabelle._ import java.awt.{BasicStroke, Graphics2D, Shape} import java.awt.geom.{AffineTransform, GeneralPath, Path2D, Rectangle2D, RoundRectangle2D, PathIterator} object Shapes { private val default_stroke = new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND) def shape(info: Layout.Info): Rectangle2D.Double = new Rectangle2D.Double(info.x - info.width2, info.y - info.height2, info.width, info.height) def highlight_node(gfx: Graphics2D, graphview: Graphview, node: Graph_Display.Node): Unit = { val metrics = graphview.metrics val extra = metrics.char_width val info = graphview.layout.get_node(node) gfx.setColor(graphview.highlight_color) gfx.fill(new Rectangle2D.Double( info.x - info.width2 - extra, info.y - info.height2 - extra, info.width + 2 * extra, info.height + 2 * extra)) } def paint_node(gfx: Graphics2D, graphview: Graphview, node: Graph_Display.Node): Unit = { val metrics = graphview.metrics val info = graphview.layout.get_node(node) val c = graphview.node_color(node) val s = shape(info) gfx.setColor(c.background) gfx.fill(s) gfx.setColor(c.border) gfx.setStroke(default_stroke) gfx.draw(s) gfx.setColor(c.foreground) gfx.setFont(metrics.font) val text_width = info.lines.foldLeft(0.0) { case (w, line) => w max metrics.string_bounds(line).getWidth } val text_height = (info.lines.length max 1) * metrics.height.ceil val x = (s.getCenterX - text_width / 2).round.toInt var y = (s.getCenterY - text_height / 2 + metrics.ascent).round.toInt for (line <- info.lines) { gfx.drawString(Word.bidi_override(line), x, y) y += metrics.height.ceil.toInt } } def paint_dummy(gfx: Graphics2D, graphview: Graphview, info: Layout.Info): Unit = { gfx.setStroke(default_stroke) gfx.setColor(graphview.dummy_color) gfx.draw(shape(info)) } object Straight_Edge { def paint(gfx: Graphics2D, graphview: Graphview, edge: Graph_Display.Edge): Unit = { val p = graphview.layout.get_node(edge._1) val q = graphview.layout.get_node(edge._2) val ds = { val a = p.y min q.y val b = p.y max q.y graphview.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList } val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2) path.moveTo(p.x, p.y) ds.foreach(d => path.lineTo(d.x, d.y)) path.lineTo(q.x, q.y) if (graphview.show_dummies) ds.foreach(paint_dummy(gfx, graphview, _)) gfx.setStroke(default_stroke) gfx.setColor(graphview.edge_color(edge, p.y < q.y)) gfx.draw(path) if (graphview.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q)) } } object Cardinal_Spline_Edge { private val slack = 0.1 def paint(gfx: Graphics2D, graphview: Graphview, edge: Graph_Display.Edge): Unit = { val p = graphview.layout.get_node(edge._1) val q = graphview.layout.get_node(edge._2) val ds = { val a = p.y min q.y val b = p.y max q.y graphview.layout.dummies_iterator(edge).filter(d => a < d.y && d.y < b).toList } if (ds.isEmpty) Straight_Edge.paint(gfx, graphview, edge) else { val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2) path.moveTo(p.x, p.y) val coords = p :: ds ::: List(q) val dx = coords(2).x - coords(0).x val dy = coords(2).y - coords(0).y val (dx2, dy2) = - coords.sliding(3).map(_.toList).foldLeft((dx, dy)) { - case ((dx, dy), List(l, m, r)) => + coords.sliding(3).foldLeft((dx, dy)) { + case ((dx, dy), Seq(l, m, r)) => val dx2 = r.x - l.x val dy2 = r.y - l.y path.curveTo( l.x + slack * dx, l.y + slack * dy, m.x - slack * dx2, m.y - slack * dy2, m.x, m.y) (dx2, dy2) - case _ => ??? + case (p, _) => p } val l = ds.last path.curveTo( l.x + slack * dx2, l.y + slack * dy2, q.x - slack * dx2, q.y - slack * dy2, q.x, q.y) if (graphview.show_dummies) ds.foreach(paint_dummy(gfx, graphview, _)) gfx.setStroke(default_stroke) gfx.setColor(graphview.edge_color(edge, p.y < q.y)) gfx.draw(path) if (graphview.show_arrow_heads) Arrow_Head.paint(gfx, path, Shapes.shape(q)) } } } object Arrow_Head { type Point = (Double, Double) private def position(path: GeneralPath, shape: Shape): Option[AffineTransform] = { def intersecting_line(path: GeneralPath, shape: Shape): Option[(Point, Point)] = { val i = path.getPathIterator(null, 1.0) val seg = Array[Double](0.0, 0.0, 0.0, 0.0, 0.0, 0.0) var p1 = (0.0, 0.0) var p2 = (0.0, 0.0) while (!i.isDone) { i.currentSegment(seg) match { case PathIterator.SEG_MOVETO => p2 = (seg(0), seg(1)) case PathIterator.SEG_LINETO => p1 = p2 p2 = (seg(0), seg(1)) if(shape.contains(seg(0), seg(1))) return Some((p1, p2)) case _ => } i.next() } None } def binary_search(line: (Point, Point), shape: Shape): Option[AffineTransform] = { val ((fx, fy), (tx, ty)) = line if (shape.contains(fx, fy) == shape.contains(tx, ty)) None else { val (dx, dy) = (fx - tx, fy - ty) if ((dx * dx + dy * dy) < 1.0) { val at = AffineTransform.getTranslateInstance(fx, fy) at.rotate(- (math.atan2(dx, dy) + math.Pi / 2)) Some(at) } else { val (mx, my) = (fx + (tx - fx) / 2.0, fy + (ty - fy) / 2.0) if (shape.contains(fx, fy) == shape.contains(mx, my)) binary_search(((mx, my), (tx, ty)), shape) else binary_search(((fx, fy), (mx, my)), shape) } } } intersecting_line(path, shape) match { case None => None case Some(line) => binary_search(line, shape) } } def paint(gfx: Graphics2D, path: GeneralPath, shape: Shape): Unit = { position(path, shape) match { case None => case Some(at) => val arrow = new GeneralPath(Path2D.WIND_EVEN_ODD, 3) arrow.moveTo(0, 0) arrow.lineTo(-10, 4) arrow.lineTo(-6, 0) arrow.lineTo(-10, -4) arrow.lineTo(0, 0) arrow.transform(at) gfx.fill(arrow) } } } } diff --git a/src/Tools/jEdit/jedit_main/scala_console.scala b/src/Tools/jEdit/jedit_main/scala_console.scala --- a/src/Tools/jEdit/jedit_main/scala_console.scala +++ b/src/Tools/jEdit/jedit_main/scala_console.scala @@ -1,171 +1,155 @@ /* Title: Tools/jEdit/jedit_main/scala_console.scala Author: Makarius Scala instance of Console plugin. */ package isabelle.jedit_main import isabelle._ import isabelle.jedit._ import console.{Console, ConsolePane, Shell, Output} import org.gjt.sp.jedit.JARClassLoader import java.io.{OutputStream, Writer, PrintWriter} +object Scala_Console { + class Interpreter(context: Scala.Compiler.Context, val console: Console) + extends Scala.Interpreter(context) + + def console_interpreter(console: Console): Option[Interpreter] = + Scala.Interpreter.get { case int: Interpreter if int.console == console => int } + + def running_interpreter(): Interpreter = { + val self = Thread.currentThread() + Scala.Interpreter.get { case int: Interpreter if int.running_thread(self) => int } + .getOrElse(error("Bad Scala interpreter thread")) + } + + def running_console(): Console = running_interpreter().console + + val init = """ +import isabelle._ +import isabelle.jedit._ +val console = isabelle.jedit_main.Scala_Console.running_console() +val view = console.getView() +""" +} + class Scala_Console extends Shell("Scala") { /* global state -- owned by GUI thread */ - @volatile private var interpreters = Map.empty[Console, Interpreter] - @volatile private var global_console: Console = null @volatile private var global_out: Output = null @volatile private var global_err: Output = null private val console_stream = new OutputStream { val buf = new StringBuilder(100) override def flush(): Unit = { val s = buf.synchronized { val s = buf.toString; buf.clear(); s } val str = UTF8.decode_permissive(s) GUI_Thread.later { if (global_out == null) java.lang.System.out.print(str) else global_out.writeAttrs(null, str) } Time.seconds(0.01).sleep() // FIXME adhoc delay to avoid loosing output } override def close(): Unit = flush() def write(byte: Int): Unit = { val c = byte.toChar buf.synchronized { buf.append(c) } if (c == '\n') flush() } } private val console_writer = new Writer { def flush(): Unit = console_stream.flush() def close(): Unit = console_stream.flush() def write(cbuf: Array[Char], off: Int, len: Int): Unit = { if (len > 0) { UTF8.bytes(new String(cbuf.slice(off, off + len))).foreach(console_stream.write(_)) } } } private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A = { global_console = console global_out = out global_err = if (err == null) out else err try { scala.Console.withErr(console_stream) { scala.Console.withOut(console_stream) { e } } } finally { console_stream.flush() global_console = null global_out = null global_err = null } } private def report_error(str: String): Unit = { if (global_console == null || global_err == null) isabelle.Output.writeln(str) else GUI_Thread.later { global_err.print(global_console.getErrorColor, str) } } - /* interpreter thread */ - - private abstract class Request - private case class Start(console: Console) extends Request - private case class Execute(console: Console, out: Output, err: Output, command: String) - extends Request - - private class Interpreter { - private val running = Synchronized[Option[Thread]](None) - def interrupt(): Unit = running.change({ opt => opt.foreach(_.interrupt()); opt }) - - private val interp = - Scala.Compiler.context(error = report_error, jar_dirs = JEdit_Lib.directories). - interpreter( - print_writer = new PrintWriter(console_writer, true), - class_loader = new JARClassLoader) - - val thread: Consumer_Thread[Request] = Consumer_Thread.fork("Scala_Console") { - case Start(console) => - interp.bind("view", "org.gjt.sp.jedit.View", console.getView) - interp.bind("console", "console.Console", console) - interp.interpret("import isabelle._; import isabelle.jedit._") - true - - case Execute(console, out, err, command) => - with_console(console, out, err) { - try { - running.change(_ => Some(Thread.currentThread())) - interp.interpret(command) - } - finally { - running.change(_ => None) - Exn.Interrupt.dispose() - } - GUI_Thread.later { - if (err != null) err.commandDone() - out.commandDone() - } - true - } - } - } - - /* jEdit console methods */ override def openConsole(console: Console): Unit = { - val interp = new Interpreter - interp.thread.send(Start(console)) - interpreters += (console -> interp) + val context = + Scala.Compiler.context( + print_writer = new PrintWriter(console_writer, true), + error = report_error, + jar_dirs = JEdit_Lib.directories, + class_loader = Some(new JARClassLoader)) + + val interpreter = new Scala_Console.Interpreter(context, console) + interpreter.execute(_.interp.interpret(Scala_Console.init)) } - override def closeConsole(console: Console): Unit = { - interpreters.get(console) match { - case Some(interp) => - interp.interrupt() - interp.thread.shutdown() - interpreters -= console - case None => - } - } + override def closeConsole(console: Console): Unit = + Scala_Console.console_interpreter(console).foreach(_.shutdown()) override def printInfoMessage(out: Output): Unit = { out.print(null, "This shell evaluates Isabelle/Scala expressions.\n\n" + "The contents of package isabelle and isabelle.jedit are imported.\n" + "The following special toplevel bindings are provided:\n" + " view -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" + " console -- jEdit Console plugin\n" + " PIDE -- Isabelle/PIDE plugin (e.g. PIDE.session, PIDE.snapshot, PIDE.rendering)\n") } override def printPrompt(console: Console, out: Output): Unit = { out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>") out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ") } override def execute( console: Console, input: String, out: Output, - err: Output, command: String + err: Output, + command: String ): Unit = { - interpreters(console).thread.send(Execute(console, out, err, command)) + Scala_Console.console_interpreter(console).foreach(interpreter => + interpreter.execute { context => + with_console(console, out, err) { context.interp.interpret(command) } + GUI_Thread.later { + Option(err).foreach(_.commandDone()) + out.commandDone() + } + }) } override def stop(console: Console): Unit = - interpreters.get(console).foreach(_.interrupt()) + Scala_Console.console_interpreter(console).foreach(_.shutdown()) } diff --git a/src/Tools/jEdit/src/jedit_bibtex.scala b/src/Tools/jEdit/src/jedit_bibtex.scala --- a/src/Tools/jEdit/src/jedit_bibtex.scala +++ b/src/Tools/jEdit/src/jedit_bibtex.scala @@ -1,152 +1,148 @@ /* Title: Tools/jEdit/src/jedit_bibtex.scala Author: Makarius BibTeX support in Isabelle/jEdit. */ package isabelle.jedit import isabelle._ import scala.collection.mutable import java.awt.event.{ActionListener, ActionEvent} import javax.swing.text.Segment import javax.swing.tree.DefaultMutableTreeNode import javax.swing.{JMenu, JMenuItem} import org.gjt.sp.jedit.Buffer import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler} object JEdit_Bibtex { /** context menu **/ - def context_menu(text_area0: JEditTextArea): List[JMenuItem] = { - text_area0 match { - case text_area: TextArea => - text_area.getBuffer match { - case buffer: Buffer - if (Bibtex.is_bibtex(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable) => - val menu = new JMenu("BibTeX entries") - for (entry <- Bibtex.known_entries) { - val item = new JMenuItem(entry.kind) - item.addActionListener(new ActionListener { - def actionPerformed(evt: ActionEvent): Unit = - Isabelle.insert_line_padding(text_area, entry.template) - }) - menu.add(item) - } - List(menu) - case _ => Nil + def context_menu(text_area: JEditTextArea): List[JMenuItem] = { + text_area.getBuffer match { + case buffer: Buffer + if Bibtex.is_bibtex(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable => + val menu = new JMenu("BibTeX entries") + for (entry <- Bibtex.known_entries) { + val item = new JMenuItem(entry.kind) + item.addActionListener(new ActionListener { + def actionPerformed(evt: ActionEvent): Unit = + Isabelle.insert_line_padding(text_area, entry.template) + }) + menu.add(item) } + List(menu) case _ => Nil } } /** token markup **/ /* token style */ private def token_style(context: String, token: Bibtex.Token): Byte = token.kind match { case Bibtex.Token.Kind.COMMAND => JEditToken.KEYWORD2 case Bibtex.Token.Kind.ENTRY => JEditToken.KEYWORD1 case Bibtex.Token.Kind.KEYWORD => JEditToken.OPERATOR case Bibtex.Token.Kind.NAT => JEditToken.LITERAL2 case Bibtex.Token.Kind.STRING => JEditToken.LITERAL1 case Bibtex.Token.Kind.NAME => JEditToken.LABEL case Bibtex.Token.Kind.IDENT => if (Bibtex.is_month(token.source)) JEditToken.LITERAL3 else Bibtex.get_entry(context) match { case Some(entry) if entry.is_required(token.source) => JEditToken.KEYWORD3 case Some(entry) if entry.is_optional(token.source) => JEditToken.KEYWORD4 case _ => JEditToken.DIGIT } case Bibtex.Token.Kind.SPACE => JEditToken.NULL case Bibtex.Token.Kind.COMMENT => JEditToken.COMMENT1 case Bibtex.Token.Kind.ERROR => JEditToken.INVALID } /* line context */ private val mode_rule_set = Token_Markup.mode_rule_set("bibtex") private class Line_Context(val context: Option[Bibtex.Line_Context]) extends TokenMarker.LineContext(mode_rule_set, null) { override def hashCode: Int = context.hashCode override def equals(that: Any): Boolean = that match { case other: Line_Context => context == other.context case _ => false } } /* token marker */ class Token_Marker extends TokenMarker { addRuleSet(mode_rule_set) override def markTokens( context: TokenMarker.LineContext, handler: TokenHandler, raw_line: Segment ): TokenMarker.LineContext = { val line_ctxt = context match { case c: Line_Context => c.context case _ => Some(Bibtex.Ignored) } val line = if (raw_line == null) new Segment else raw_line def no_markup = { val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString) (List(styled_token), new Line_Context(None)) } val context1 = { val (styled_tokens, context1) = line_ctxt match { case Some(ctxt) => try { val (chunks, ctxt1) = Bibtex.parse_line(line, ctxt) val styled_tokens = for { chunk <- chunks; tok <- chunk.tokens } yield (token_style(chunk.kind, tok), tok.source) (styled_tokens, new Line_Context(Some(ctxt1))) } catch { case ERROR(msg) => Output.warning(msg); no_markup } case None => no_markup } var offset = 0 for ((style, token) <- styled_tokens) { val length = token.length val end_offset = offset + length if ((offset until end_offset).exists(i => line.charAt(i) == '\t')) { for (i <- offset until end_offset) handler.handleToken(line, style, i, 1, context1) } else handler.handleToken(line, style, offset, length, context1) offset += length } handler.handleToken(line, JEditToken.END, line.count, 0, context1) context1 } val context2 = context1.intern handler.setLineContext(context2) context2 } } }