# HG changeset patch # User wenzelm # Date 1253021839 -7200 # Node ID e3df9c8699ea0d3064367fbdb1996eeff7d7a851 # Parent 3ec545c964d5afe4f1305f0636b2cdc923d4f904 handle_result: no special treatment of outer markup (it is now properly identified by the prover); misc tuning; diff -r 3ec545c964d5 -r e3df9c8699ea src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala --- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Tue Sep 15 13:33:02 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Tue Sep 15 15:37:19 2009 +0200 @@ -97,11 +97,6 @@ def choose_color(kind: String, styles: Array[SyntaxStyle]): Color = styles(choose_byte(kind)).getForegroundColor - - private val outer: Set[String] = - Set(Markup.IDENT, Markup.COMMAND, Markup.KEYWORD, Markup.VERBATIM, Markup.COMMENT, - Markup.CONTROL, Markup.MALFORMED, Markup.STRING, Markup.ALTSTRING) - def is_outer(kind: String) = outer.contains(kind) } diff -r 3ec545c964d5 -r e3df9c8699ea src/Tools/jEdit/src/prover/Prover.scala --- a/src/Tools/jEdit/src/prover/Prover.scala Tue Sep 15 13:33:02 2009 +0200 +++ b/src/Tools/jEdit/src/prover/Prover.scala Tue Sep 15 15:37:19 2009 +0200 @@ -17,7 +17,7 @@ import isabelle.proofdocument.{ProofDocument, Change, Token} -class Prover(isabelle_system: Isabelle_System, logic: String) extends Actor +class Prover(system: Isabelle_System, logic: String) extends Actor { /* incoming messages */ @@ -43,8 +43,7 @@ /* prover process */ private val process = - new Isabelle_Process(isabelle_system, this, "-m", "xsymbols", logic) - with Isar_Document + new Isabelle_Process(system, this, "-m", "xsymbols", logic) with Isar_Document def stop() { process.kill } @@ -77,10 +76,15 @@ /* prover results */ - val output_text_view = new JTextArea + val output_text_view = new JTextArea // FIXME separate jEdit component private def handle_result(result: Isabelle_Process.Result) { + // FIXME separate jEdit component + Swing_Thread.later { output_text_view.append(result.toString + "\n") } + + val message = Isabelle_Process.parse_message(system, result) + val state = result.props.find(p => p._1 == Markup.ID) match { case None => None @@ -89,64 +93,48 @@ else if (states.contains(id)) Some(states(id)) else None } - Swing_Thread.later { output_text_view.append(result.toString + "\n") } // slow? - - val message = Isabelle_Process.parse_message(isabelle_system, result) - if (state.isDefined) state.get ! (this, message) - else result.kind match { - - case Isabelle_Process.Kind.STATUS => - //{{{ handle all kinds of status messages here - message match { - case XML.Elem(Markup.MESSAGE, _, elems) => - for (elem <- elems) { - elem match { - //{{{ - // command and keyword declarations - case XML.Elem(Markup.COMMAND_DECL, - (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) => - _command_decls += (name -> kind) - _completion += name - case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) => - _keyword_decls += name - _completion += name - - // process ready (after initialization) - case XML.Elem(Markup.READY, _, _) => prover_ready = true + else if (result.kind == Isabelle_Process.Kind.STATUS) { + //{{{ global status message + message match { + case XML.Elem(Markup.MESSAGE, _, elems) => + for (elem <- elems) { + elem match { + // document edits + case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) + if document_versions.exists(_.id == doc_id) => + val doc = document_versions.find(_.id == doc_id).get + for { + XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) + <- edits + } { + if (commands.contains(cmd_id)) { + val cmd = commands(cmd_id) + val state = new Command_State(cmd) + states += (state_id -> state) + doc.states += (cmd -> state) + command_change.event(cmd) + } + } + + // command and keyword declarations + case XML.Elem(Markup.COMMAND_DECL, + (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) => + _command_decls += (name -> kind) + _completion += name + case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) => + _keyword_decls += name + _completion += name - // document edits - case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) - if document_versions.exists(_.id == doc_id) => - val doc = document_versions.find(_.id == doc_id).get - for { - XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) - <- edits - } { - if (commands.contains(cmd_id)) { - val cmd = commands(cmd_id) - val state = new Command_State(cmd) - states += (state_id -> state) - doc.states += (cmd -> state) - command_change.event(cmd) - } - } - case XML.Elem(kind, attr, body) => - // TODO: This is mostly irrelevant information on removed commands, but it can - // also be outer-syntax-markup since there is no id in props (fix that?) - val (begin, end) = Position.offsets_of(attr) - val markup_id = Position.id_of(attr) - val outer = isabelle.jedit.DynamicTokenMarker.is_outer(kind) - if (outer && begin.isDefined && end.isDefined && markup_id.isDefined) - commands.get(markup_id.get).map(cmd => cmd ! (this, message)) - case _ => - //}}} - } + // process ready (after initialization) + case XML.Elem(Markup.READY, _, _) => prover_ready = true + + case _ => } - case _ => - } - //}}} - case _ => + } + case _ => + } + //}}} } } @@ -172,10 +160,10 @@ (c1.map(_.id).getOrElse(document_0.id), c2 match { case None => None - case Some(cmd) => - commands += (cmd.id -> cmd) - process.define_command(cmd.id, isabelle_system.symbols.encode(cmd.content)) - Some(cmd.id) + case Some(command) => + commands += (command.id -> command) + process.define_command(command.id, system.symbols.encode(command.content)) + Some(command.id) }) } process.edit_document(old.id, doc.id, id_changes)