# HG changeset patch # User wenzelm # Date 1376049441 -7200 # Node ID 551d09fc245c24b4da18daf36fa19d7e9960c217 # Parent 9587134ec780e453856ab12c43b683467de4291c# Parent 6fc13c31c775ce4e7b06640bdbbca88a1a20c878 merged; diff -r 9587134ec780 -r 551d09fc245c src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Fri Aug 09 12:27:29 2013 +0200 +++ b/src/Pure/PIDE/command.scala Fri Aug 09 13:57:21 2013 +0200 @@ -111,10 +111,9 @@ // FIXME java.lang.System.err.println("Ignored report message: " + msg) state }) - case XML.Elem(Markup(name, atts), body) => - atts match { + case XML.Elem(Markup(name, props), body) => + props match { case Markup.Serial(i) => - val props = Position.purge(atts) val message1 = XML.Elem(Markup(Markup.message(name), props), body) val message2 = XML.Elem(Markup(name, props), body) diff -r 9587134ec780 -r 551d09fc245c src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Fri Aug 09 12:27:29 2013 +0200 +++ b/src/Pure/PIDE/protocol.ML Fri Aug 09 13:57:21 2013 +0200 @@ -32,6 +32,10 @@ (fn [] => Execution.discontinue ()); val _ = + Isabelle_Process.protocol_command "Document.cancel_exec" + (fn [exec_id] => Execution.cancel (Document_ID.parse exec_id)); + +val _ = Isabelle_Process.protocol_command "Document.update" (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state => let diff -r 9587134ec780 -r 551d09fc245c src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Fri Aug 09 12:27:29 2013 +0200 +++ b/src/Pure/PIDE/protocol.scala Fri Aug 09 13:57:21 2013 +0200 @@ -315,9 +315,16 @@ Document_ID(command.id), encode(command.name), encode(command.source)) - /* document versions */ + /* execution */ + + def discontinue_execution(): Unit = + protocol_command("Document.discontinue_execution") - def discontinue_execution() { protocol_command("Document.discontinue_execution") } + def cancel_exec(id: Document_ID.Exec): Unit = + protocol_command("Document.cancel_exec", Document_ID(id)) + + + /* document versions */ def update(old_id: Document_ID.Version, new_id: Document_ID.Version, edits: List[Document.Edit_Command]) @@ -363,8 +370,6 @@ /* dialog via document content */ - def dialog_result(serial: Long, result: String) - { + def dialog_result(serial: Long, result: String): Unit = protocol_command("Document.dialog_result", Properties.Value.Long(serial), result) - } } diff -r 9587134ec780 -r 551d09fc245c src/Pure/PIDE/query_operation.ML --- a/src/Pure/PIDE/query_operation.ML Fri Aug 09 12:27:29 2013 +0200 +++ b/src/Pure/PIDE/query_operation.ML Fri Aug 09 13:57:21 2013 +0200 @@ -18,25 +18,23 @@ Command.print_function name (fn {args = instance :: args, ...} => SOME {delay = NONE, pri = 0, persistent = false, - print_fn = fn _ => fn state => + print_fn = fn _ => uninterruptible (fn restore_attributes => fn state => let fun result s = Output.result [(Markup.instanceN, instance)] s; fun status m = result (Markup.markup_only m); - fun error_msg exn = - if Exn.is_interrupt exn then reraise exn - else - XML.Elem ((Markup.errorN, []), [XML.Text (ML_Compiler.exn_message exn)]) - |> YXML.string_of |> result; + fun toplevel_error exn = + result (Markup.markup (Markup.errorN, []) (ML_Compiler.exn_message exn)); val _ = status Markup.running; - val outputs = f state args handle exn => (error_msg exn; []); + val outputs = + Multithreading.interruptible (fn () => f state args) () + handle exn (*sic!*) => (toplevel_error exn; []); val _ = outputs |> Par_List.map (fn out => - (case Exn.capture out () of - Exn.Res s => - result (YXML.string_of (XML.Elem ((Markup.writelnN, []), [XML.Text s]))) - | Exn.Exn exn => error_msg exn)); + (case Exn.capture (restore_attributes out) () (*sic!*) of + Exn.Res s => result (Markup.markup (Markup.writelnN, []) s) + | Exn.Exn exn => toplevel_error exn)); val _ = status Markup.finished; - in () end} + in () end)} | _ => NONE); fun register name f = diff -r 9587134ec780 -r 551d09fc245c src/Pure/ROOT --- a/src/Pure/ROOT Fri Aug 09 12:27:29 2013 +0200 +++ b/src/Pure/ROOT Fri Aug 09 13:57:21 2013 +0200 @@ -201,7 +201,6 @@ "Thy/thy_output.ML" "Thy/thy_syntax.ML" "Tools/build.ML" - "Tools/legacy_xml_syntax.ML" "Tools/named_thms.ML" "Tools/proof_general.ML" "assumption.ML" diff -r 9587134ec780 -r 551d09fc245c src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Aug 09 12:27:29 2013 +0200 +++ b/src/Pure/ROOT.ML Fri Aug 09 13:57:21 2013 +0200 @@ -302,7 +302,6 @@ use "Tools/build.ML"; use "Tools/named_thms.ML"; use "Tools/proof_general.ML"; -use "Tools/legacy_xml_syntax.ML"; (* ML toplevel pretty printing *) diff -r 9587134ec780 -r 551d09fc245c src/Pure/System/session.scala --- a/src/Pure/System/session.scala Fri Aug 09 12:27:29 2013 +0200 +++ b/src/Pure/System/session.scala Fri Aug 09 13:57:21 2013 +0200 @@ -238,6 +238,7 @@ /* actor messages */ private case class Start(args: List[String]) + private case class Cancel_Exec(exec_id: Document_ID.Exec) private case class Change( doc_edits: List[Document.Edit_Command], previous: Document.Version, @@ -506,6 +507,9 @@ global_options.event(Session.Global_Options(options)) reply(()) + case Cancel_Exec(exec_id) if prover.isDefined => + prover.get.cancel_exec(exec_id) + case Session.Raw_Edits(edits) if prover.isDefined => handle_raw_edits(edits) reply(()) @@ -552,6 +556,8 @@ session_actor !? Stop } + def cancel_exec(exec_id: Document_ID.Exec) { session_actor ! Cancel_Exec(exec_id) } + def update(edits: List[Document.Edit_Text]) { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(edits) } diff -r 9587134ec780 -r 551d09fc245c src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Fri Aug 09 12:27:29 2013 +0200 +++ b/src/Pure/Tools/find_theorems.ML Fri Aug 09 13:57:21 2013 +0200 @@ -21,12 +21,7 @@ } val read_criterion: Proof.context -> string criterion -> term criterion - val parse_query: string -> (bool * string criterion) list - - val xml_of_query: term query -> XML.tree - val query_of_xml: XML.tree -> term query - val xml_of_result: int option * theorem list -> XML.tree - val result_of_xml: XML.tree -> int option * theorem list + val read_query: Position.T -> string -> (bool * string criterion) list val find_theorems: Proof.context -> thm option -> int option -> bool -> (bool * term criterion) list -> int option * (Facts.ref * thm) list @@ -40,7 +35,6 @@ val pretty_theorem: Proof.context -> theorem -> Pretty.T val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T - end; structure Find_Theorems: FIND_THEOREMS = @@ -108,46 +102,6 @@ fun map_criteria f {goal, limit, rem_dups, criteria} = {goal = goal, limit = limit, rem_dups = rem_dups, criteria = f criteria}; -fun xml_of_criterion (Name name) = XML.Elem (("Name", [("val", name)]), []) - | xml_of_criterion Intro = XML.Elem (("Intro", []) , []) - | xml_of_criterion Elim = XML.Elem (("Elim", []) , []) - | xml_of_criterion Dest = XML.Elem (("Dest", []) , []) - | xml_of_criterion Solves = XML.Elem (("Solves", []) , []) - | xml_of_criterion (Simp pat) = XML.Elem (("Simp", []), [Legacy_XML_Syntax.xml_of_term pat]) - | xml_of_criterion (Pattern pat) = XML.Elem (("Pattern", []), [Legacy_XML_Syntax.xml_of_term pat]); - -fun criterion_of_xml (XML.Elem (("Name", [("val", name)]), [])) = Name name - | criterion_of_xml (XML.Elem (("Intro", []) , [])) = Intro - | criterion_of_xml (XML.Elem (("Elim", []) , [])) = Elim - | criterion_of_xml (XML.Elem (("Dest", []) , [])) = Dest - | criterion_of_xml (XML.Elem (("Solves", []) , [])) = Solves - | criterion_of_xml (XML.Elem (("Simp", []), [tree])) = Simp (Legacy_XML_Syntax.term_of_xml tree) - | criterion_of_xml (XML.Elem (("Pattern", []), [tree])) = Pattern (Legacy_XML_Syntax.term_of_xml tree) - | criterion_of_xml tree = raise Legacy_XML_Syntax.XML ("criterion_of_xml: bad tree", tree); - -fun xml_of_query {goal = NONE, limit, rem_dups, criteria} = - let - val properties = [] - |> (if rem_dups then cons ("rem_dups", "") else I) - |> (if is_some limit then cons ("limit", Markup.print_int (the limit)) else I); - in - XML.Elem (("Query", properties), XML.Encode.list - (XML.Encode.pair XML.Encode.bool (single o xml_of_criterion)) criteria) - end - | xml_of_query _ = raise Fail "cannot serialize goal"; - -fun query_of_xml (XML.Elem (("Query", properties), body)) = - let - val rem_dups = Properties.defined properties "rem_dups"; - val limit = Properties.get properties "limit" |> Option.map Markup.parse_int; - val criteria = - XML.Decode.list (XML.Decode.pair XML.Decode.bool - (criterion_of_xml o the_single)) body; - in - {goal = NONE, limit = limit, rem_dups = rem_dups, criteria = criteria} - end - | query_of_xml tree = raise Legacy_XML_Syntax.XML ("query_of_xml: bad tree", tree); - (** theorems, either internal or external (without proof) **) @@ -162,35 +116,6 @@ Position.markup pos o Markup.properties [("name", name)] | fact_ref_markup fact_ref = raise Fail "bad fact ref"; -fun xml_of_theorem (Internal _) = raise Fail "xml_of_theorem: Internal" - | xml_of_theorem (External (fact_ref, prop)) = - XML.Elem (fact_ref_markup fact_ref ("External", []), [Legacy_XML_Syntax.xml_of_term prop]); - -fun theorem_of_xml (XML.Elem (("External", properties), [tree])) = - let - val name = the (Properties.get properties "name"); - val pos = Position.of_properties properties; - val intvs_opt = - Option.map (single o Facts.Single o Markup.parse_int) - (Properties.get properties "index"); - in - External (Facts.Named ((name, pos), intvs_opt), Legacy_XML_Syntax.term_of_xml tree) - end - | theorem_of_xml tree = raise Legacy_XML_Syntax.XML ("theorem_of_xml: bad tree", tree); - -fun xml_of_result (opt_found, theorems) = - let - val properties = - if is_some opt_found then [("found", Markup.print_int (the opt_found))] else []; - in - XML.Elem (("Result", properties), XML.Encode.list (single o xml_of_theorem) theorems) - end; - -fun result_of_xml (XML.Elem (("Result", properties), body)) = - (Properties.get properties "found" |> Option.map Markup.parse_int, - XML.Decode.list (theorem_of_xml o the_single) body) - | result_of_xml tree = raise Legacy_XML_Syntax.XML ("result_of_xml: bad tree", tree); - fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm | prop_of (External (_, prop)) = prop; @@ -594,7 +519,7 @@ (if null theorems then [Pretty.str "nothing found"] else [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @ - grouped 10 Par_List.map (pretty_theorem ctxt) theorems) + grouped 10 Par_List.map (Pretty.item o single o pretty_theorem ctxt) theorems) end |> Pretty.fbreaks |> curry Pretty.blk 0; fun pretty_theorems_cmd state opt_lim rem_dups spec = @@ -624,22 +549,20 @@ Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true --| Parse.$$$ ")")) (NONE, true); -val query_parser = Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion)); +val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion); in -(* FIXME proper wrapper for parser combinator *) -fun parse_query str = - (str ^ ";") - |> Outer_Syntax.scan Position.start +fun read_query pos str = + Outer_Syntax.scan pos str |> filter Token.is_proper - |> Scan.error query_parser - |> fst; + |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof))) + |> #1; val _ = Outer_Syntax.improper_command @{command_spec "find_theorems"} "find theorems meeting specified criteria" - (options -- query_parser >> (fn ((opt_lim, rem_dups), spec) => + (options -- query >> (fn ((opt_lim, rem_dups), spec) => Toplevel.keep (fn state => Pretty.writeln (pretty_theorems_cmd state opt_lim rem_dups spec)))); @@ -650,7 +573,9 @@ (** PIDE query operation **) val _ = - Query_Operation.register "find_theorems" (fn state => fn query => - Pretty.string_of (pretty_theorems_cmd state NONE false (maps parse_query query))); + Query_Operation.register "find_theorems" (fn st => fn args => + if can Toplevel.theory_of st then + Pretty.string_of (pretty_theorems_cmd st NONE false (maps (read_query Position.none) args)) + else error "Unknown theory context"); end; diff -r 9587134ec780 -r 551d09fc245c src/Pure/Tools/isabelle.xsd --- a/src/Pure/Tools/isabelle.xsd Fri Aug 09 12:27:29 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,193 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff -r 9587134ec780 -r 551d09fc245c src/Pure/Tools/legacy_xml_syntax.ML --- a/src/Pure/Tools/legacy_xml_syntax.ML Fri Aug 09 12:27:29 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,173 +0,0 @@ -(* Title: Pure/Tools/legacy_xml_syntax.ML - Author: Stefan Berghofer, TU Muenchen - -Input and output of types, terms, and proofs in XML format. -See isabelle.xsd for a description of the syntax. - -Legacy module, see Pure/term_xml.ML etc. -*) - -signature LEGACY_XML_SYNTAX = -sig - val xml_of_type: typ -> XML.tree - val xml_of_term: term -> XML.tree - val xml_of_proof: Proofterm.proof -> XML.tree - val write_to_file: Path.T -> string -> XML.tree -> unit - exception XML of string * XML.tree - val type_of_xml: XML.tree -> typ - val term_of_xml: XML.tree -> term - val proof_of_xml: XML.tree -> Proofterm.proof -end; - -structure Legacy_XML_Syntax : LEGACY_XML_SYNTAX = -struct - -(**** XML output ****) - -fun xml_of_class name = XML.Elem (("class", [("name", name)]), []); - -fun xml_of_type (TVar ((s, i), S)) = - XML.Elem (("TVar", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])), - map xml_of_class S) - | xml_of_type (TFree (s, S)) = - XML.Elem (("TFree", [("name", s)]), map xml_of_class S) - | xml_of_type (Type (s, Ts)) = - XML.Elem (("Type", [("name", s)]), map xml_of_type Ts); - -fun xml_of_term (Bound i) = - XML.Elem (("Bound", [("index", string_of_int i)]), []) - | xml_of_term (Free (s, T)) = - XML.Elem (("Free", [("name", s)]), [xml_of_type T]) - | xml_of_term (Var ((s, i), T)) = - XML.Elem (("Var", ("name", s) :: (if i=0 then [] else [("index", string_of_int i)])), - [xml_of_type T]) - | xml_of_term (Const (s, T)) = - XML.Elem (("Const", [("name", s)]), [xml_of_type T]) - | xml_of_term (t $ u) = - XML.Elem (("App", []), [xml_of_term t, xml_of_term u]) - | xml_of_term (Abs (s, T, t)) = - XML.Elem (("Abs", [("vname", s)]), [xml_of_type T, xml_of_term t]); - -fun xml_of_opttypes NONE = [] - | xml_of_opttypes (SOME Ts) = [XML.Elem (("types", []), map xml_of_type Ts)]; - -(* FIXME: the t argument of PThm and PAxm is actually redundant, since *) -(* it can be looked up in the theorem database. Thus, it could be *) -(* omitted from the xml representation. *) - -(* FIXME not exhaustive *) -fun xml_of_proof (PBound i) = - XML.Elem (("PBound", [("index", string_of_int i)]), []) - | xml_of_proof (Abst (s, optT, prf)) = - XML.Elem (("Abst", [("vname", s)]), - (case optT of NONE => [] | SOME T => [xml_of_type T]) @ [xml_of_proof prf]) - | xml_of_proof (AbsP (s, optt, prf)) = - XML.Elem (("AbsP", [("vname", s)]), - (case optt of NONE => [] | SOME t => [xml_of_term t]) @ [xml_of_proof prf]) - | xml_of_proof (prf % optt) = - XML.Elem (("Appt", []), - xml_of_proof prf :: (case optt of NONE => [] | SOME t => [xml_of_term t])) - | xml_of_proof (prf %% prf') = - XML.Elem (("AppP", []), [xml_of_proof prf, xml_of_proof prf']) - | xml_of_proof (Hyp t) = XML.Elem (("Hyp", []), [xml_of_term t]) - | xml_of_proof (PThm (_, ((s, t, optTs), _))) = - XML.Elem (("PThm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs) - | xml_of_proof (PAxm (s, t, optTs)) = - XML.Elem (("PAxm", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs) - | xml_of_proof (Oracle (s, t, optTs)) = - XML.Elem (("Oracle", [("name", s)]), xml_of_term t :: xml_of_opttypes optTs) - | xml_of_proof MinProof = - XML.Elem (("MinProof", []), []); - - -(* useful for checking the output against a schema file *) - -fun write_to_file path elname x = - File.write path - ("\n" ^ - XML.string_of (XML.Elem ((elname, - [("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance"), - ("xsi:noNamespaceSchemaLocation", "isabelle.xsd")]), - [x]))); - - - -(**** XML input ****) - -exception XML of string * XML.tree; - -fun class_of_xml (XML.Elem (("class", [("name", name)]), [])) = name - | class_of_xml tree = raise XML ("class_of_xml: bad tree", tree); - -fun index_of_string s tree idx = - (case Int.fromString idx of - NONE => raise XML (s ^ ": bad index", tree) - | SOME i => i); - -fun type_of_xml (tree as XML.Elem (("TVar", atts), classes)) = TVar - ((case Properties.get atts "name" of - NONE => raise XML ("type_of_xml: name of TVar missing", tree) - | SOME name => name, - the_default 0 (Option.map (index_of_string "type_of_xml" tree) - (Properties.get atts "index"))), - map class_of_xml classes) - | type_of_xml (XML.Elem (("TFree", [("name", s)]), classes)) = - TFree (s, map class_of_xml classes) - | type_of_xml (XML.Elem (("Type", [("name", s)]), types)) = - Type (s, map type_of_xml types) - | type_of_xml tree = raise XML ("type_of_xml: bad tree", tree); - -fun term_of_xml (tree as XML.Elem (("Bound", [("index", idx)]), [])) = - Bound (index_of_string "bad variable index" tree idx) - | term_of_xml (XML.Elem (("Free", [("name", s)]), [typ])) = - Free (s, type_of_xml typ) - | term_of_xml (tree as XML.Elem (("Var", atts), [typ])) = Var - ((case Properties.get atts "name" of - NONE => raise XML ("type_of_xml: name of Var missing", tree) - | SOME name => name, - the_default 0 (Option.map (index_of_string "term_of_xml" tree) - (Properties.get atts "index"))), - type_of_xml typ) - | term_of_xml (XML.Elem (("Const", [("name", s)]), [typ])) = - Const (s, type_of_xml typ) - | term_of_xml (XML.Elem (("App", []), [term, term'])) = - term_of_xml term $ term_of_xml term' - | term_of_xml (XML.Elem (("Abs", [("vname", s)]), [typ, term])) = - Abs (s, type_of_xml typ, term_of_xml term) - | term_of_xml tree = raise XML ("term_of_xml: bad tree", tree); - -fun opttypes_of_xml [] = NONE - | opttypes_of_xml [XML.Elem (("types", []), types)] = - SOME (map type_of_xml types) - | opttypes_of_xml (tree :: _) = raise XML ("opttypes_of_xml: bad tree", tree); - -fun proof_of_xml (tree as XML.Elem (("PBound", [("index", idx)]), [])) = - PBound (index_of_string "proof_of_xml" tree idx) - | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [proof])) = - Abst (s, NONE, proof_of_xml proof) - | proof_of_xml (XML.Elem (("Abst", [("vname", s)]), [typ, proof])) = - Abst (s, SOME (type_of_xml typ), proof_of_xml proof) - | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [proof])) = - AbsP (s, NONE, proof_of_xml proof) - | proof_of_xml (XML.Elem (("AbsP", [("vname", s)]), [term, proof])) = - AbsP (s, SOME (term_of_xml term), proof_of_xml proof) - | proof_of_xml (XML.Elem (("Appt", []), [proof])) = - proof_of_xml proof % NONE - | proof_of_xml (XML.Elem (("Appt", []), [proof, term])) = - proof_of_xml proof % SOME (term_of_xml term) - | proof_of_xml (XML.Elem (("AppP", []), [proof, proof'])) = - proof_of_xml proof %% proof_of_xml proof' - | proof_of_xml (XML.Elem (("Hyp", []), [term])) = - Hyp (term_of_xml term) - | proof_of_xml (XML.Elem (("PThm", [("name", s)]), term :: opttypes)) = - (* FIXME? *) - PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes), - Future.value (Proofterm.approximate_proof_body MinProof))) - | proof_of_xml (XML.Elem (("PAxm", [("name", s)]), term :: opttypes)) = - PAxm (s, term_of_xml term, opttypes_of_xml opttypes) - | proof_of_xml (XML.Elem (("Oracle", [("name", s)]), term :: opttypes)) = - Oracle (s, term_of_xml term, opttypes_of_xml opttypes) - | proof_of_xml (XML.Elem (("MinProof", _), _)) = MinProof - | proof_of_xml tree = raise XML ("proof_of_xml: bad tree", tree); - -end; diff -r 9587134ec780 -r 551d09fc245c src/Tools/WWW_Find/Start_WWW_Find.thy --- a/src/Tools/WWW_Find/Start_WWW_Find.thy Fri Aug 09 12:27:29 2013 +0200 +++ b/src/Tools/WWW_Find/Start_WWW_Find.thy Fri Aug 09 13:57:21 2013 +0200 @@ -5,7 +5,6 @@ theory Start_WWW_Find imports WWW_Find begin ML {* - YXML_Find_Theorems.init (); val port = Markup.parse_int (getenv "SCGIPORT"); ScgiServer.server' 10 "/" port; *} diff -r 9587134ec780 -r 551d09fc245c src/Tools/WWW_Find/WWW_Find.thy --- a/src/Tools/WWW_Find/WWW_Find.thy Fri Aug 09 12:27:29 2013 +0200 +++ b/src/Tools/WWW_Find/WWW_Find.thy Fri Aug 09 13:57:21 2013 +0200 @@ -14,7 +14,6 @@ ML_file "echo.ML" ML_file "html_templates.ML" ML_file "find_theorems.ML" -ML_file "yxml_find_theorems.ML" end diff -r 9587134ec780 -r 551d09fc245c src/Tools/WWW_Find/find_theorems.ML --- a/src/Tools/WWW_Find/find_theorems.ML Fri Aug 09 12:27:29 2013 +0200 +++ b/src/Tools/WWW_Find/find_theorems.ML Fri Aug 09 13:57:21 2013 +0200 @@ -16,7 +16,7 @@ val args = Symtab.lookup arg_data; val query_str = the_default "" (args "query"); - fun get_query () = Find_Theorems.parse_query query_str; + fun get_query () = Find_Theorems.read_query Position.none query_str; val limit = case args "limit" of NONE => default_limit diff -r 9587134ec780 -r 551d09fc245c src/Tools/WWW_Find/yxml_find_theorems.ML --- a/src/Tools/WWW_Find/yxml_find_theorems.ML Fri Aug 09 12:27:29 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,47 +0,0 @@ -(* Title: Tools/WWW_Find/yxml_find_theorems.ML - Author: Sree Harsha Totakura, TUM - Author: Lars Noschinski, TUM - Author: Alexander Krauss, TUM - -Simple find theorems web service with yxml interface for programmatic -invocation. -*) - -signature YXML_FIND_THEOREMS = -sig - val init: unit -> unit -end - - -structure YXML_Find_Theorems : YXML_FIND_THEOREMS = -struct - -val the_theory = "Main"; (* FIXME!!! EXPERIMENTAL *) - -fun yxml_find_theorems theorem_list yxml_query = - let - val ctxt = Proof_Context.init_global (Thy_Info.get_theory the_theory); - in - Find_Theorems.query_of_xml (YXML.parse yxml_query) - |> Find_Theorems.filter_theorems ctxt theorem_list - ||> rev o (filter (fn Find_Theorems.External x => true | _ => false)) - |> Find_Theorems.xml_of_result |> YXML.string_of - end; - -fun visible_facts facts = - Facts.dest_static [] facts - |> filter_out (Facts.is_concealed facts o #1); - -fun init () = - let - val all_facts = - maps Facts.selections - (visible_facts (Global_Theory.facts_of (Thy_Info.get_theory the_theory))) - |> map (Find_Theorems.External o apsnd prop_of); - in - ScgiServer.register ("yxml_find_theorems", SOME Mime.html (*FIXME?*), - ScgiServer.raw_post_handler (yxml_find_theorems all_facts)) - end; - -end; - diff -r 9587134ec780 -r 551d09fc245c src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Fri Aug 09 12:27:29 2013 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Fri Aug 09 13:57:21 2013 +0200 @@ -34,6 +34,7 @@ "src/plugin.scala" "src/pretty_text_area.scala" "src/pretty_tooltip.scala" + "src/process_indicator.scala" "src/protocol_dockable.scala" "src/query_operation.scala" "src/raw_output_dockable.scala" diff -r 9587134ec780 -r 551d09fc245c src/Tools/jEdit/src/find_dockable.scala --- a/src/Tools/jEdit/src/find_dockable.scala Fri Aug 09 12:27:29 2013 +0200 +++ b/src/Tools/jEdit/src/find_dockable.scala Fri Aug 09 13:57:21 2013 +0200 @@ -31,8 +31,22 @@ /* query operation */ + private val process_indicator = new Process_Indicator + + private def consume_status(status: Query_Operation.Status.Value) + { + status match { + case Query_Operation.Status.WAITING => + process_indicator.update("Waiting for evaluation of context ...", 5) + case Query_Operation.Status.RUNNING => + process_indicator.update("Running find operation ...", 15) + case Query_Operation.Status.FINISHED => + process_indicator.update(null, 0) + } + } + private val find_theorems = - Query_Operation(view, "find_theorems", + Query_Operation(view, "find_theorems", consume_status _, (snapshot, results, body) => pretty_text_area.update(snapshot, results, Pretty.separate(body))) @@ -121,6 +135,6 @@ private val controls = new FlowPanel(FlowPanel.Alignment.Right)( - query_wrapped, find_theorems.animation, apply_query, locate_query, zoom) + query_wrapped, process_indicator.component, apply_query, locate_query, zoom) add(controls.peer, BorderLayout.NORTH) } diff -r 9587134ec780 -r 551d09fc245c src/Tools/jEdit/src/process_indicator.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/process_indicator.scala Fri Aug 09 13:57:21 2013 +0200 @@ -0,0 +1,65 @@ +/* Title: Tools/jEdit/src/process_indicator.scala + Author: Makarius + +Process indicator with animated icon. +*/ + +package isabelle.jedit + + +import isabelle._ + +import java.awt.Image +import java.awt.event.{ActionListener, ActionEvent} +import javax.swing.{ImageIcon, Timer} +import scala.swing.{Label, Component} + + +class Process_Indicator +{ + private val label = new Label + + private val passive_icon = + JEdit_Lib.load_image_icon(PIDE.options.string("process_passive_icon")).getImage + private val active_icons = + space_explode(':', PIDE.options.string("process_active_icons")).map(name => + JEdit_Lib.load_image_icon(name).getImage) + + private val animation = new ImageIcon(passive_icon) { + private var current_frame = 0 + private val timer = + new Timer(0, new ActionListener { + override def actionPerformed(e: ActionEvent) { + current_frame = (current_frame + 1) % active_icons.length + setImage(active_icons(current_frame)) + label.repaint + } + }) + timer.setRepeats(true) + + def update(rate: Int) + { + if (rate == 0) { + setImage(passive_icon) + timer.stop + label.repaint + } + else { + val delay = 1000 / rate + timer.setInitialDelay(delay) + timer.setDelay(delay) + timer.restart + } + } + } + label.icon = animation + + def component: Component = label + + def update(tip: String, rate: Int) + { + label.tooltip = tip + animation.update(rate) + } +} + diff -r 9587134ec780 -r 551d09fc245c src/Tools/jEdit/src/query_operation.scala --- a/src/Tools/jEdit/src/query_operation.scala Fri Aug 09 12:27:29 2013 +0200 +++ b/src/Tools/jEdit/src/query_operation.scala Fri Aug 09 13:57:21 2013 +0200 @@ -2,7 +2,7 @@ Author: Makarius One-shot query operations via asynchronous print functions and temporary -document overlay. +document overlays. */ package isabelle.jedit @@ -11,43 +11,44 @@ import isabelle._ import scala.actors.Actor._ -import scala.swing.Label import org.gjt.sp.jedit.View -import org.gjt.sp.jedit.gui.AnimatedIcon object Query_Operation { + object Status extends Enumeration + { + val WAITING = Value("waiting") + val RUNNING = Value("running") + val FINISHED = Value("finished") + } + def apply( view: View, - name: String, - consume: (Document.Snapshot, Command.Results, XML.Body) => Unit) = - new Query_Operation(view, name, consume) + operation_name: String, + consume_status: Status.Value => Unit, + consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit) = + new Query_Operation(view, operation_name, consume_status, consume_output) } final class Query_Operation private( view: View, operation_name: String, - consume_result: (Document.Snapshot, Command.Results, XML.Body) => Unit) + consume_status: Query_Operation.Status.Value => Unit, + consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit) { private val instance = Document_ID.make().toString /* implicit state -- owned by Swing thread */ - private object Status extends Enumeration - { - val WAITING = Value("waiting") - val RUNNING = Value("running") - val FINISHED = Value("finished") - } - private var current_location: Option[Command] = None private var current_query: List[String] = Nil private var current_update_pending = false private var current_output: List[XML.Tree] = Nil - private var current_status = Status.FINISHED + private var current_status = Query_Operation.Status.FINISHED + private var current_exec_id = Document_ID.none private def reset_state() { @@ -55,7 +56,8 @@ current_query = Nil current_update_pending = false current_output = Nil - current_status = Status.FINISHED + current_status = Query_Operation.Status.FINISHED + current_exec_id = Document_ID.none } private def remove_overlay() @@ -70,38 +72,6 @@ } - /* animation */ - - val animation = new Label - - private val passive_icon = - JEdit_Lib.load_image_icon(PIDE.options.string("process_passive_icon")).getImage - private val active_icons = - space_explode(':', PIDE.options.string("process_active_icons")).map(name => - JEdit_Lib.load_image_icon(name).getImage) - - private val animation_icon = - new AnimatedIcon(passive_icon, active_icons.toArray, 5, animation.peer) - animation.icon = animation_icon - - private def animation_update() - { - animation_icon.stop - current_status match { - case Status.WAITING => - animation.tooltip = "Waiting for evaluation of query context ..." - animation_icon.setRate(5) - animation_icon.start - case Status.RUNNING => - animation.tooltip = "Running query operation ..." - animation_icon.setRate(15) - animation_icon.start - case Status.FINISHED => - animation.tooltip = null - } - } - - /* content update */ private def content_update() @@ -111,42 +81,52 @@ /* snapshot */ - val (snapshot, state) = + val (snapshot, state, removed) = current_location match { case Some(cmd) => val snapshot = PIDE.document_snapshot(cmd.node_name) val state = snapshot.state.command_state(snapshot.version, cmd) - (snapshot, state) + val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd) + (snapshot, state, removed) case None => - (Document.State.init.snapshot(), Command.empty.init_state) + (Document.State.init.snapshot(), Command.empty.init_state, true) } val results = (for { - (_, XML.Elem(Markup(Markup.RESULT, props), body)) <- state.results.entries + (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- state.results.entries if props.contains((Markup.INSTANCE, instance)) - } yield body).toList + } yield elem).toList /* output */ val new_output = for { - List(XML.Elem(markup, body)) <- results + XML.Elem(_, List(XML.Elem(markup, body))) <- results if Markup.messages.contains(markup.name) - } - yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body) + } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body) /* status */ - def get_status(name: String, status: Status.Value): Option[Status.Value] = - results.collectFirst({ case List(elem: XML.Elem) if elem.name == name => status }) + def get_status(name: String, status: Query_Operation.Status.Value) + : Option[Query_Operation.Status.Value] = + results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status }) val new_status = - get_status(Markup.FINISHED, Status.FINISHED) orElse - get_status(Markup.RUNNING, Status.RUNNING) getOrElse - Status.WAITING + if (removed) Query_Operation.Status.FINISHED + else + get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse + get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse + Query_Operation.Status.WAITING + + if (new_status == Query_Operation.Status.RUNNING) + results.collectFirst( + { + case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem)) + if elem.name == Markup.RUNNING => id + }).foreach(id => current_exec_id = id) /* state update */ @@ -156,14 +136,14 @@ current_update_pending = true else { current_update_pending = false - if (current_output != new_output) { + if (current_output != new_output && !removed) { current_output = new_output - consume_result(snapshot, state.results, new_output) + consume_output(snapshot, state.results, new_output) } if (current_status != new_status) { current_status = new_status - animation_update() - if (new_status == Status.FINISHED) { + consume_status(new_status) + if (new_status == Query_Operation.Status.FINISHED) { remove_overlay() PIDE.flush_buffers() } @@ -173,7 +153,10 @@ } - /* apply query */ + /* query operations */ + + def cancel_query(): Unit = + Swing_Thread.require { PIDE.session.cancel_exec(current_exec_id) } def apply_query(query: List[String]) { @@ -184,23 +167,21 @@ val snapshot = doc_view.model.snapshot() remove_overlay() reset_state() + consume_output(Document.State.init.snapshot(), Command.Results.empty, Nil) snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match { case Some(command) => current_location = Some(command) current_query = query - current_status = Status.WAITING + current_status = Query_Operation.Status.WAITING doc_view.model.insert_overlay(command, operation_name, instance :: query) case None => } - animation_update() + consume_status(current_status) PIDE.flush_buffers() case None => } } - - /* locate query */ - def locate_query() { Swing_Thread.require() @@ -229,7 +210,8 @@ current_location match { case Some(command) if current_update_pending || - (current_status != Status.FINISHED && changed.commands.contains(command)) => + (current_status != Query_Operation.Status.FINISHED && + changed.commands.contains(command)) => Swing_Thread.later { content_update() } case _ => } diff -r 9587134ec780 -r 551d09fc245c src/Tools/jEdit/src/sledgehammer_dockable.scala --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Fri Aug 09 12:27:29 2013 +0200 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Fri Aug 09 13:57:21 2013 +0200 @@ -31,8 +31,22 @@ /* query operation */ + private val process_indicator = new Process_Indicator + + private def consume_status(status: Query_Operation.Status.Value) + { + status match { + case Query_Operation.Status.WAITING => + process_indicator.update("Waiting for evaluation of context ...", 5) + case Query_Operation.Status.RUNNING => + process_indicator.update("Sledgehammering ...", 15) + case Query_Operation.Status.FINISHED => + process_indicator.update(null, 0) + } + } + private val sledgehammer = - Query_Operation(view, "sledgehammer", + Query_Operation(view, "sledgehammer", consume_status _, (snapshot, results, body) => pretty_text_area.update(snapshot, results, Pretty.separate(body))) @@ -101,6 +115,11 @@ } private val provers = new HistoryTextField("isabelle-sledgehammer-provers") { + override def processKeyEvent(evt: KeyEvent) + { + if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked + super.processKeyEvent(evt) + } setToolTipText(provers_label.tooltip) setColumns(20) } @@ -127,6 +146,11 @@ reactions += { case ButtonClicked(_) => clicked } } + private val cancel_query = new Button("Cancel") { + tooltip = "Interrupt unfinished query process" + reactions += { case ButtonClicked(_) => sledgehammer.cancel_query() } + } + private val locate_query = new Button("Locate") { tooltip = "Locate context of current query within source text" reactions += { case ButtonClicked(_) => sledgehammer.locate_query() } @@ -139,6 +163,6 @@ private val controls = new FlowPanel(FlowPanel.Alignment.Right)( provers_label, Component.wrap(provers), timeout, subgoal, isar_proofs, - sledgehammer.animation, apply_query, locate_query, zoom) + process_indicator.component, apply_query, cancel_query, locate_query, zoom) add(controls.peer, BorderLayout.NORTH) }