--- 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)
--- 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
--- 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)
- }
}
--- 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 =
--- 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"
--- 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 *)
--- 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) }
--- 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;
--- 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 @@
-<xsd:schema xmlns:xsd="http://www.w3.org/2001/XMLSchema">
-
-<xsd:element name="class">
- <xsd:complexType>
- <xsd:attribute name="name" type="xsd:string" use="required"/>
- </xsd:complexType>
-</xsd:element>
-
-<xsd:element name="type">
- <xsd:complexType>
- <xsd:group ref="typeGroup"/>
- </xsd:complexType>
-</xsd:element>
-
-<xsd:element name="types">
- <xsd:complexType>
- <xsd:group ref="typeGroup" minOccurs="0" maxOccurs="unbounded"/>
- </xsd:complexType>
-</xsd:element>
-
-<xsd:group name="typeGroup">
- <xsd:choice>
- <xsd:element name="TVar">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:element ref="class" minOccurs="0" maxOccurs="unbounded"/>
- </xsd:sequence>
- <xsd:attribute name="name" type="xsd:string" use="required"/>
- <xsd:attribute name="index" type="xsd:integer"/>
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="TFree">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:element ref="class" minOccurs="0" maxOccurs="unbounded"/>
- </xsd:sequence>
- <xsd:attribute name="name" type="xsd:string" use="required"/>
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="Type">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:group ref="typeGroup" minOccurs="0" maxOccurs="unbounded"/>
- </xsd:sequence>
- <xsd:attribute name="name" type="xsd:string" use="required"/>
- </xsd:complexType>
- </xsd:element>
- </xsd:choice>
-</xsd:group>
-
-<xsd:element name="term">
- <xsd:complexType>
- <xsd:group ref="termGroup"/>
- </xsd:complexType>
-</xsd:element>
-
-<xsd:group name="termGroup">
- <xsd:choice>
- <xsd:element name="Var">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:group ref="typeGroup"/>
- </xsd:sequence>
- <xsd:attribute name="name" type="xsd:string" use="required"/>
- <xsd:attribute name="index" type="xsd:integer"/>
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="Free">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:group ref="typeGroup"/>
- </xsd:sequence>
- <xsd:attribute name="name" type="xsd:string" use="required"/>
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="Const">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:group ref="typeGroup"/>
- </xsd:sequence>
- <xsd:attribute name="name" type="xsd:string" use="required"/>
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="Bound">
- <xsd:complexType>
- <xsd:attribute name="index" type="xsd:integer" use="required"/>
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="App">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:group ref="termGroup"/>
- <xsd:group ref="termGroup"/>
- </xsd:sequence>
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="Abs">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:group ref="typeGroup"/>
- <xsd:group ref="termGroup"/>
- </xsd:sequence>
- <xsd:attribute name="vname" type="xsd:string" use="required"/>
- </xsd:complexType>
- </xsd:element>
- </xsd:choice>
-</xsd:group>
-
-<xsd:element name="proof">
- <xsd:complexType>
- <xsd:group ref="proofGroup"/>
- </xsd:complexType>
-</xsd:element>
-
-<xsd:group name="proofGroup">
- <xsd:choice>
- <xsd:element name="PThm">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:group ref="termGroup" minOccurs="0"/>
- <xsd:element ref="types" minOccurs="0"/>
- </xsd:sequence>
- <xsd:attribute name="name" type="xsd:string" use="required"/>
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="PAxm">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:group ref="termGroup" minOccurs="0"/>
- <xsd:element ref="types" minOccurs="0"/>
- </xsd:sequence>
- <xsd:attribute name="name" type="xsd:string" use="required"/>
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="Oracle">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:group ref="termGroup"/>
- <xsd:element ref="types" minOccurs="0"/>
- </xsd:sequence>
- <xsd:attribute name="name" type="xsd:string" use="required"/>
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="PBound">
- <xsd:complexType>
- <xsd:attribute name="index" type="xsd:integer" use="required"/>
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="Appt">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:group ref="proofGroup"/>
- <xsd:group ref="termGroup" minOccurs="0"/>
- </xsd:sequence>
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="AppP">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:group ref="proofGroup"/>
- <xsd:group ref="proofGroup"/>
- </xsd:sequence>
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="Abst">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:group ref="typeGroup" minOccurs="0"/>
- <xsd:group ref="proofGroup"/>
- </xsd:sequence>
- <xsd:attribute name="vname" type="xsd:string" use="required"/>
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="AbsP">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:group ref="termGroup" minOccurs="0"/>
- <xsd:group ref="proofGroup"/>
- </xsd:sequence>
- <xsd:attribute name="vname" type="xsd:string" use="required"/>
- </xsd:complexType>
- </xsd:element>
- <xsd:element name="Hyp">
- <xsd:complexType>
- <xsd:sequence>
- <xsd:group ref="termGroup"/>
- </xsd:sequence>
- </xsd:complexType>
- </xsd:element>
- </xsd:choice>
-</xsd:group>
-
-</xsd:schema>
--- 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
- ("<?xml version=\"1.0\" encoding=\"UTF-8\"?>\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;
--- 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;
*}
--- 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
--- 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
--- 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;
-
--- 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"
--- 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)
}
--- /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)
+ }
+}
+
--- 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 _ =>
}
--- 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)
}