aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/coq.ml2
-rw-r--r--ide/coqOps.ml44
-rw-r--r--ide/coqide.ml16
-rw-r--r--ide/coqidetop.mllib2
-rw-r--r--ide/ide.mllib4
-rw-r--r--ide/ide_slave.ml20
-rw-r--r--ide/ideutils.ml4
-rw-r--r--ide/ideutils.mli2
-rw-r--r--ide/interface.mli9
-rw-r--r--ide/richpp.ml200
-rw-r--r--ide/richpp.mli64
-rw-r--r--ide/wg_Command.ml2
-rw-r--r--ide/wg_MessageView.ml21
-rw-r--r--ide/wg_MessageView.mli4
-rw-r--r--ide/wg_ProofView.ml12
-rw-r--r--ide/xmlprotocol.ml71
-rw-r--r--ide/xmlprotocol.mli3
17 files changed, 388 insertions, 92 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 9637b5b3f..e2036beee 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -205,7 +205,7 @@ type handle = {
proc : CoqTop.process;
xml_oc : Xml_printer.t;
mutable alive : bool;
- mutable waiting_for : ccb option; (* last call + callback + log *)
+ mutable waiting_for : ccb option; (* last call + callback *)
}
(** Coqtop process status :
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 0f3629c8f..7982ffc8b 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -162,13 +162,16 @@ let flags_to_color f =
else if List.mem `INCOMPLETE f then `NAME "gray"
else `NAME Preferences.processed_color#get
-let validate s =
- let open Xml_datatype in
- let rec validate = function
- | PCData s -> Glib.Utf8.validate s
- | Element (_, _, children) -> List.for_all validate children
- in
- validate (Richpp.repr s)
+(* Move to utils? *)
+let rec validate (s : Pp.std_ppcmds) = match s with
+ | Pp.Ppcmd_empty
+ | Pp.Ppcmd_print_break _
+ | Pp.Ppcmd_force_newline -> true
+ | Pp.Ppcmd_glue l -> List.for_all validate l
+ | Pp.Ppcmd_string s -> Glib.Utf8.validate s
+ | Pp.Ppcmd_box (_,s)
+ | Pp.Ppcmd_tag (_,s) -> validate s
+ | Pp.Ppcmd_comment s -> List.for_all Glib.Utf8.validate s
module Doc = Document
@@ -418,9 +421,10 @@ object(self)
| _ -> false
method private enqueue_feedback msg =
+ (* Minilib.log ("Feedback received: " ^ Xml_printer.to_string_fmt (Xmlprotocol.of_feedback msg)); *)
let id = msg.id in
if self#is_dummy_id id then () else Queue.add msg feedbacks
-
+
method private process_feedback () =
let rec eat_feedback n =
if n = 0 then true else
@@ -466,7 +470,7 @@ object(self)
(Printf.sprintf "%s %s %s" filepath ident ty)
| Message(Error, loc, msg), Some (id,sentence) ->
let loc = Option.default Loc.ghost loc in
- let msg = Richpp.raw_print msg in
+ let msg = Pp.string_of_ppcmds msg in
log "ErrorMsg" id;
remove_flag sentence `PROCESSING;
add_flag sentence (`ERROR (loc, msg));
@@ -476,14 +480,15 @@ object(self)
self#position_error_tag_at_sentence sentence (Some (Loc.unloc loc))
| Message(Warning, loc, msg), Some (id,sentence) ->
let loc = Option.default Loc.ghost loc in
- let rmsg = Richpp.raw_print msg in
- log "WarningMsg" id;
+ let rmsg = Pp.string_of_ppcmds msg in
+ log ("WarningMsg: " ^ Pp.string_of_ppcmds msg)id;
add_flag sentence (`WARNING (loc, rmsg));
self#attach_tooltip sentence loc rmsg;
self#position_warning_tag_at_sentence sentence loc;
messages#push Warning msg
| Message(lvl, loc, msg), Some (id,sentence) ->
- messages#push lvl msg
+ log ("Msg: " ^ Pp.string_of_ppcmds msg) id;
+ messages#push lvl msg
| InProgress n, _ ->
if n < 0 then processed <- processed + abs n
else to_process <- to_process + n
@@ -629,10 +634,9 @@ object(self)
if Queue.is_empty queue then conclude topstack else
match Queue.pop queue, topstack with
| `Skip(start,stop), [] ->
-
- logger Feedback.Error (Richpp.richpp_of_string "You must close the proof with Qed or Admitted");
+ logger Feedback.Error (Pp.str "You must close the proof with Qed or Admitted");
self#discard_command_queue queue;
- conclude []
+ conclude []
| `Skip(start,stop), (_,s) :: topstack ->
assert(start#equal (buffer#get_iter_at_mark s.start));
assert(stop#equal (buffer#get_iter_at_mark s.stop));
@@ -646,7 +650,7 @@ object(self)
let handle_answer = function
| Good (id, (Util.Inl (* NewTip *) (), msg)) ->
Doc.assign_tip_id document id;
- logger Feedback.Notice (Richpp.richpp_of_string msg);
+ logger Feedback.Notice (Pp.str msg);
self#commit_queue_transaction sentence;
loop id []
| Good (id, (Util.Inr (* Unfocus *) tip, msg)) ->
@@ -654,7 +658,7 @@ object(self)
let topstack, _ = Doc.context document in
self#exit_focus;
self#cleanup (Doc.cut_at document tip);
- logger Feedback.Notice (Richpp.richpp_of_string msg);
+ logger Feedback.Notice (Pp.str msg);
self#mark_as_needed sentence;
if Queue.is_empty queue then loop tip []
else loop tip (List.rev topstack)
@@ -673,7 +677,7 @@ object(self)
let next = function
| Good _ ->
messages#clear;
- messages#push Feedback.Info (Richpp.richpp_of_string "All proof terms checked by the kernel");
+ messages#push Feedback.Info (Pp.str "All proof terms checked by the kernel");
Coq.return ()
| Fail x -> self#handle_failure x in
Coq.bind (Coq.status true) next
@@ -860,7 +864,7 @@ object(self)
let next = function
| Fail (_, l, str) -> (* FIXME: check *)
display_error (l, str);
- messages#add (Richpp.richpp_of_string ("Unsuccessfully tried: "^phrase));
+ messages#add (Pp.str ("Unsuccessfully tried: "^phrase));
more
| Good msg ->
messages#add_string msg;
@@ -906,7 +910,7 @@ object(self)
let get_initial_state =
let next = function
| Fail (_, _, message) ->
- let message = "Couldn't initialize coqtop\n\n" ^ (Richpp.raw_print message) in
+ let message = "Couldn't initialize coqtop\n\n" ^ (Pp.string_of_ppcmds message) in
let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok ~message_type:`ERROR ~message () in
ignore (popup#run ()); exit 1
| Good id -> initial_state <- id; Coq.return () in
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 3d56f9dd4..25858acce 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -318,7 +318,7 @@ let export kind sn =
local_cd f ^ cmd_coqdoc#get ^ " --" ^ kind ^ " -o " ^
(Filename.quote output) ^ " " ^ (Filename.quote basef) ^ " 2>&1"
in
- sn.messages#set (Richpp.richpp_of_string ("Running: "^cmd));
+ sn.messages#set (Pp.str ("Running: "^cmd));
let finally st = flash_info (cmd ^ pr_exit_status st)
in
run_command (fun msg -> sn.messages#add_string msg) finally cmd
@@ -431,7 +431,7 @@ let compile sn =
^ " " ^ (Filename.quote f) ^ " 2>&1"
in
let buf = Buffer.create 1024 in
- sn.messages#set (Richpp.richpp_of_string ("Running: "^cmd));
+ sn.messages#set (Pp.str ("Running: "^cmd));
let display s =
sn.messages#add_string s;
Buffer.add_string buf s
@@ -441,8 +441,8 @@ let compile sn =
flash_info (f ^ " successfully compiled")
else begin
flash_info (f ^ " failed to compile");
- sn.messages#set (Richpp.richpp_of_string "Compilation output:\n");
- sn.messages#add (Richpp.richpp_of_string (Buffer.contents buf));
+ sn.messages#set (Pp.str "Compilation output:\n");
+ sn.messages#add (Pp.str (Buffer.contents buf));
end
in
run_command display finally cmd
@@ -464,7 +464,7 @@ let make sn =
|Some f ->
File.saveall ();
let cmd = local_cd f ^ cmd_make#get ^ " 2>&1" in
- sn.messages#set (Richpp.richpp_of_string "Compilation output:\n");
+ sn.messages#set (Pp.str "Compilation output:\n");
Buffer.reset last_make_buf;
last_make := "";
last_make_index := 0;
@@ -508,11 +508,11 @@ let next_error sn =
let stopi = b#get_iter_at_byte ~line:(line-1) stop in
b#apply_tag Tags.Script.error ~start:starti ~stop:stopi;
b#place_cursor ~where:starti;
- sn.messages#set (Richpp.richpp_of_string error_msg);
+ sn.messages#set (Pp.str error_msg);
sn.script#misc#grab_focus ()
with Not_found ->
last_make_index := 0;
- sn.messages#set (Richpp.richpp_of_string "No more errors.\n")
+ sn.messages#set (Pp.str "No more errors.\n")
let next_error = cb_on_current_term next_error
@@ -789,7 +789,7 @@ let coqtop_arguments sn =
let args = String.concat " " args in
let msg = Printf.sprintf "Invalid arguments: %s" args in
let () = sn.messages#clear in
- sn.messages#push Feedback.Error (Richpp.richpp_of_string msg)
+ sn.messages#push Feedback.Error (Pp.str msg)
else dialog#destroy ()
in
let _ = entry#connect#activate ok_cb in
diff --git a/ide/coqidetop.mllib b/ide/coqidetop.mllib
index ed1fa465d..043ad6008 100644
--- a/ide/coqidetop.mllib
+++ b/ide/coqidetop.mllib
@@ -2,7 +2,7 @@ Xml_lexer
Xml_parser
Xml_printer
Serialize
-Richprinter
+Richpp
Xmlprotocol
Texmacspp
Document
diff --git a/ide/ide.mllib b/ide/ide.mllib
index 72a14134b..12170c462 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -9,11 +9,11 @@ Config_lexer
Utf8_convert
Preferences
Project_file
-Serialize
-Richprinter
Xml_lexer
Xml_parser
Xml_printer
+Serialize
+Richpp
Xmlprotocol
Ideutils
Coq
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 0cb8d377f..88b61042e 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -32,9 +32,6 @@ let init_signal_handler () =
let f _ = if !catch_break then raise Sys.Break else Control.interrupt := true in
Sys.set_signal Sys.sigint (Sys.Signal_handle f)
-
-(** Redirection of standard output to a printable buffer *)
-
let pr_with_pid s = Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s
let pr_error s = pr_with_pid s
@@ -174,13 +171,13 @@ let process_goal sigma g =
let id = Goal.uid g in
let ccl =
let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
- Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr)
+ pr_goal_concl_style_env env sigma norm_constr
in
let process_hyp d (env,l) =
let d = CompactedDecl.map_constr (Reductionops.nf_evar sigma) d in
let d' = CompactedDecl.to_named_context d in
(List.fold_right Environ.push_named d' env,
- (Richpp.richpp_of_pp (pr_compacted_decl env sigma d)) :: l) in
+ (pr_compacted_decl env sigma d) :: l) in
let (_env, hyps) =
Context.Compacted.fold process_hyp
(Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in
@@ -340,13 +337,10 @@ let handle_exn (e, info) =
let loc_of e = match Loc.get_loc e with
| Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc)
| _ -> None in
- let mk_msg () =
- let msg = CErrors.print ~info e in
- Richpp.richpp_of_pp msg
- in
+ let mk_msg () = CErrors.print ~info e in
match e with
- | CErrors.Drop -> dummy, None, Richpp.richpp_of_string "Drop is not allowed by coqide!"
- | CErrors.Quit -> dummy, None, Richpp.richpp_of_string "Quit is not allowed by coqide!"
+ | CErrors.Drop -> dummy, None, Pp.str "Drop is not allowed by coqide!"
+ | CErrors.Quit -> dummy, None, Pp.str "Quit is not allowed by coqide!"
| e ->
match Stateid.get info with
| Some (valid, _) -> valid, loc_of info, mk_msg ()
@@ -446,7 +440,6 @@ let print_xml =
try Xml_printer.print oc xml; Mutex.unlock m
with e -> let e = CErrors.push e in Mutex.unlock m; iraise e
-
let slave_feeder xml_oc msg =
let xml = Xmlprotocol.of_feedback msg in
print_xml xml_oc xml
@@ -467,7 +460,6 @@ let loop () =
(* SEXP parser make *)
let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in
let () = Xml_parser.check_eof xml_ic false in
- Feedback.set_logger Feedback.feedback_logger;
Feedback.add_feeder (slave_feeder xml_oc);
(* We'll handle goal fetching and display in our own way *)
Vernacentries.enable_goal_printing := false;
@@ -478,7 +470,7 @@ let loop () =
(* pr_with_pid (Xml_printer.to_string_fmt xml_query); *)
let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in
let () = pr_debug_call q in
- let r = eval_call q in
+ let r = eval_call q in
let () = pr_debug_answer q r in
(* pr_with_pid (Xml_printer.to_string_fmt (Xmlprotocol.of_answer q r)); *)
print_xml xml_oc (Xmlprotocol.of_answer q r);
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index c3a280796..498a911ee 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -327,7 +327,7 @@ let textview_width (view : #GText.view_skel) =
let char_width = GPango.to_pixels metrics#approx_char_width in
pixel_width / char_width
-type logger = Feedback.level -> Richpp.richpp -> unit
+type logger = Feedback.level -> Pp.std_ppcmds -> unit
let default_logger level message =
let level = match level with
@@ -337,7 +337,7 @@ let default_logger level message =
| Feedback.Warning -> `WARNING
| Feedback.Error -> `ERROR
in
- Minilib.log ~level (xml_to_string message)
+ Minilib.log ~level (Pp.string_of_ppcmds message)
(** {6 File operations} *)
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index e32a4d9e3..1ae66e23e 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -69,7 +69,7 @@ val requote : string -> string
val textview_width : #GText.view_skel -> int
(** Returns an approximate value of the character width of a textview *)
-type logger = Feedback.level -> Richpp.richpp -> unit
+type logger = Feedback.level -> Pp.std_ppcmds -> unit
val default_logger : logger
(** Default logger. It logs messages that the casual user should not see. *)
diff --git a/ide/interface.mli b/ide/interface.mli
index 123cac6c2..43446f391 100644
--- a/ide/interface.mli
+++ b/ide/interface.mli
@@ -12,15 +12,14 @@
type raw = bool
type verbose = bool
-type richpp = Richpp.richpp
(** The type of coqtop goals *)
type goal = {
goal_id : string;
(** Unique goal identifier *)
- goal_hyp : richpp list;
+ goal_hyp : Pp.std_ppcmds list;
(** List of hypotheses *)
- goal_ccl : richpp;
+ goal_ccl : Pp.std_ppcmds;
(** Goal conclusion *)
}
@@ -119,7 +118,7 @@ type edit_id = Feedback.edit_id
should probably retract to that point *)
type 'a value =
| Good of 'a
- | Fail of (state_id * location * richpp)
+ | Fail of (state_id * location * Pp.std_ppcmds)
type ('a, 'b) union = ('a, 'b) Util.union
@@ -203,7 +202,7 @@ type about_sty = unit
type about_rty = coq_info
type handle_exn_sty = Exninfo.iexn
-type handle_exn_rty = state_id * location * richpp
+type handle_exn_rty = state_id * location * Pp.std_ppcmds
(* Retrocompatibility stuff *)
type interp_sty = (raw * verbose) * string
diff --git a/ide/richpp.ml b/ide/richpp.ml
new file mode 100644
index 000000000..c0128dbc2
--- /dev/null
+++ b/ide/richpp.ml
@@ -0,0 +1,200 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Util
+open Xml_datatype
+
+type 'annotation located = {
+ annotation : 'annotation option;
+ startpos : int;
+ endpos : int
+}
+
+type 'a stack =
+| Leaf
+| Node of string * 'a located gxml list * int * 'a stack
+
+type 'a context = {
+ mutable stack : 'a stack;
+ (** Pending opened nodes *)
+ mutable offset : int;
+ (** Quantity of characters printed so far *)
+ mutable annotations : 'a option Int.Map.t;
+ (** Map associating annotations to indexes *)
+ mutable index : int;
+ (** Current index of annotations *)
+}
+
+(** We use Format to introduce tags inside the pretty-printed document.
+ Each inserted tag is a fresh index that we keep in sync with the contents
+ of annotations.
+
+ We build an XML tree on the fly, by plugging ourselves in Format tag
+ marking functions. As those functions are called when actually writing to
+ the device, the resulting tree is correct.
+*)
+let rich_pp annotate ppcmds =
+
+ let context = {
+ stack = Leaf;
+ offset = 0;
+ annotations = Int.Map.empty;
+ index = (-1);
+ } in
+
+ let pp_tag obj =
+ let index = context.index + 1 in
+ let () = context.index <- index in
+ let obj = annotate obj in
+ let () = context.annotations <- Int.Map.add index obj context.annotations in
+ string_of_int index
+ in
+
+ let pp_buffer = Buffer.create 180 in
+
+ let push_pcdata () =
+ (** Push the optional PCData on the above node *)
+ let len = Buffer.length pp_buffer in
+ if len = 0 then ()
+ else match context.stack with
+ | Leaf -> assert false
+ | Node (node, child, pos, ctx) ->
+ let data = Buffer.contents pp_buffer in
+ let () = Buffer.clear pp_buffer in
+ let () = context.stack <- Node (node, PCData data :: child, pos, ctx) in
+ context.offset <- context.offset + len
+ in
+
+ let open_xml_tag tag =
+ let () = push_pcdata () in
+ context.stack <- Node (tag, [], context.offset, context.stack)
+ in
+
+ let close_xml_tag tag =
+ let () = push_pcdata () in
+ match context.stack with
+ | Leaf -> assert false
+ | Node (node, child, pos, ctx) ->
+ let () = assert (String.equal tag node) in
+ let annotation =
+ try Int.Map.find (int_of_string node) context.annotations
+ with _ -> None
+ in
+ let annotation = {
+ annotation = annotation;
+ startpos = pos;
+ endpos = context.offset;
+ } in
+ let xml = Element (node, annotation, List.rev child) in
+ match ctx with
+ | Leaf ->
+ (** Final node: we keep the result in a dummy context *)
+ context.stack <- Node ("", [xml], 0, Leaf)
+ | Node (node, child, pos, ctx) ->
+ context.stack <- Node (node, xml :: child, pos, ctx)
+ in
+
+ let open Format in
+
+ let ft = formatter_of_buffer pp_buffer in
+
+ let tag_functions = {
+ mark_open_tag = (fun tag -> let () = open_xml_tag tag in "");
+ mark_close_tag = (fun tag -> let () = close_xml_tag tag in "");
+ print_open_tag = ignore;
+ print_close_tag = ignore;
+ } in
+
+ pp_set_formatter_tag_functions ft tag_functions;
+ pp_set_mark_tags ft true;
+
+ (* Set formatter width. This is currently a hack and duplicate code
+ with Pp_control. Hopefully it will be fixed better in Coq 8.7 *)
+ let w = pp_get_margin str_formatter () in
+ let m = max (64 * w / 100) (w-30) in
+ pp_set_margin ft w;
+ pp_set_max_indent ft m;
+
+ (** The whole output must be a valid document. To that
+ end, we nest the document inside <pp> tags. *)
+ pp_open_tag ft "pp";
+ Pp.(pp_with ~pp_tag ft ppcmds);
+ pp_close_tag ft ();
+
+ (** Get the resulting XML tree. *)
+ let () = pp_print_flush ft () in
+ let () = assert (Buffer.length pp_buffer = 0) in
+ match context.stack with
+ | Node ("", [xml], 0, Leaf) -> xml
+ | _ -> assert false
+
+
+let annotations_positions xml =
+ let rec node accu = function
+ | Element (_, { annotation = Some annotation; startpos; endpos }, cs) ->
+ children ((annotation, (startpos, endpos)) :: accu) cs
+ | Element (_, _, cs) ->
+ children accu cs
+ | _ ->
+ accu
+ and children accu cs =
+ List.fold_left node accu cs
+ in
+ node [] xml
+
+let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml =
+ let rec node = function
+ | Element (index, { annotation; startpos; endpos }, cs) ->
+ let attributes =
+ [ "startpos", string_of_int startpos;
+ "endpos", string_of_int endpos
+ ]
+ @ (match annotation with
+ | None -> []
+ | Some annotation -> attributes_of_annotation annotation
+ )
+ in
+ let tag =
+ match annotation with
+ | None -> index
+ | Some annotation -> tag_of_annotation annotation
+ in
+ Element (tag, attributes, List.map node cs)
+ | PCData s ->
+ PCData s
+ in
+ node xml
+
+type richpp = xml
+
+let repr xml = xml
+let richpp_of_xml xml = xml
+let richpp_of_string s = PCData s
+
+let richpp_of_pp pp =
+ let annotate t = Some (Ppstyle.repr t) in
+ let rec drop = function
+ | PCData s -> [PCData s]
+ | Element (_, annotation, cs) ->
+ let cs = List.concat (List.map drop cs) in
+ match annotation.annotation with
+ | None -> cs
+ | Some s -> [Element (String.concat "." s, [], cs)]
+ in
+ let xml = rich_pp annotate pp in
+ Element ("_", [], drop xml)
+
+let raw_print xml =
+ let buf = Buffer.create 1024 in
+ let rec print = function
+ | PCData s -> Buffer.add_string buf s
+ | Element (_, _, cs) -> List.iter print cs
+ in
+ let () = print xml in
+ Buffer.contents buf
+
diff --git a/ide/richpp.mli b/ide/richpp.mli
new file mode 100644
index 000000000..2e839e996
--- /dev/null
+++ b/ide/richpp.mli
@@ -0,0 +1,64 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** This module offers semi-structured pretty-printing. *)
+
+(** Each annotation of the semi-structured document refers to the
+ substring it annotates. *)
+type 'annotation located = {
+ annotation : 'annotation option;
+ startpos : int;
+ endpos : int
+}
+
+(** [rich_pp get_annotations ppcmds] returns the interpretation
+ of [ppcmds] as a semi-structured document
+ that represents (located) annotations of this string.
+ The [get_annotations] function is used to convert tags into the desired
+ annotation. *)
+val rich_pp :
+ (Pp.pp_tag -> 'annotation option) -> Pp.std_ppcmds ->
+ 'annotation located Xml_datatype.gxml
+
+(** [annotations_positions ssdoc] returns a list associating each
+ annotations with its position in the string from which [ssdoc] is
+ built. *)
+val annotations_positions :
+ 'annotation located Xml_datatype.gxml ->
+ ('annotation * (int * int)) list
+
+(** [xml_of_rich_pp ssdoc] returns an XML representation of the
+ semi-structured document [ssdoc]. *)
+val xml_of_rich_pp :
+ ('annotation -> string) ->
+ ('annotation -> (string * string) list) ->
+ 'annotation located Xml_datatype.gxml ->
+ Xml_datatype.xml
+
+(** {5 Enriched text} *)
+
+type richpp
+(** Type of text with style annotations *)
+
+val richpp_of_pp : Pp.std_ppcmds -> richpp
+(** Extract style information from formatted text *)
+
+val richpp_of_xml : Xml_datatype.xml -> richpp
+(** Do not use outside of dedicated areas *)
+
+val richpp_of_string : string -> richpp
+(** Make a styled text out of a normal string *)
+
+val repr : richpp -> Xml_datatype.xml
+(** Observe the styled text as XML *)
+
+(** {5 Debug/Compat} *)
+
+(** Represent the semi-structured document as a string, dropping any additional
+ information. *)
+val raw_print : richpp -> string
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index d33c0add4..b83bd107e 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -103,7 +103,7 @@ object(self)
let process =
Coq.bind (Coq.query (phrase,Stateid.dummy)) (function
| Interface.Fail (_,l,str) ->
- Ideutils.insert_xml result#buffer str;
+ Ideutils.insert_xml result#buffer (Richpp.richpp_of_pp str);
notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce;
Coq.return ()
| Interface.Good res ->
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 0330b8eff..1cf389c75 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -28,9 +28,9 @@ class type message_view =
inherit GObj.widget
method connect : message_view_signals
method clear : unit
- method add : Richpp.richpp -> unit
+ method add : Pp.std_ppcmds -> unit
method add_string : string -> unit
- method set : Richpp.richpp -> unit
+ method set : Pp.std_ppcmds -> unit
method push : Ideutils.logger
(** same as [add], but with an explicit level instead of [Notice] *)
method buffer : GText.buffer
@@ -79,21 +79,14 @@ let message_view () : message_view =
| Feedback.Warning -> [Tags.Message.warning]
| _ -> []
in
- let rec non_empty = function
- | Xml_datatype.PCData "" -> false
- | Xml_datatype.PCData _ -> true
- | Xml_datatype.Element (_, _, children) -> List.exists non_empty children
- in
- if non_empty (Richpp.repr msg) then begin
- let mark = `MARK mark in
- Ideutils.insert_xml ~mark buffer ~tags msg;
- buffer#insert ~iter:(buffer#get_iter_at_mark mark) "\n";
- push#call (level, msg)
- end
+ let mark = `MARK mark in
+ Ideutils.insert_xml ~mark buffer ~tags (Richpp.richpp_of_pp msg);
+ buffer#insert ~iter:(buffer#get_iter_at_mark mark) "\n";
+ push#call (level, msg)
method add msg = self#push Feedback.Notice msg
- method add_string s = self#add (Richpp.richpp_of_string s)
+ method add_string s = self#add (Pp.str s)
method set msg = self#clear; self#add msg
diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli
index 2d34533de..a71d345a5 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/wg_MessageView.mli
@@ -18,9 +18,9 @@ class type message_view =
inherit GObj.widget
method connect : message_view_signals
method clear : unit
- method add : Richpp.richpp -> unit
+ method add : Pp.std_ppcmds -> unit
method add_string : string -> unit
- method set : Richpp.richpp -> unit
+ method set : Pp.std_ppcmds -> unit
method push : Ideutils.logger
(** same as [add], but with an explicit level instead of [Notice] *)
method buffer : GText.buffer
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 47c86045a..72aa9051a 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -84,7 +84,7 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
let () = hook_tag_cb tag hint sel_cb on_hover in
[tag], hints
in
- let () = insert_xml ~tags proof#buffer hyp in
+ let () = insert_xml ~tags proof#buffer (Richpp.richpp_of_pp hyp) in
proof#buffer#insert "\n";
insert_hyp rem_hints hs
in
@@ -98,13 +98,13 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
else []
in
proof#buffer#insert (goal_str 1 goals_cnt);
- insert_xml proof#buffer cur_goal;
+ insert_xml proof#buffer (Richpp.richpp_of_pp cur_goal);
proof#buffer#insert "\n"
in
(* Insert remaining goals (no hypotheses) *)
let fold_goal i _ { Interface.goal_ccl = g } =
proof#buffer#insert (goal_str i goals_cnt);
- insert_xml proof#buffer g;
+ insert_xml proof#buffer (Richpp.richpp_of_pp g);
proof#buffer#insert "\n"
in
let () = Util.List.fold_left_i fold_goal 2 () rem_goals in
@@ -144,7 +144,7 @@ let display mode (view : #GText.view_skel) goals hints evars =
(* The proof is finished, with the exception of given up goals. *)
view#buffer#insert "No more subgoals, but there are some goals you gave up:\n\n";
let iter goal =
- insert_xml view#buffer goal.Interface.goal_ccl;
+ insert_xml view#buffer (Richpp.richpp_of_pp goal.Interface.goal_ccl);
view#buffer#insert "\n"
in
List.iter iter given_up_goals;
@@ -153,7 +153,7 @@ let display mode (view : #GText.view_skel) goals hints evars =
(* All the goals have been resolved but those on the shelf. *)
view#buffer#insert "All the remaining goals are on the shelf:\n\n";
let iter goal =
- insert_xml view#buffer goal.Interface.goal_ccl;
+ insert_xml view#buffer (Richpp.richpp_of_pp goal.Interface.goal_ccl);
view#buffer#insert "\n"
in
List.iter iter shelved_goals
@@ -166,7 +166,7 @@ let display mode (view : #GText.view_skel) goals hints evars =
view#buffer#insert "This subproof is complete, but there are some unfocused goals:\n\n";
let iter i goal =
let () = view#buffer#insert (goal_str (succ i)) in
- insert_xml view#buffer goal.Interface.goal_ccl;
+ insert_xml view#buffer (Richpp.richpp_of_pp goal.Interface.goal_ccl);
view#buffer#insert "\n"
in
List.iteri iter bg
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index 65f44fdd3..08f23d3d4 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -97,6 +97,49 @@ let to_richpp xml = match xml with
| Element ("richpp", [], [x]) -> Richpp.richpp_of_xml x
| x -> raise Serialize.(Marshal_error("richpp",x))
+let of_box (ppb : Pp.block_type) = let open Pp in match ppb with
+ | Pp_hbox i -> constructor "ppbox" "hbox" [of_int i]
+ | Pp_vbox i -> constructor "ppbox" "vbox" [of_int i]
+ | Pp_hvbox i -> constructor "ppbox" "hvbox" [of_int i]
+ | Pp_hovbox i -> constructor "ppbox" "hovbox" [of_int i]
+
+let to_box = let open Pp in
+ do_match "ppbox" (fun s args -> match s with
+ | "hbox" -> Pp_hbox (to_int (singleton args))
+ | "vbox" -> Pp_vbox (to_int (singleton args))
+ | "hvbox" -> Pp_hvbox (to_int (singleton args))
+ | "hovbox" -> Pp_hovbox (to_int (singleton args))
+ | x -> raise (Marshal_error("*ppbox",PCData x))
+ )
+
+let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match pp with
+ | Ppcmd_empty -> constructor "ppdoc" "emtpy" []
+ | Ppcmd_string s -> constructor "ppdoc" "string" [of_string s]
+ | Ppcmd_glue sl -> constructor "ppdoc" "glue" [of_list of_pp sl]
+ | Ppcmd_box (bt,s) -> constructor "ppdoc" "box" [of_pair of_box of_pp (bt,s)]
+ | Ppcmd_tag (t,s) -> constructor "ppdoc" "tag" [of_pair (of_list of_string) of_pp (t,s)]
+ | Ppcmd_print_break (i,j)
+ -> constructor "ppdoc" "break" [of_pair of_int of_int (i,j)]
+ | Ppcmd_force_newline -> constructor "ppdoc" "newline" []
+ | Ppcmd_comment cmd -> constructor "ppdoc" "comment" [of_list of_string cmd]
+
+
+let rec to_pp xpp = let open Pp in
+ do_match "ppdoc" (fun s args -> match s with
+ | "empty" -> Ppcmd_empty
+ | "string" -> Ppcmd_string (to_string (singleton args))
+ | "glue" -> Ppcmd_glue (to_list to_pp (singleton args))
+ | "box" -> let (bt,s) = to_pair to_box to_pp (singleton args) in
+ Ppcmd_box(bt,s)
+ | "tag" -> let (tg,s) = to_pair (to_list to_string) to_pp (singleton args) in
+ Ppcmd_tag(tg,s)
+ | "break" -> let (i,j) = to_pair to_int to_int (singleton args) in
+ Ppcmd_print_break(i, j)
+ | "newline" -> Ppcmd_force_newline
+ | "comment" -> Ppcmd_comment (to_list to_string (singleton args))
+ | x -> raise (Marshal_error("*ppdoc",PCData x))
+ ) xpp
+
let of_value f = function
| Good x -> Element ("value", ["val", "good"], [f x])
| Fail (id,loc, msg) ->
@@ -104,7 +147,7 @@ let of_value f = function
| None -> []
| Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] in
let id = of_stateid id in
- Element ("value", ["val", "fail"] @ loc, [id; of_richpp msg])
+ Element ("value", ["val", "fail"] @ loc, [id; of_pp msg])
let to_value f = function
| Element ("value", attrs, l) ->
@@ -120,7 +163,7 @@ let to_value f = function
in
let (id, msg) = match l with [id; msg] -> (id, msg) | _ -> raise (Marshal_error("val",PCData "no id attribute")) in
let id = to_stateid id in
- let msg = to_richpp msg in
+ let msg = to_pp msg in
Fail (id, loc, msg)
else raise (Marshal_error("good or fail",PCData ans))
| x -> raise (Marshal_error("value",x))
@@ -147,15 +190,15 @@ let to_evar = function
| x -> raise (Marshal_error("evar",x))
let of_goal g =
- let hyp = of_list of_richpp g.goal_hyp in
- let ccl = of_richpp g.goal_ccl in
+ let hyp = of_list of_pp g.goal_hyp in
+ let ccl = of_pp g.goal_ccl in
let id = of_string g.goal_id in
Element ("goal", [], [id; hyp; ccl])
let to_goal = function
| Element ("goal", [], [id; hyp; ccl]) ->
- let hyp = to_list to_richpp hyp in
- let ccl = to_richpp ccl in
- let id = to_string id in
+ let hyp = to_list to_pp hyp in
+ let ccl = to_pp ccl in
+ let id = to_string id in
{ goal_hyp = hyp; goal_ccl = ccl; goal_id = id; }
| x -> raise (Marshal_error("goal",x))
@@ -344,8 +387,8 @@ end = struct
Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals
else
let pr_goal { goal_hyp = hyps; goal_ccl = goal } =
- "[" ^ String.concat "; " (List.map Richpp.raw_print hyps) ^ " |- " ^
- Richpp.raw_print goal ^ "]" in
+ "[" ^ String.concat "; " (List.map Pp.string_of_ppcmds hyps) ^ " |- " ^
+ Pp.string_of_ppcmds goal ^ "]" in
String.concat " " (List.map pr_goal g.fg_goals)
let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]"
let pr_status (s : status) =
@@ -701,10 +744,10 @@ let to_call : xml -> unknown_call =
let pr_value_gen pr = function
| Good v -> "GOOD " ^ pr v
- | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^Richpp.raw_print str^"]"
+ | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^ Pp.string_of_ppcmds str ^ "]"
| Fail (id,Some(i,j),str) ->
"FAIL "^Stateid.to_string id^
- " ("^string_of_int i^","^string_of_int j^")["^Richpp.raw_print str^"]"
+ " ("^string_of_int i^","^string_of_int j^")["^Pp.string_of_ppcmds str^"]"
let pr_value v = pr_value_gen (fun _ -> "FIXME") v
let pr_full_value : type a. a call -> a value -> string = fun call value -> match call with
| Add _ -> pr_value_gen (print add_rty_t ) value
@@ -760,7 +803,7 @@ let document to_string_fmt =
(to_string_fmt (of_value (fun _ -> PCData "b") (Good ())));
Printf.printf "or:\n\n%s\n\nwhere the attributes loc_s and loc_c are optional.\n"
(to_string_fmt (of_value (fun _ -> PCData "b")
- (Fail (Stateid.initial,Some (15,34),Richpp.richpp_of_string "error message"))));
+ (Fail (Stateid.initial,Some (15,34), Pp.str "error message"))));
document_type_encoding to_string_fmt
(* Moved from feedback.mli : This is IDE specific and we don't want to
@@ -787,12 +830,12 @@ let to_message_level =
let of_message lvl loc msg =
let lvl = of_message_level lvl in
let xloc = of_option of_loc loc in
- let content = of_richpp msg in
+ let content = of_pp msg in
Xml_datatype.Element ("message", [], [lvl; xloc; content])
let to_message xml = match xml with
| Xml_datatype.Element ("message", [], [lvl; xloc; content]) ->
- Message(to_message_level lvl, to_option to_loc xloc, to_richpp content)
+ Message(to_message_level lvl, to_option to_loc xloc, to_pp content)
| x -> raise (Marshal_error("message",x))
let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli
index ca911178f..f6fae24d7 100644
--- a/ide/xmlprotocol.mli
+++ b/ide/xmlprotocol.mli
@@ -66,5 +66,6 @@ val of_feedback : Feedback.feedback -> xml
val to_feedback : xml -> Feedback.feedback
val is_feedback : xml -> bool
-val of_message : Feedback.level -> Loc.t option -> Richpp.richpp -> xml
+val of_message : Feedback.level -> Loc.t option -> Pp.std_ppcmds -> xml
+(* val to_message : xml -> Feedback.message *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 09:18:06 +0000