--- 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 |>
--- 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 =
--- 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;
--- 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);
--- 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)
--- 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);
--- 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;
--- 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
--- 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"
--- 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)
--- 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 _ =
--- 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);
--- 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);
--- 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")
}
}
--- 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
--- 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 *)
--- 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);
--- 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 *)
--- 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;
--- 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;
--- 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 *)
--- 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)
}
--- 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 }
}
--- 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)
}
--- 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 =>