--- a/src/Pure/PIDE/isabelle_markup.ML Thu Jan 05 14:15:37 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.ML Thu Jan 05 14:34:18 2012 +0100
@@ -81,7 +81,6 @@
val command_spanN: string val command_span: string -> Markup.T
val ignored_spanN: string val ignored_span: Markup.T
val malformed_spanN: string val malformed_span: Markup.T
- val loaded_theoryN: string val loaded_theory: string -> Markup.T
val elapsedN: string
val cpuN: string
val gcN: string
@@ -105,6 +104,7 @@
val badN: string val bad: Markup.T
val functionN: string
val ready: Properties.T
+ val loaded_theory: string -> Properties.T
val assign_execs: Properties.T
val removed_versions: Properties.T
val invoke_scala: string -> string -> Properties.T
@@ -260,11 +260,6 @@
val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
-(* theory loader *)
-
-val (loaded_theoryN, loaded_theory) = markup_string "loaded_theory" Markup.nameN;
-
-
(* timing *)
val timingN = "timing";
@@ -320,6 +315,8 @@
val ready = [(functionN, "ready")];
+fun loaded_theory name = [(functionN, "loaded_theory"), (Markup.nameN, name)];
+
val assign_execs = [(functionN, "assign_execs")];
val removed_versions = [(functionN, "removed_versions")];
--- a/src/Pure/PIDE/isabelle_markup.scala Thu Jan 05 14:15:37 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.scala Thu Jan 05 14:34:18 2012 +0100
@@ -160,11 +160,6 @@
val MALFORMED_SPAN = "malformed_span"
- /* theory loader */
-
- val LOADED_THEORY = "loaded_theory"
-
-
/* timing */
val TIMING = "timing"
@@ -257,25 +252,31 @@
val Ready: Properties.T = List((FUNCTION, "ready"))
+ object Loaded_Theory
+ {
+ def unapply(props: Properties.T): Option[String] =
+ props match {
+ case List((FUNCTION, "loaded_theory"), (Markup.NAME, name)) => Some(name)
+ case _ => None
+ }
+ }
+
val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
- val INVOKE_SCALA = "invoke_scala"
object Invoke_Scala
{
def unapply(props: Properties.T): Option[(String, String)] =
props match {
- case List((FUNCTION, INVOKE_SCALA), (Markup.NAME, name), (ID, id)) => Some((name, id))
+ case List((FUNCTION, "invoke_scala"), (Markup.NAME, name), (ID, id)) => Some((name, id))
case _ => None
}
}
-
- val CANCEL_SCALA = "cancel_scala"
object Cancel_Scala
{
def unapply(props: Properties.T): Option[String] =
props match {
- case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
+ case List((FUNCTION, "cancel_scala"), (ID, id)) => Some(id)
case _ => None
}
}
--- a/src/Pure/System/session.scala Thu Jan 05 14:15:37 2012 +0100
+++ b/src/Pure/System/session.scala Thu Jan 05 14:34:18 2012 +0100
@@ -355,6 +355,7 @@
}
result.properties match {
+
case Position.Id(state_id) if !result.is_raw =>
try {
val st = global_state.change_yield(_.accumulate(state_id, result.message))
@@ -363,6 +364,7 @@
catch {
case _: Document.State.Fail => bad_result(result)
}
+
case Isabelle_Markup.Assign_Execs if result.is_raw =>
XML.content(result.body).mkString match {
case Protocol.Assign(id, assign) =>
@@ -376,6 +378,7 @@
if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
prune_next = System.currentTimeMillis() + prune_delay.ms
}
+
case Isabelle_Markup.Removed_Versions if result.is_raw =>
XML.content(result.body).mkString match {
case Protocol.Removed(removed) =>
@@ -383,19 +386,26 @@
catch { case _: Document.State.Fail => bad_result(result) }
case _ => bad_result(result)
}
+
case Isabelle_Markup.Invoke_Scala(name, id) if result.is_raw =>
Future.fork {
val arg = XML.content(result.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 =>
System.err.println("cancel_scala " + id) // FIXME actually cancel JVM task
+
case Isabelle_Markup.Ready if result.is_raw =>
// 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 =>
+ thy_load.register_thy(name)
+
case _ =>
if (result.is_syslog) {
reverse_syslog ::= result.message
@@ -407,7 +417,6 @@
result.body match {
case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
case List(Keyword.Keyword_Decl(name)) => syntax += name
- case List(Thy_Info.Loaded_Theory(name)) => thy_load.register_thy(name)
case _ => bad_result(result)
}
}
--- a/src/Pure/Thy/thy_info.ML Thu Jan 05 14:15:37 2012 +0100
+++ b/src/Pure/Thy/thy_info.ML Thu Jan 05 14:34:18 2012 +0100
@@ -89,7 +89,7 @@
fun get_names () = Graph.topological_order (get_thys ());
fun status () =
- List.app (Output.status o Markup.markup_only o Isabelle_Markup.loaded_theory) (get_names ());
+ List.app (fn name => Output.raw_message (Isabelle_Markup.loaded_theory name) "") (get_names ());
(* access thy *)
--- a/src/Pure/Thy/thy_info.scala Thu Jan 05 14:15:37 2012 +0100
+++ b/src/Pure/Thy/thy_info.scala Thu Jan 05 14:34:18 2012 +0100
@@ -7,21 +7,6 @@
package isabelle
-object Thy_Info
-{
- /* protocol messages */
-
- object Loaded_Theory {
- def unapply(msg: XML.Tree): Option[String] =
- msg match {
- case XML.Elem(Markup(Isabelle_Markup.LOADED_THEORY, List((Markup.NAME, name))), _) =>
- Some(name)
- case _ => None
- }
- }
-}
-
-
class Thy_Info(thy_load: Thy_Load)
{
/* messages */