diff options
author | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-25 14:14:42 +0000 |
---|---|---|
committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-25 14:14:42 +0000 |
commit | 637e200e44c6144d0ec8ac28867ec2c5484ffc2d (patch) | |
tree | 16908fe3948dbad0d3b0e4add034cb27f0bf959e /lib | |
parent | 943cb0b91cfb15e2bdc04c626035e8cba0e65c02 (diff) |
Coqide: Globalization feedback (proof of concept)
A new feedback message for globalization infos can be sent by
Coq to Coqide. Coqide stores the information in the proof of
concept module wg_Tooltip, that also sets things up so that
these infos are displayed as a tooltip when the mouse is over
the text they are attached to. These infos are available only
on locked text, and on the text just processed in the case of an
error (on this piece of text, they vanish as the error tag vanishes
as soon as the user edits the text).
wg_Tooltip stocks these infos as lazy string. This is not needed
in the proof of concept, but is necessary to scale up: Coq may not
generate the full piece of info when the message is sent (because of
high computational cost or big size) and just send an id; later on,
when/if the user asks for the piece of info, the gui requests the
info explicitly using the id.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16456 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
-rw-r--r-- | lib/clib.mllib | 1 | ||||
-rw-r--r-- | lib/interface.mli | 1 | ||||
-rw-r--r-- | lib/lib.mllib | 1 | ||||
-rw-r--r-- | lib/serialize.ml | 27 |
4 files changed, 29 insertions, 1 deletions
diff --git a/lib/clib.mllib b/lib/clib.mllib index 9667df31c..a9b596b99 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -15,6 +15,7 @@ CList CString CArray Util +Loc Serialize Xml_utils Flags diff --git a/lib/interface.mli b/lib/interface.mli index 3ff05f6f2..e1419da9b 100644 --- a/lib/interface.mli +++ b/lib/interface.mli @@ -123,6 +123,7 @@ type edit_id = int type feedback_content = | AddedAxiom | Processed + | GlobRef of Loc.t * string * string * string * string type feedback = { edit_id : edit_id; diff --git a/lib/lib.mllib b/lib/lib.mllib index eb7285bdd..eabac2cfd 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -1,6 +1,5 @@ Xml_lexer Xml_parser -Loc Errors Bigint Dyn diff --git a/lib/serialize.ml b/lib/serialize.ml index 823f4245d..186c3dc89 100644 --- a/lib/serialize.ml +++ b/lib/serialize.ml @@ -525,15 +525,42 @@ let is_message = function | Element ("message", _, _) -> true | _ -> false +let of_loc loc = + let start, stop = Loc.unloc loc in + Element ("loc",[("start",string_of_int start);("stop",string_of_int stop)],[]) + +let to_loc xml = match xml with +| Element ("loc", l,[]) -> + (try + let start = List.assoc "start" l in + let stop = List.assoc "stop" l in + Loc.make_loc (int_of_string start, int_of_string stop) + with Not_found | Invalid_argument _ -> raise Marshal_error) +| _ -> raise Marshal_error + let to_feedback_content xml = do_match xml "feedback_content" (fun s args -> match s with | "addedaxiom" -> AddedAxiom | "processed" -> Processed + | "globref" -> + (match args with + | [loc; filepath; modpath; ident; ty] -> + GlobRef(to_loc loc, to_string filepath, to_string modpath, + to_string ident, to_string ty) + | _ -> raise Marshal_error) | _ -> raise Marshal_error) let of_feedback_content = function | AddedAxiom -> constructor "feedback_content" "addedaxiom" [] | Processed -> constructor "feedback_content" "processed" [] +| GlobRef(loc, filepath, modpath, ident, ty) -> + constructor "feedback_content" "globref" [ + of_loc loc; + of_string filepath; + of_string modpath; + of_string ident; + of_string ty + ] let of_feedback msg = let content = of_feedback_content msg.content in |