diff --git a/src/libraries/utils/markdown.ml b/src/libraries/utils/markdown.ml
index 58cbefe073af85c358d7a35ecde98327b889fc4b..4d33aa797e8e178b77b185d6d0bf030f51a265a8 100644
--- a/src/libraries/utils/markdown.ml
+++ b/src/libraries/utils/markdown.ml
@@ -48,22 +48,28 @@ type block_element =
and block = block_element list
+and table = {
+ caption: text option;
+ header: (text * align) list;
+ content: text list list;
+ }
+
and element =
+ | Comment of string (** markdown comment, printed <!-- like this --> *)
| Block of block
+ | Table of table
| Raw of string list
- (** non-markdown. Each element of the list is printed as-is on its own line.
+ (** Each element of the list is printed as-is on its own line.
A blank line separates the [Raw] node from the next one. *)
- | Comment of string (** markdown comment, printed <!-- like this --> *)
- | H1 of text * string option (** optional label. *)
+ | Delayed of (unit -> elements)
+ | H1 of text * string option
| H2 of text * string option
| H3 of text * string option
| H4 of text * string option
| H5 of text * string option
| H6 of text * string option
- | Table of { caption: text option; header: (text * align) list;
- content: text list list; }
-type elements = element list
+and elements = element list
type pandoc_markdown =
{ title: text;
@@ -123,8 +129,9 @@ let list items = [UL items]
let enum items = [OL items]
let description items = [DL items]
-let block b = [Block b]
let par text = [Block [Text text]]
+let block b = [Block b]
+let delayed f = [Delayed f]
(* -------------------------------------------------------------------------- *)
(* --- Sectioning --- *)
@@ -185,6 +192,10 @@ let mk_date () =
let pandoc ?(title=[Plain ""]) ?(authors=[]) ?(date=mk_date()) elements =
{ title; authors; date; elements }
+(* -------------------------------------------------------------------------- *)
+(* --- Printers --- *)
+(* -------------------------------------------------------------------------- *)
+
let relativize page target =
let page_dir = String.split_on_char '/' page in
let target_dir = String.split_on_char '/' target in
@@ -236,9 +247,8 @@ let pp_lab fmt = function
| None -> ()
| Some lab -> Format.fprintf fmt " {#%s}" lab
-let test_size txt =
- (* get rid of ?page *)
- let pp_text fmt = pp_text fmt in
+let test_size ?page txt =
+ let pp_text fmt = pp_text ?page fmt in
String.length (Format.asprintf "%a" pp_text txt)
let pp_dashes fmt size =
@@ -251,7 +261,7 @@ let pp_sep_line fmt sizes =
Format.fprintf fmt "@]@\n"
let pp_header ?page fmt (t,_) size =
- let real_size = test_size t in
+ let real_size = test_size ?page t in
let spaces = String.make (size - real_size) ' ' in
Format.fprintf fmt " %a%s |" (pp_text ?page) t spaces
@@ -300,6 +310,47 @@ let pp_table_content ?page fmt l sizes =
List.iter (pp_table_line ?page fmt sizes) l;
Format.fprintf fmt "@]"
+let pp_table_caption ?page fmt = function None -> () | Some t ->
+ Format.fprintf fmt "@[<h>Table: %a@]@\n@\n" (pp_text ?page) t
+
+[@@@ warning "-32"]
+let pp_table_extended ?page fmt { caption; header; content } =
+ begin
+ pp_table_caption ?page fmt caption;
+ let sizes = compute_sizes header content in
+ pp_sep_line fmt sizes;
+ pp_headers ?page fmt header sizes;
+ pp_aligns fmt header sizes;
+ pp_table_content ?page fmt content sizes;
+ end
+[@@@ warning "+32"]
+
+let pp_table_inlined ?page fmt { caption; header; content } =
+ begin
+ pp_table_caption ?page fmt caption;
+ Format.fprintf fmt "@[<v>";
+ let pp = pp_text ?page in
+ List.iter
+ (function (h,_) -> Format.fprintf fmt "| @[<h>%a@] " pp h)
+ header;
+ Format.fprintf fmt "|@\n";
+ List.iter
+ (fun (h,align) ->
+ let dash h k = String.make (max 3 (test_size ?page h + k)) '-' in
+ match align with
+ | Left -> Format.fprintf fmt "|:%s" (dash h 1)
+ | Right -> Format.fprintf fmt "|%s:" (dash h 1)
+ | Center -> Format.fprintf fmt "|:%s:" (dash h 0)
+ ) header;
+ Format.fprintf fmt "|@\n" ;
+ List.iter (fun row ->
+ List.iter
+ (fun col -> Format.fprintf fmt "| @[<h>%a@] " pp col) row ;
+ Format.fprintf fmt "|@\n" ;
+ ) content ;
+ Format.fprintf fmt "@]" ;
+ end
+
let rec pp_block_element ?page fmt e =
let pp_text fmt = pp_text ?page fmt in
match e with
@@ -355,23 +406,17 @@ and pp_element ?page fmt e =
| Comment s ->
Format.fprintf fmt
"@[<hv>@[<hov 5><!-- %a@]@ -->@]" Format.pp_print_text s
+ | Table table -> pp_table_inlined ?page fmt table
+ (* pp_table_extended ?page fmt table *)
+ | Delayed f -> pp_elements ?page fmt (f ())
| H1(t,lab) -> Format.fprintf fmt "@[<h># %a%a@]" pp_text t pp_lab lab
| H2(t,lab) -> Format.fprintf fmt "@[<h>## %a%a@]" pp_text t pp_lab lab
| H3(t,lab) -> Format.fprintf fmt "@[<h>### %a%a@]" pp_text t pp_lab lab
| H4(t,lab) -> Format.fprintf fmt "@[<h>#### %a%a@]" pp_text t pp_lab lab
| H5(t,lab) -> Format.fprintf fmt "@[<h>##### %a%a@]" pp_text t pp_lab lab
| H6(t,lab) -> Format.fprintf fmt "@[<h>###### %a%a@]" pp_text t pp_lab lab
- | Table { caption; header; content } ->
- (match caption with
- | None -> ()
- | Some t -> Format.fprintf fmt "@[<h>Table: %a@]@\n@\n" pp_text t);
- let sizes = compute_sizes header content in
- pp_sep_line fmt sizes;
- pp_headers ?page fmt header sizes;
- pp_aligns fmt header sizes;
- pp_table_content ?page fmt content sizes
-let pp_elements ?page fmt l =
+and pp_elements ?page fmt l =
let pp_sep fmt () =
Format.pp_print_newline fmt ();
Format.pp_print_newline fmt ()
@@ -393,3 +438,5 @@ let pp_pandoc ?page fmt { title; authors; date; elements } =
end;
pp_elements ?page fmt elements;
Format.fprintf fmt "@]%!"
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/libraries/utils/markdown.mli b/src/libraries/utils/markdown.mli
index 1745b1683ce3fc0251216055886e0f3df18fadd5..7e7047fd73d11a876aaa914bf9d058be12c4f1ba 100644
--- a/src/libraries/utils/markdown.mli
+++ b/src/libraries/utils/markdown.mli
@@ -63,22 +63,28 @@ type block_element =
and block = block_element list
+and table = {
+ caption: text option;
+ header: (text * align) list;
+ content: text list list;
+}
+
and element =
+ | Comment of string (** markdown comment, printed <!-- like this --> *)
| Block of block
+ | Table of table
| Raw of string list
- (** non-markdown. Each element of the list is printed as-is on its own line.
+ (** Each element of the list is printed as-is on its own line.
A blank line separates the [Raw] node from the next one. *)
- | Comment of string (** markdown comment, printed <!-- like this --> *)
- | H1 of text * string option (** optional label. *)
+ | Delayed of (unit -> elements)
+ | H1 of text * string option
| H2 of text * string option
| H3 of text * string option
| H4 of text * string option
| H5 of text * string option
| H6 of text * string option
- | Table of { caption: text option; header: (text * align) list;
- content: text list list; }
-type elements = element list
+and elements = element list
type pandoc_markdown =
{ title: text;
@@ -163,6 +169,9 @@ val block : block -> elements
*)
val rawfile: string -> elements
+(** Delayed element. The content is computed on pretty-printing. *)
+val delayed: (unit -> elements) -> elements
+
(** {2 Document Structure} *)
(** Creates a document from a list of elements and optional metadatas.
diff --git a/src/plugins/markdown-report/md_gen.ml b/src/plugins/markdown-report/md_gen.ml
index b5cec960eb4f8f16c7903049efa4f2c529e6d29d..a29009b11cad4b55de5779661e956919d7350cfe 100644
--- a/src/plugins/markdown-report/md_gen.ml
+++ b/src/plugins/markdown-report/md_gen.ml
@@ -432,8 +432,8 @@ let gen_section_warnings env =
(text @@ glue [
plain ("The table below lists the " ^ plural warnings "warning");
plain "that have been emitted by the analyzer.";
- plain "They might put additional assumptions on the relevance";
- plain "of the analysis results and must be reviewed carefully";
+ plain "They might put additional assumptions on the relevance";
+ plain "of the analysis results and must be reviewed carefully";
]) @
(text @@ glue [
plain "Note that this does not take into account emitted alarms:";
diff --git a/src/plugins/server/data.ml b/src/plugins/server/data.ml
index 99b3bca1693f5846967499c9e6227e607e8fa8b2..3731b58b8eb4dca606fbb26672de6755e2758204 100644
--- a/src/plugins/server/data.ml
+++ b/src/plugins/server/data.ml
@@ -277,13 +277,13 @@ struct
| Some v -> Fmap.add name (D.to_json v) r in
{ member ; getter ; setter }
- let fields = Syntax.fields ~title:"Field" !fdocs
+ let fields () = [Syntax.fields ~title:"Field" !fdocs]
let syntax =
Syntax.publish ~page:R.page ~name:R.name
~descr:R.descr
~synopsis:(Syntax.record [])
- ~details:[fields] ()
+ ~details:(Markdown.delayed fields) ()
let of_json js =
List.fold_left
diff --git a/src/plugins/server/kernel_main.ml b/src/plugins/server/kernel_main.ml
index 24bd58d36ad81be45493e4616ec44c1a12456698..9c18bde3e567481bb4d896806af56e5654d57781 100644
--- a/src/plugins/server/kernel_main.ml
+++ b/src/plugins/server/kernel_main.ml
@@ -123,16 +123,16 @@ struct
let syntax = R.syntax
- let descr = Md.plain
- let kind = R.field "kind" ~descr:(descr "Message kind") (module LogKind)
- let plugin = R.field "plugin" ~descr:(descr "Emitter plugin") (module Jstring)
- let message = R.field "message" ~descr:(descr "Message text") (module Jstring)
+ let kind = R.field "kind" ~descr:(Md.plain "Message kind") (module LogKind)
+ let plugin = R.field "plugin" ~descr:(Md.plain "Emitter plugin") (module Jstring)
+ let message = R.field "message" ~descr:(Md.plain "Message text") (module Jstring)
let category = R.option "category"
- ~descr:(descr "Message category (DEBUG or WARNING)")
+ ~descr:(Md.plain "Message category (DEBUG or WARNING)")
(module Jstring)
- let source = R.option "source" ~descr:(descr "Source file position")
+ let source = R.option "source"
+ ~descr:(Md.plain "Source file position")
(module LogSource)
type t = Log.event
diff --git a/src/plugins/server/request.ml b/src/plugins/server/request.ml
index 0b1ef3b62f6b6107f155d12415622387eb9ec070..01fd23fe22225c248c14dad8b62b96be6102b73f 100644
--- a/src/plugins/server/request.ml
+++ b/src/plugins/server/request.ml
@@ -309,19 +309,18 @@ let register_sig (type a b) (s : (a,b) signature) (process : rq -> a -> b) =
in
let skind = Main.string_of_kind s.kind in
let title = Printf.sprintf "`%s` %s" skind s.name in
- let caption = Some s.descr in
let header = [ plain "Input", Center; plain "Output", Center] in
let content =
[[ Syntax.text @@ sy_input s.input ;
Syntax.text @@ sy_output s.output ]]
in
- let synopsis = Table { caption; header; content } in
- let content =
- [ synopsis ; Block s.details] @
+ let synopsis = Table { caption=None ; header; content } in
+ let description =
+ [ Block [Text s.descr ] ; synopsis ; Block s.details] @
doc_input s.input @
doc_output s.output
in
- let _ = Doc.publish ~page:s.page ~name:s.name ~title content [] in
+ let _ = Doc.publish ~page:s.page ~name:s.name ~title description [] in
Main.register s.kind s.name processor ;
s.defined <- true