# HG changeset patch # User wenzelm # Date 1330811604 -3600 # Node ID 3bbc156823dd546bc6d37111283ce12ff4c3d8c0 # Parent 69b10720104062ddb7c20ba0942cc27ffbcfa4b6# Parent 4f298836018b0d64a2df5d9a1b6d0734bad4d3d1 merged; diff -r 69b107201040 -r 3bbc156823dd src/HOL/SPARK/Tools/fdl_parser.ML --- a/src/HOL/SPARK/Tools/fdl_parser.ML Sat Mar 03 22:46:34 2012 +0100 +++ b/src/HOL/SPARK/Tools/fdl_parser.ML Sat Mar 03 22:53:24 2012 +0100 @@ -325,7 +325,7 @@ fun declarations x = ($$$ "title" |-- subprogram_kind -- identifier --| $$$ ";" -- (Scan.repeat ((type_decl || const_decl || var_decl || fun_decl) --| - !!! ($$$ ";")) >> (fn ds => apply ds empty_decls)) --| + !!! ($$$ ";")) >> (fn ds => fold I ds empty_decls)) --| $$$ "end" --| $$$ ";") x; fun parse_declarations pos s = @@ -371,7 +371,7 @@ val rules = parse_all (rule >> (apfst o cons) || rule_family >> (apsnd o cons)) >> - (fn rls => apply (rev rls) ([], [])); + (fn rls => fold_rev I rls ([], [])); fun parse_rules pos s = s |> diff -r 69b107201040 -r 3bbc156823dd src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML Sat Mar 03 22:46:34 2012 +0100 +++ b/src/HOL/Tools/choice_specification.ML Sat Mar 03 22:53:24 2012 +0100 @@ -185,20 +185,21 @@ fun undo_imps thm = Thm.equal_elim (Thm.symmetric rew_imp) thm - fun add_final (arg as (thy, thm)) = + fun add_final (thm, thy) = if name = "" - then arg |> Library.swap + then (thm, thy) else (writeln (" " ^ name ^ ": " ^ Display.string_of_thm_global thy thm); Global_Theory.store_thm (Binding.name name, thm) thy) in - args |> apsnd (remove_alls frees) - |> apsnd undo_imps - |> apsnd Drule.export_without_context - |> Thm.theory_attributes + swap args + |> apfst (remove_alls frees) + |> apfst undo_imps + |> apfst Drule.export_without_context + |-> Thm.theory_attributes (map (Attrib.attribute thy) (@{attributes [nitpick_choice_spec]} @ atts)) |> add_final - |> Library.swap + |> swap end fun process_all [proc_arg] args = diff -r 69b107201040 -r 3bbc156823dd src/Pure/General/output.ML --- a/src/Pure/General/output.ML Sat Mar 03 22:46:34 2012 +0100 +++ b/src/Pure/General/output.ML Sat Mar 03 22:53:24 2012 +0100 @@ -34,7 +34,7 @@ val prompt_fn: (output -> unit) Unsynchronized.ref val status_fn: (output -> unit) Unsynchronized.ref val report_fn: (output -> unit) Unsynchronized.ref - val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref + val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref end val urgent_message: string -> unit val error_msg': serial * string -> unit @@ -42,7 +42,7 @@ val prompt: string -> unit val status: string -> unit val report: string -> unit - val raw_message: Properties.T -> string -> unit + val protocol_message: Properties.T -> string -> unit end; structure Output: OUTPUT = @@ -97,8 +97,8 @@ val prompt_fn = Unsynchronized.ref physical_stdout; val status_fn = Unsynchronized.ref (fn _: output => ()); val report_fn = Unsynchronized.ref (fn _: output => ()); - val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref = - Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.raw_message undefined in TTY mode"); + val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref = + Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.protocol_message undefined in TTY mode"); end; fun writeln s = ! Private_Hooks.writeln_fn (output s); @@ -110,7 +110,7 @@ fun prompt s = ! Private_Hooks.prompt_fn (output s); fun status s = ! Private_Hooks.status_fn (output s); fun report s = ! Private_Hooks.report_fn (output s); -fun raw_message props s = ! Private_Hooks.raw_message_fn props (output s); +fun protocol_message props s = ! Private_Hooks.protocol_message_fn props (output s); end; diff -r 69b107201040 -r 3bbc156823dd src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Sat Mar 03 22:46:34 2012 +0100 +++ b/src/Pure/Isar/attrib.ML Sat Mar 03 22:53:24 2012 +0100 @@ -191,8 +191,7 @@ Parse.$$$ "[" |-- Args.attribs (intern thy) --| Parse.$$$ "]" >> (fn srcs => let val atts = map (attribute_i thy) srcs; - val (context', th') = - Library.apply (map Thm.apply_attribute atts) (context, Drule.dummy_thm); + val (th', context') = fold (uncurry o Thm.apply_attribute) atts (Drule.dummy_thm, context); in (context', pick "" [th']) end) || (Scan.ahead Args.alt_name -- Args.named_fact get_fact @@ -204,8 +203,8 @@ let val ths = Facts.select thmref fact; val atts = map (attribute_i thy) srcs; - val (context', ths') = - Library.foldl_map (Library.apply (map Thm.apply_attribute atts)) (context, ths); + val (ths', context') = + fold_map (curry (fold (uncurry o Thm.apply_attribute) atts)) ths context; in (context', pick name ths') end) end); diff -r 69b107201040 -r 3bbc156823dd src/Pure/Isar/keyword.ML --- a/src/Pure/Isar/keyword.ML Sat Mar 03 22:46:34 2012 +0100 +++ b/src/Pure/Isar/keyword.ML Sat Mar 03 22:53:24 2012 +0100 @@ -153,7 +153,7 @@ fun status_message m s = Position.setmp_thread_data Position.none - (if print_mode_active keyword_statusN then Output.raw_message m else writeln) s; + (if print_mode_active keyword_statusN then Output.protocol_message m else writeln) s; fun keyword_status name = status_message (Isabelle_Markup.keyword_decl name) diff -r 69b107201040 -r 3bbc156823dd src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Sat Mar 03 22:46:34 2012 +0100 +++ b/src/Pure/Isar/method.ML Sat Mar 03 22:53:24 2012 +0100 @@ -377,13 +377,12 @@ local fun thms ss = Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat; -fun app (f, att) (context, ths) = - Library.foldl_map (Thm.apply_attribute att) (Context.map_proof f context, ths); +fun app (f, att) ths context = fold_map (Thm.apply_attribute att) ths (Context.map_proof f context); in fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :|-- - (fn (m, ths) => Scan.succeed (app m (context, ths)))); + (fn (m, ths) => Scan.succeed (swap (app m ths context)))); fun sections ss = Scan.repeat (section ss); diff -r 69b107201040 -r 3bbc156823dd src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sat Mar 03 22:46:34 2012 +0100 +++ b/src/Pure/Isar/proof_context.ML Sat Mar 03 22:53:24 2012 +0100 @@ -894,13 +894,12 @@ in -fun note_thmss kind = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt => +fun note_thmss kind = fold_map (fn ((b, more_atts), raw_facts) => fn ctxt => let val name = full_name ctxt b; val facts = Global_Theory.name_thmss false name raw_facts; - fun app (th, attrs) x = - swap (Library.foldl_map - (Thm.proof_attributes (surround (Thm.kind kind) (attrs @ more_attrs))) (x, th)); + fun app (ths, atts) = + fold_map (Thm.proof_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths; val (res, ctxt') = fold_map app facts ctxt; val thms = Global_Theory.name_thms false false name (flat res); val Mode {stmt, ...} = get_mode ctxt; diff -r 69b107201040 -r 3bbc156823dd src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Sat Mar 03 22:46:34 2012 +0100 +++ b/src/Pure/Isar/specification.ML Sat Mar 03 22:53:24 2012 +0100 @@ -415,7 +415,7 @@ |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths) |> tap (fn state => not schematic andalso Proof.schematic_goal state andalso error "Illegal schematic goal statement") - |> Library.apply (map (fn (f, _) => f int) (rev (Theorem_Hook.get (Context.Proof goal_ctxt)))) + |> fold_rev (fn (f, _) => f int) (Theorem_Hook.get (Context.Proof goal_ctxt)) end; in diff -r 69b107201040 -r 3bbc156823dd src/Pure/PIDE/isabelle_markup.ML --- a/src/Pure/PIDE/isabelle_markup.ML Sat Mar 03 22:46:34 2012 +0100 +++ b/src/Pure/PIDE/isabelle_markup.ML Sat Mar 03 22:53:24 2012 +0100 @@ -302,7 +302,7 @@ val (badN, bad) = markup_elem "bad"; -(* raw message functions *) +(* protocol message functions *) val functionN = "function" diff -r 69b107201040 -r 3bbc156823dd src/Pure/PIDE/isabelle_markup.scala --- a/src/Pure/PIDE/isabelle_markup.scala Sat Mar 03 22:46:34 2012 +0100 +++ b/src/Pure/PIDE/isabelle_markup.scala Sat Mar 03 22:53:24 2012 +0100 @@ -229,7 +229,7 @@ val TRACING = "tracing" val WARNING = "warning" val ERROR = "error" - val RAW = "raw" + val PROTOCOL = "protocol" val SYSTEM = "system" val STDOUT = "stdout" val STDERR = "stderr" @@ -242,7 +242,7 @@ val BAD = "bad" - /* raw message functions */ + /* protocol message functions */ val FUNCTION = "function" val Function = new Properties.String(FUNCTION) diff -r 69b107201040 -r 3bbc156823dd src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Sat Mar 03 22:46:34 2012 +0100 +++ b/src/Pure/PIDE/protocol.ML Sat Mar 03 22:53:24 2012 +0100 @@ -57,7 +57,7 @@ val (assignment, state1) = Document.update old_id new_id edits state; val _ = Future.join_tasks running; val _ = - Output.raw_message Isabelle_Markup.assign_execs + Output.protocol_message Isabelle_Markup.assign_execs ((new_id, assignment) |> let open XML.Encode in pair int (pair (list (pair int (option int))) (list (pair string (option int)))) end @@ -73,7 +73,7 @@ YXML.parse_body versions_yxml |> let open XML.Decode in list int end; val state1 = Document.remove_versions versions state; - val _ = Output.raw_message Isabelle_Markup.removed_versions versions_yxml; + val _ = Output.protocol_message Isabelle_Markup.removed_versions versions_yxml; in state1 end)); val _ = diff -r 69b107201040 -r 3bbc156823dd src/Pure/System/invoke_scala.ML --- a/src/Pure/System/invoke_scala.ML Sat Mar 03 22:46:34 2012 +0100 +++ b/src/Pure/System/invoke_scala.ML Sat Mar 03 22:53:24 2012 +0100 @@ -33,10 +33,10 @@ fun promise_method name arg = let val id = new_id (); - fun abort () = Output.raw_message (Isabelle_Markup.cancel_scala id) ""; + fun abort () = Output.protocol_message (Isabelle_Markup.cancel_scala id) ""; val promise = Future.promise abort : string future; val _ = Synchronized.change promises (Symtab.update (id, promise)); - val _ = Output.raw_message (Isabelle_Markup.invoke_scala name id) arg; + val _ = Output.protocol_message (Isabelle_Markup.invoke_scala name id) arg; in promise end; fun method name arg = Future.join (promise_method name arg); diff -r 69b107201040 -r 3bbc156823dd src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Sat Mar 03 22:46:34 2012 +0100 +++ b/src/Pure/System/isabelle_process.ML Sat Mar 03 22:53:24 2012 +0100 @@ -109,7 +109,7 @@ Output.Private_Hooks.tracing_fn := (fn s => standard_message mbox (SOME (serial ())) "E" s); Output.Private_Hooks.warning_fn := (fn s => standard_message mbox (SOME (serial ())) "F" s); Output.Private_Hooks.error_fn := (fn (i, s) => standard_message mbox (SOME i) "G" s); - Output.Private_Hooks.raw_message_fn := message true mbox "H"; + Output.Private_Hooks.protocol_message_fn := message true mbox "H"; Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn; Output.Private_Hooks.prompt_fn := ignore; message true mbox "A" [] (Session.welcome ()) @@ -185,7 +185,7 @@ val _ = Keyword.status (); val _ = Thy_Info.status (); - val _ = Output.raw_message Isabelle_Markup.ready ""; + val _ = Output.protocol_message Isabelle_Markup.ready ""; in loop channel end)); fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2); diff -r 69b107201040 -r 3bbc156823dd src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Sat Mar 03 22:46:34 2012 +0100 +++ b/src/Pure/System/isabelle_process.scala Sat Mar 03 22:53:24 2012 +0100 @@ -18,7 +18,7 @@ object Isabelle_Process { - /* results */ + /* messages */ object Kind { @@ -30,7 +30,7 @@ ('E' : Int) -> Isabelle_Markup.TRACING, ('F' : Int) -> Isabelle_Markup.WARNING, ('G' : Int) -> Isabelle_Markup.ERROR, - ('H' : Int) -> Isabelle_Markup.RAW) + ('H' : Int) -> Isabelle_Markup.PROTOCOL) } sealed abstract class Message @@ -44,7 +44,7 @@ XML.elem(Isabelle_Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString } - class Result(val message: XML.Elem) extends Message + class Output(val message: XML.Elem) extends Message { def kind: String = message.markup.name def properties: Properties.T = message.markup.properties @@ -57,14 +57,14 @@ def is_system = kind == Isabelle_Markup.SYSTEM def is_status = kind == Isabelle_Markup.STATUS def is_report = kind == Isabelle_Markup.REPORT - def is_raw = kind == Isabelle_Markup.RAW + def is_protocol = kind == Isabelle_Markup.PROTOCOL def is_syslog = is_init || is_exit || is_system || is_stderr override def toString: String = { val res = if (is_status || is_report) message.body.map(_.toString).mkString - else if (is_raw) "..." + else if (is_protocol) "..." else Pretty.string_of(message.body) if (properties.isEmpty) kind.toString + " [[" + res + "]]" @@ -84,29 +84,29 @@ import Isabelle_Process._ - /* results */ + /* output */ - private def system_result(text: String) + private def system_output(text: String) { - receiver(new Result(XML.Elem(Markup(Isabelle_Markup.SYSTEM, Nil), List(XML.Text(text))))) + receiver(new Output(XML.Elem(Markup(Isabelle_Markup.SYSTEM, Nil), List(XML.Text(text))))) } private val xml_cache = new XML.Cache() - private def put_result(kind: String, props: Properties.T, body: XML.Body) + private def output_message(kind: String, props: Properties.T, body: XML.Body) { if (kind == Isabelle_Markup.INIT) system_channel.accepted() - if (kind == Isabelle_Markup.RAW) - receiver(new Result(XML.Elem(Markup(kind, props), body))) + if (kind == Isabelle_Markup.PROTOCOL) + receiver(new Output(XML.Elem(Markup(kind, props), body))) else { val msg = XML.Elem(Markup(kind, props), Protocol.clean_message(body)) - receiver(new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem])) + receiver(new Output(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem])) } } - private def put_result(kind: String, text: String) + private def output_message(kind: String, text: String) { - put_result(kind, Nil, List(XML.Text(Symbol.decode(text)))) + output_message(kind, Nil, List(XML.Text(Symbol.decode(text)))) } @@ -147,7 +147,7 @@ private def terminate_process() { try { process.terminate } - catch { case e: IOException => system_result("Failed to terminate Isabelle: " + e.getMessage) } + catch { case e: IOException => system_output("Failed to terminate Isabelle: " + e.getMessage) } } private val process_manager = Simple_Thread.fork("process_manager") @@ -169,10 +169,10 @@ } (finished.isEmpty || !finished.get, result.toString.trim) } - if (startup_errors != "") system_result(startup_errors) + if (startup_errors != "") system_output(startup_errors) if (startup_failed) { - put_result(Isabelle_Markup.EXIT, "Return code: 127") + output_message(Isabelle_Markup.EXIT, "Return code: 127") process.stdin.close Thread.sleep(300) terminate_process() @@ -182,17 +182,17 @@ val (command_stream, message_stream) = system_channel.rendezvous() standard_input = stdin_actor() - val stdout = raw_output_actor(false) - val stderr = raw_output_actor(true) + val stdout = physical_output_actor(false) + val stderr = physical_output_actor(true) command_input = input_actor(command_stream) val message = message_actor(message_stream) val rc = process_result.join - system_result("process terminated") + system_output("process terminated") for ((thread, _) <- List(standard_input, stdout, stderr, command_input, message)) thread.join - system_result("process_manager terminated") - put_result(Isabelle_Markup.EXIT, "Return code: " + rc.toString) + system_output("process_manager terminated") + output_message(Isabelle_Markup.EXIT, "Return code: " + rc.toString) } system_channel.accepted() } @@ -205,7 +205,7 @@ def terminate() { close() - system_result("Terminating Isabelle process") + system_output("Terminating Isabelle process") terminate_process() } @@ -213,7 +213,7 @@ /** stream actors **/ - /* raw stdin */ + /* physical stdin */ private def stdin_actor(): (Thread, Actor) = { @@ -235,15 +235,15 @@ //}}} } } - catch { case e: IOException => system_result(name + ": " + e.getMessage) } - system_result(name + " terminated") + catch { case e: IOException => system_output(name + ": " + e.getMessage) } + system_output(name + " terminated") } } - /* raw output */ + /* physical output */ - private def raw_output_actor(err: Boolean): (Thread, Actor) = + private def physical_output_actor(err: Boolean): (Thread, Actor) = { val (name, reader, markup) = if (err) ("standard_error", process.stderr, Isabelle_Markup.STDERR) @@ -263,7 +263,7 @@ else done = true } if (result.length > 0) { - put_result(markup, result.toString) + output_message(markup, result.toString) result.length = 0 } else { @@ -273,8 +273,8 @@ //}}} } } - catch { case e: IOException => system_result(name + ": " + e.getMessage) } - system_result(name + " terminated") + catch { case e: IOException => system_output(name + ": " + e.getMessage) } + system_output(name + " terminated") } } @@ -304,8 +304,8 @@ //}}} } } - catch { case e: IOException => system_result(name + ": " + e.getMessage) } - system_result(name + " terminated") + catch { case e: IOException => system_output(name + ": " + e.getMessage) } + system_output(name + " terminated") } } @@ -364,8 +364,8 @@ case List(XML.Elem(Markup(name, props), Nil)) if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) => val kind = Kind.message_markup(name(0)) - val body = read_chunk(kind != Isabelle_Markup.RAW) - put_result(kind, props, body) + val body = read_chunk(kind != Isabelle_Markup.PROTOCOL) + output_message(kind, props, body) case _ => read_chunk(false) throw new Protocol_Error("bad header: " + header.toString) @@ -376,12 +376,12 @@ } while (c != -1) } catch { - case e: IOException => system_result("Cannot read message:\n" + e.getMessage) - case e: Protocol_Error => system_result("Malformed message:\n" + e.getMessage) + case e: IOException => system_output("Cannot read message:\n" + e.getMessage) + case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage) } stream.close - system_result(name + " terminated") + system_output(name + " terminated") } } diff -r 69b107201040 -r 3bbc156823dd src/Pure/System/session.scala --- a/src/Pure/System/session.scala Sat Mar 03 22:46:34 2012 +0100 +++ b/src/Pure/System/session.scala Sat Mar 03 22:53:24 2012 +0100 @@ -12,6 +12,7 @@ import java.util.{Timer, TimerTask} import scala.collection.mutable +import scala.collection.immutable.Queue import scala.actors.TIMEOUT import scala.actors.Actor._ @@ -37,7 +38,7 @@ class Session(thy_load: Thy_Load = new Thy_Load) { - /* real time parameters */ // FIXME properties or settings (!?) + /* tuning parameters */ // FIXME properties or settings (!?) val message_delay = Time.seconds(0.01) // prover messages val input_delay = Time.seconds(0.3) // user input (e.g. text edits, cursor movement) @@ -46,6 +47,7 @@ val load_delay = Time.seconds(0.5) // file load operations (new buffers etc.) val prune_delay = Time.seconds(60.0) // prune history -- delete old versions val prune_size = 0 // size of retained history + val syslog_limit = 100 /* pervasive event buses */ @@ -54,9 +56,9 @@ val caret_focus = new Event_Bus[Session.Caret_Focus.type] val commands_changed = new Event_Bus[Session.Commands_Changed] val phase_changed = new Event_Bus[Session.Phase] - val syslog_messages = new Event_Bus[Isabelle_Process.Result] - val raw_output_messages = new Event_Bus[Isabelle_Process.Result] - val protocol_messages = new Event_Bus[Isabelle_Process.Message] // potential bottle-neck + val syslog_messages = new Event_Bus[Isabelle_Process.Output] + val raw_output_messages = new Event_Bus[Isabelle_Process.Output] + val all_messages = new Event_Bus[Isabelle_Process.Message] // potential bottle-neck @@ -119,8 +121,8 @@ @volatile private var syntax = Outer_Syntax.init() def current_syntax(): Outer_Syntax = syntax - @volatile private var reverse_syslog = List[XML.Elem]() - def syslog(): String = cat_lines(reverse_syslog.reverse.map(msg => XML.content(msg).mkString)) + private val syslog = Volatile(Queue.empty[XML.Elem]) + def current_syslog(): String = cat_lines(syslog().iterator.map(msg => XML.content(msg).mkString)) @volatile private var _phase: Session.Phase = Session.Inactive private def phase_=(new_phase: Session.Phase) @@ -191,7 +193,14 @@ def invoke(msg: Isabelle_Process.Message): Unit = synchronized { buffer += msg msg match { - case result: Isabelle_Process.Result if result.is_raw => flush() + case output: Isabelle_Process.Output => + if (output.is_syslog) + syslog >> (queue => + { + val queue1 = queue.enqueue(output.message) + if (queue1.length > syslog_limit) queue1.dequeue._2 else queue1 + }) + if (output.is_protocol) flush() case _ => } } @@ -334,34 +343,34 @@ //}}} - /* prover results */ + /* prover output */ - def handle_result(result: Isabelle_Process.Result) + def handle_output(output: Isabelle_Process.Output) //{{{ { - def bad_result(result: Isabelle_Process.Result) + def bad_output(output: Isabelle_Process.Output) { if (verbose) - System.err.println("Ignoring prover result: " + result.message.toString) + System.err.println("Ignoring prover output: " + output.message.toString) } - result.properties match { + output.properties match { - case Position.Id(state_id) if !result.is_raw => + case Position.Id(state_id) if !output.is_protocol => try { - val st = global_state >>> (_.accumulate(state_id, result.message)) + val st = global_state >>> (_.accumulate(state_id, output.message)) delay_commands_changed.invoke(st.command) } catch { - case _: Document.State.Fail => bad_result(result) + case _: Document.State.Fail => bad_output(output) } - case Isabelle_Markup.Assign_Execs if result.is_raw => - XML.content(result.body).mkString match { + case Isabelle_Markup.Assign_Execs if output.is_protocol => + XML.content(output.body).mkString match { case Protocol.Assign(id, assign) => try { handle_assign(id, assign) } - catch { case _: Document.State.Fail => bad_result(result) } - case _ => bad_result(result) + catch { case _: Document.State.Fail => bad_output(output) } + case _ => bad_output(output) } // FIXME separate timeout event/message!? if (prover.isDefined && System.currentTimeMillis() > prune_next) { @@ -370,47 +379,44 @@ prune_next = System.currentTimeMillis() + prune_delay.ms } - case Isabelle_Markup.Removed_Versions if result.is_raw => - XML.content(result.body).mkString match { + case Isabelle_Markup.Removed_Versions if output.is_protocol => + XML.content(output.body).mkString match { case Protocol.Removed(removed) => try { handle_removed(removed) } - catch { case _: Document.State.Fail => bad_result(result) } - case _ => bad_result(result) + catch { case _: Document.State.Fail => bad_output(output) } + case _ => bad_output(output) } - case Isabelle_Markup.Invoke_Scala(name, id) if result.is_raw => + case Isabelle_Markup.Invoke_Scala(name, id) if output.is_protocol => Future.fork { - val arg = XML.content(result.body).mkString + val arg = XML.content(output.body).mkString val (tag, res) = Invoke_Scala.method(name, arg) prover.get.invoke_scala(id, tag, res) } - case Isabelle_Markup.Cancel_Scala(id) if result.is_raw => + case Isabelle_Markup.Cancel_Scala(id) if output.is_protocol => System.err.println("cancel_scala " + id) // FIXME actually cancel JVM task - case Isabelle_Markup.Ready if result.is_raw => + case Isabelle_Markup.Ready if output.is_protocol => // FIXME move to ML side (!?) syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have") syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show") phase = Session.Ready - case Isabelle_Markup.Loaded_Theory(name) if result.is_raw => + case Isabelle_Markup.Loaded_Theory(name) if output.is_protocol => thy_load.register_thy(name) - case Isabelle_Markup.Command_Decl(name, kind) if result.is_raw => + case Isabelle_Markup.Command_Decl(name, kind) if output.is_protocol => syntax += (name, kind) - case Isabelle_Markup.Keyword_Decl(name) if result.is_raw => + case Isabelle_Markup.Keyword_Decl(name) if output.is_protocol => syntax += name case _ => - if (result.is_syslog) { - reverse_syslog ::= result.message - if (result.is_exit && phase == Session.Startup) phase = Session.Failed - else if (result.is_exit) phase = Session.Inactive - } - else if (result.is_stdout) { } - else bad_result(result) + if (output.is_exit && phase == Session.Startup) phase = Session.Failed + else if (output.is_exit) phase = Session.Inactive + else if (output.is_stdout) { } + else bad_output(output) } } //}}} @@ -465,13 +471,13 @@ case Messages(msgs) => msgs foreach { case input: Isabelle_Process.Input => - protocol_messages.event(input) + all_messages.event(input) - case result: Isabelle_Process.Result => - handle_result(result) - if (result.is_syslog) syslog_messages.event(result) - if (result.is_stdout || result.is_stderr) raw_output_messages.event(result) - protocol_messages.event(result) + case output: Isabelle_Process.Output => + handle_output(output) + if (output.is_syslog) syslog_messages.event(output) + if (output.is_stdout || output.is_stderr) raw_output_messages.event(output) + all_messages.event(output) } case change: Change_Node diff -r 69b107201040 -r 3bbc156823dd src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Sat Mar 03 22:46:34 2012 +0100 +++ b/src/Pure/Thy/thy_info.ML Sat Mar 03 22:53:24 2012 +0100 @@ -89,7 +89,8 @@ fun get_names () = Graph.topological_order (get_thys ()); fun status () = - List.app (fn name => Output.raw_message (Isabelle_Markup.loaded_theory name) "") (get_names ()); + List.app (fn name => Output.protocol_message (Isabelle_Markup.loaded_theory name) "") + (get_names ()); (* access thy *) diff -r 69b107201040 -r 3bbc156823dd src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Sat Mar 03 22:46:34 2012 +0100 +++ b/src/Pure/global_theory.ML Sat Mar 03 22:53:24 2012 +0100 @@ -80,7 +80,7 @@ (* forked proofs *) -fun register_proofs (thy, thms) = (Data.map (apsnd (pairself (add_proofs thms))) thy, thms); +fun register_proofs thms thy = (thms, Data.map (apsnd (pairself (add_proofs thms))) thy); val begin_recent_proofs = Data.map (apsnd (apfst (K empty_proofs))); val join_recent_proofs = force_proofs o #1 o #2 o Data.get; @@ -153,13 +153,12 @@ fun enter_thms pre_name post_name app_att (b, thms) thy = if Binding.is_empty b - then swap (register_proofs (app_att (thy, thms))) + then app_att thms thy |-> register_proofs else let val naming = Sign.naming_of thy; val name = Name_Space.full_name naming b; - val (thy', thms') = - register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms))); + val (thms', thy') = app_att (pre_name name thms) thy |>> post_name name |-> register_proofs; val thms'' = map (Thm.transfer thy') thms'; val thy'' = thy' |> (Data.map o apfst) @@ -170,19 +169,18 @@ (* store_thm(s) *) fun store_thms (b, thms) = - enter_thms (name_thms true true) (name_thms false true) I (b, thms); + enter_thms (name_thms true true) (name_thms false true) pair (b, thms); fun store_thm (b, th) = store_thms (b, [th]) #>> the_single; fun store_thm_open (b, th) = - enter_thms (name_thms true false) (name_thms false false) I (b, [th]) #>> the_single; + enter_thms (name_thms true false) (name_thms false false) pair (b, [th]) #>> the_single; (* add_thms(s) *) fun add_thms_atts pre_name ((b, thms), atts) = - enter_thms pre_name (name_thms false true) - (Library.foldl_map (Thm.theory_attributes atts)) (b, thms); + enter_thms pre_name (name_thms false true) (fold_map (Thm.theory_attributes atts)) (b, thms); fun gen_add_thmss pre_name = fold_map (add_thms_atts pre_name); @@ -204,13 +202,14 @@ (* note_thmss *) -fun note_thmss kind = fold_map (fn ((b, more_atts), ths_atts) => fn thy => +fun note_thmss kind = fold_map (fn ((b, more_atts), facts) => fn thy => let val name = Sign.full_name thy b; - fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths); - val (thms, thy') = thy |> enter_thms - (name_thmss true) (name_thms false true) (apsnd flat o Library.foldl_map app) - (b, map (fn (ths, atts) => (ths, surround (Thm.kind kind) (atts @ more_atts))) ths_atts); + fun app (ths, atts) = + fold_map (Thm.theory_attributes (surround (Thm.kind kind) (atts @ more_atts))) ths; + val (thms, thy') = + enter_thms (name_thmss true) (name_thms false true) (apfst flat oo fold_map app) + (b, facts) thy; in ((name, thms), thy') end); diff -r 69b107201040 -r 3bbc156823dd src/Pure/library.ML --- a/src/Pure/library.ML Sat Mar 03 22:46:34 2012 +0100 +++ b/src/Pure/library.ML Sat Mar 03 22:53:24 2012 +0100 @@ -62,7 +62,6 @@ val the_single: 'a list -> 'a val singleton: ('a list -> 'b list) -> 'a -> 'b val yield_singleton: ('a list -> 'c -> 'b list * 'c) -> 'a -> 'c -> 'b * 'c - val apply: ('a -> 'a) list -> 'a -> 'a val perhaps_apply: ('a -> 'a option) list -> 'a -> 'a option val perhaps_loop: ('a -> 'a option) -> 'a -> 'a option val foldl1: ('a * 'a -> 'a) -> 'a list -> 'a @@ -229,7 +228,6 @@ include BASIC_LIBRARY val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b - val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list end; structure Library: LIBRARY = @@ -334,9 +332,6 @@ fun yield_singleton f x = f [x] #>> the_single; -fun apply [] x = x - | apply (f :: fs) x = apply fs (f x); - fun perhaps_apply funs arg = let fun app [] res = res @@ -386,16 +381,6 @@ | itr (x::l) = f(x, itr l) in itr l end; -fun foldl_map f = - let - fun fold_aux (x, []) = (x, []) - | fold_aux (x, y :: ys) = - let - val (x', y') = f (x, y); - val (x'', ys') = fold_aux (x', ys); - in (x'', y' :: ys') end; - in fold_aux end; - (* basic list functions *) diff -r 69b107201040 -r 3bbc156823dd src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Sat Mar 03 22:46:34 2012 +0100 +++ b/src/Pure/more_thm.ML Sat Mar 03 22:53:24 2012 +0100 @@ -73,10 +73,10 @@ val rule_attribute: (Context.generic -> thm -> thm) -> attribute val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute - val apply_attribute: attribute -> Context.generic * thm -> Context.generic * thm + val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic - val theory_attributes: attribute list -> theory * thm -> theory * thm - val proof_attributes: attribute list -> Proof.context * thm -> Proof.context * thm + val theory_attributes: attribute list -> thm -> theory -> thm * theory + val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context val no_attributes: 'a -> 'a * 'b list val simple_fact: 'a -> ('a * 'b list) list val tag_rule: Properties.entry -> thm -> thm @@ -403,16 +403,16 @@ fun declaration_attribute f (x, th) = (SOME (f th x), NONE); fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end; -fun apply_attribute (att: attribute) (x, th) = +fun apply_attribute (att: attribute) th x = let val (x', th') = att (x, th) - in (the_default x x', the_default th th') end; + in (the_default th th', the_default x x') end; -fun attribute_declaration att th x = #1 (apply_attribute att (x, th)); +fun attribute_declaration att th x = #2 (apply_attribute att th x); fun apply_attributes mk dest = let - fun app [] = I - | app (att :: atts) = fn (x, th) => apply_attribute att (mk x, th) |>> dest |> app atts; + fun app [] th x = (th, x) + | app (att :: atts) th x = apply_attribute att th (mk x) ||> dest |-> app atts; in app end; val theory_attributes = apply_attributes Context.Theory Context.the_theory; diff -r 69b107201040 -r 3bbc156823dd src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Sat Mar 03 22:46:34 2012 +0100 +++ b/src/Pure/simplifier.ML Sat Mar 03 22:53:24 2012 +0100 @@ -315,7 +315,7 @@ (Args.context -- Scan.lift add_del) :|-- (fn (ctxt, decl) => Scan.repeat1 (Scan.lift (Args.named_attribute (decl o the_simproc ctxt o check_simproc ctxt)))) >> (fn atts => Thm.declaration_attribute (fn th => - Library.apply (map (fn att => Thm.attribute_declaration (Morphism.form att) th) atts))); + fold (fn att => Thm.attribute_declaration (Morphism.form att) th) atts)); end; diff -r 69b107201040 -r 3bbc156823dd src/Tools/IsaPlanner/isand.ML --- a/src/Tools/IsaPlanner/isand.ML Sat Mar 03 22:46:34 2012 +0100 +++ b/src/Tools/IsaPlanner/isand.ML Sat Mar 03 22:53:24 2012 +0100 @@ -270,7 +270,7 @@ (* make free vars into schematic vars with index zero *) fun unfix_frees frees = - apply (map (K (Thm.forall_elim_var 0)) frees) + fold (K (Thm.forall_elim_var 0)) frees o Drule.forall_intr_list frees; (* fix term and type variables *) diff -r 69b107201040 -r 3bbc156823dd src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Sat Mar 03 22:46:34 2012 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Sat Mar 03 22:53:24 2012 +0100 @@ -387,7 +387,7 @@ phase match { case Session.Failed => Swing_Thread.now { - val text = new scala.swing.TextArea(Isabelle.session.syslog()) + val text = new scala.swing.TextArea(Isabelle.session.current_syslog()) text.editable = false Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text) } diff -r 69b107201040 -r 3bbc156823dd src/Tools/jEdit/src/protocol_dockable.scala --- a/src/Tools/jEdit/src/protocol_dockable.scala Sat Mar 03 22:46:34 2012 +0100 +++ b/src/Tools/jEdit/src/protocol_dockable.scala Sat Mar 03 22:53:24 2012 +0100 @@ -31,14 +31,14 @@ case input: Isabelle_Process.Input => Swing_Thread.now { text_area.append(input.toString + "\n") } - case result: Isabelle_Process.Result => - Swing_Thread.now { text_area.append(result.message.toString + "\n") } + case output: Isabelle_Process.Output => + Swing_Thread.now { text_area.append(output.message.toString + "\n") } case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad) } } } - override def init() { Isabelle.session.protocol_messages += main_actor } - override def exit() { Isabelle.session.protocol_messages -= main_actor } + override def init() { Isabelle.session.all_messages += main_actor } + override def exit() { Isabelle.session.all_messages -= main_actor } } diff -r 69b107201040 -r 3bbc156823dd src/Tools/jEdit/src/raw_output_dockable.scala --- a/src/Tools/jEdit/src/raw_output_dockable.scala Sat Mar 03 22:46:34 2012 +0100 +++ b/src/Tools/jEdit/src/raw_output_dockable.scala Sat Mar 03 22:53:24 2012 +0100 @@ -29,9 +29,9 @@ private val main_actor = actor { loop { react { - case result: Isabelle_Process.Result => - if (result.is_stdout || result.is_stderr) - Swing_Thread.now { text_area.append(XML.content(result.message).mkString) } + case output: Isabelle_Process.Output => + if (output.is_stdout || output.is_stderr) + Swing_Thread.now { text_area.append(XML.content(output.message).mkString) } case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad) } diff -r 69b107201040 -r 3bbc156823dd src/Tools/jEdit/src/session_dockable.scala --- a/src/Tools/jEdit/src/session_dockable.scala Sat Mar 03 22:46:34 2012 +0100 +++ b/src/Tools/jEdit/src/session_dockable.scala Sat Mar 03 22:53:24 2012 +0100 @@ -43,7 +43,7 @@ status.peer.setLayoutOrientation(JList.VERTICAL_WRAP) status.selection.intervalMode = ListView.IntervalMode.Single - private val syslog = new TextArea(Isabelle.session.syslog()) + private val syslog = new TextArea(Isabelle.session.current_syslog()) private val tabs = new TabbedPane { pages += new TabbedPane.Page("README", Component.wrap(readme)) @@ -173,13 +173,11 @@ private val main_actor = actor { loop { react { - case result: Isabelle_Process.Result => - if (result.is_syslog) + case output: Isabelle_Process.Output => + if (output.is_syslog) Swing_Thread.now { - val text = Isabelle.session.syslog() - if (text != syslog.text) { - syslog.text = text - } + val text = Isabelle.session.current_syslog() + if (text != syslog.text) syslog.text = text } case phase: Session.Phase =>