# HG changeset patch # User wenzelm # Date 1325770458 -3600 # Node ID 1e9ec1a44dfcf3667e83b1fb025cea43f17fe257 # Parent 30a69cd8a9a0c9d539fceba286bb93bc0c3154ca prefer raw_message for protocol implementation; tuned; diff -r 30a69cd8a9a0 -r 1e9ec1a44dfc src/Pure/PIDE/isabelle_markup.ML --- 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")]; diff -r 30a69cd8a9a0 -r 1e9ec1a44dfc src/Pure/PIDE/isabelle_markup.scala --- 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 } } diff -r 30a69cd8a9a0 -r 1e9ec1a44dfc src/Pure/System/session.scala --- 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) } } diff -r 30a69cd8a9a0 -r 1e9ec1a44dfc src/Pure/Thy/thy_info.ML --- 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 *) diff -r 30a69cd8a9a0 -r 1e9ec1a44dfc src/Pure/Thy/thy_info.scala --- 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 */