From 575340fbf3fb1a8a95f2612b5726787c6fd68ef5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 24 Oct 2019 14:49:38 +0200
Subject: [PATCH] [markdown] smart constructors
---
src/libraries/utils/markdown.ml | 106 +++++++++-----
src/libraries/utils/markdown.mli | 145 +++++++++++++++-----
src/plugins/markdown-report/eva_coverage.ml | 8 +-
src/plugins/markdown-report/md_gen.ml | 81 +++++------
src/plugins/markdown-report/sarif_gen.ml | 4 +-
src/plugins/server/doc.ml | 2 +-
src/plugins/server/request.ml | 4 +-
src/plugins/server/syntax.ml | 45 +++---
src/plugins/server/syntax.mli | 2 +-
9 files changed, 241 insertions(+), 156 deletions(-)
diff --git a/src/libraries/utils/markdown.ml b/src/libraries/utils/markdown.ml
index 612c40a9019..2f9e3555411 100644
--- a/src/libraries/utils/markdown.ml
+++ b/src/libraries/utils/markdown.ml
@@ -72,26 +72,65 @@ type pandoc_markdown =
elements: elements
}
-let plain s = [ Plain s]
+let glue ?sep ls =
+ match sep , ls with
+ | (None | Some []) , _ -> List.concat ls
+ | _ , [] -> []
+ | _ , [l] -> l
+ | Some s , ls -> (* tailrec *)
+ let rec aux w s = function
+ | [] -> List.rev w
+ | [e] -> List.rev_append w e
+ | e::el -> aux s (List.rev_append s (List.rev_append e w)) el
+ in aux s [] ls
+
+(* -------------------------------------------------------------------------- *)
+(* --- Formatting --- *)
+(* -------------------------------------------------------------------------- *)
+
+let plain s = [ Plain s ]
+let emph s = [ Emph s ]
+let bold s = [ Bold s ]
+let code s = [ Inline_code s ]
+
+let format txt = Format.kasprintf plain txt
+
+let image ~alt ~file = [Image(alt,file)]
+
+let mklink ?text href =
+ let txt =
+ match text with Some txt -> txt | None ->
+ let tt = match href with URL u -> u | Page p -> p | Section(_,s) -> s in
+ [Inline_code tt]
+ in [Link(txt, href)]
+
+let url ?text href = mklink ?text (URL href)
+
+let link ?text ?page ?name () =
+ mklink ?text @@ match page, name with
+ | None, None -> Page ""
+ | Some p, None -> Page p
+ | None, Some a -> Section("",a)
+ | Some p, Some a -> Section(p,a)
+
+let codeblock lang pp code =
+ let s = Format.asprintf "@[%a@]" pp code in
+ let lines = String.split_on_char '\n' s in
+ [Code_block (lang, lines)]
-let plain_format txt = Format.kasprintf plain txt
+let text text = [Text text]
+let list items = [UL items]
+let enum items = [OL items]
+let description items = [DL items]
-let link_current_page sec = Section("", sec)
+let block b = [Block b]
+let par text = [Block [Text text]]
-let plain_link h =
- let s = match h with
- | URL url -> url
- | Page p -> p
- | Section (_,s) -> s
- in
- Link ([Inline_code s], h)
+(* -------------------------------------------------------------------------- *)
+(* --- Sectioning --- *)
+(* -------------------------------------------------------------------------- *)
-let codelines lang pp code =
- let s = Format.asprintf "@[%a@]" pp code in
- let lines = String.split_on_char '\n' s in
- Code_block (lang, lines)
-
-let raw_markdown filename =
+let rawfile filename =
let chan = open_in filename in
let res = ref [] in
try
@@ -101,17 +140,9 @@ let raw_markdown filename =
assert false
with End_of_file ->
close_in chan;
- Raw (List.rev !res)
-
-let glue ?(sep=[]) texts =
- let rec aux = function
- | [] -> []
- | [t] -> t
- | hd::tl -> hd @ sep @ aux tl
- in
- aux texts
+ [Raw (List.rev !res)]
-let id m =
+let label m =
let buffer = Buffer.create (String.length m) in
let lowercase = Char.lowercase_ascii in
let dash = ref false in
@@ -129,12 +160,8 @@ let id m =
Buffer.contents buffer
let section ?name ~title elements =
- let anchor =
- match name with
- | None -> id title
- | Some n -> n
- in
- (H1 (plain title, Some anchor)) :: elements
+ let anchor = label @@ match name with Some n -> n | None -> title in
+ (H1 ([Plain title], Some anchor)) :: elements
let subsections header body =
let body =
@@ -151,11 +178,11 @@ let subsections header body =
let mk_date () =
let tm = Unix.gmtime (Unix.time()) in
- plain
- (Printf.sprintf "%d-%02d-%02d"
- (1900 + tm.Unix.tm_year) (1 + tm.Unix.tm_mon) tm.Unix.tm_mday)
+ format "%d-%02d-%02d"
+ (1900 + tm.Unix.tm_year)
+ (1 + tm.Unix.tm_mon) tm.Unix.tm_mday
-let pandoc ?(title=plain "") ?(authors=[]) ?(date=mk_date()) elements =
+let pandoc ?(title=[Plain ""]) ?(authors=[]) ?(date=mk_date()) elements =
{ title; authors; date; elements }
let relativize page target =
@@ -182,7 +209,7 @@ let relativize page target =
let pp_href ?(page="") fmt = function
| URL s -> Format.pp_print_string fmt s
| Page s -> Format.pp_print_string fmt (relativize page s)
- | Section (p,s) -> Format.fprintf fmt "%s#%s" (relativize page p) (id s)
+ | Section (p,s) -> Format.fprintf fmt "%s#%s" (relativize page p) (label s)
let rec pp_inline ?page fmt =
function
@@ -200,7 +227,10 @@ and pp_text ?page fmt l =
| [] -> ()
| [ elt ] -> pp_inline ?page fmt elt
| elt :: text ->
- Format.fprintf fmt "%a@ %a" (pp_inline ?page) elt (pp_text ?page) text
+ (* tailrec *)
+ pp_inline ?page fmt elt ;
+ Format.pp_print_space fmt () ;
+ pp_text ?page fmt text
let pp_lab fmt = function
| None -> ()
diff --git a/src/libraries/utils/markdown.mli b/src/libraries/utils/markdown.mli
index 71ba39525a2..afa491d9302 100644
--- a/src/libraries/utils/markdown.mli
+++ b/src/libraries/utils/markdown.mli
@@ -20,10 +20,17 @@
(* *)
(**************************************************************************)
+(** {2 Markdown Document}
+ Structured representation of Markdown content. *)
+
+(** Table columns alignment *)
type align = Left | Center | Right
+(** Local refs and URLs *)
type href =
- | URL of string (** uninterpreted URL *)
+ | URL of string
+ (** URL href is printed as it is. *)
+
| Page of string
(** URL relative to a common root.
During pretty-printing, if given the path of the current
@@ -31,20 +38,22 @@ type href =
when writing to [foo/bar.md], [Page "foo/bla.md"] will be output as
[(bla.md)].
*)
- | Section of string * string (** URL of an anchor within a [Page] *)
+
+ | Section of string * string
+ (** URL of an anchor within a [Page], see above. *)
type inline =
- | Plain of string
- | Emph of string
- | Bold of string
- | Inline_code of string
- | Link of text * href
- | Image of string * string (** [Image(alt,location)] *)
+ | Plain of string (** Printed as it is *)
+ | Emph of string (** Printed as ["_……_"] *)
+ | Bold of string (** Printed as ["**……**"] *)
+ | Inline_code of string (** Printed as ["`……`"] *)
+ | Link of text * href (** Hyperlink with text and URL *)
+ | Image of string * string (** [Image(alt,path)] with alternative text and image file *)
-and text = inline list
+and text = inline list (** Inline elements separated by spaces *)
type block_element =
- | Text of text (** single paragraph of text. *)
+ | Text of text (** Single paragraph of text. *)
| Block_quote of element list
| UL of block list
| OL of block list
@@ -78,34 +87,92 @@ type pandoc_markdown =
elements: elements
}
-(** creates a document from a list of elements and optional metadatas.
- Defaults are:
- - title: empty
- - authors: empty list
- - date: current day, in ISO format
-*)
-val pandoc:
- ?title:text -> ?authors: text list -> ?date: text -> elements ->
- pandoc_markdown
+(** {2 Formatting Utilities}
-(** get the content of a file as raw markdown.
- @raise Sys_error if there's no such file.
+ Remark: [text] values are list of [inline] values, hence
+ you may combined with the [(@)] operator or with the [glue ?sep] utility
+ function (see below).
*)
-val raw_markdown: string -> element
+(** Plain markdown *)
val plain: string -> text
-val plain_format: ('a, Format.formatter, unit, text) format4 -> 'a
+(** Emph text *)
+val emph: string -> text
+
+(** Bold text *)
+val bold: string -> text
+
+(** Inline code *)
+val code: string -> text
+
+(** Image *)
+val image: alt:string -> file:string -> text
+
+(** Local links *)
+val link: ?text:text -> ?page:string -> ?name:string -> unit -> text
+
+(** URL links *)
+val url: ?text:text -> string -> text
+
+(** Plain markdown content of the formatted string *)
+val format: ('a, Format.formatter, unit, text) format4 -> 'a
+
+(** {2 Blocks Utilities}
+
+ Remark: [block] values are list of [block_element] values, hence
+ you may combined with the [(@)] operator or with the [glue ?sep] utility
+ function (see below).
+*)
+
+(** Text Block *)
+val text : text -> block
+
+(** Itemized list *)
+val list : block list -> block
+
+(** Enumerated list *)
+val enum : block list -> block
-(** glue text fragments. *)
-val glue: ?sep: text -> text list -> text
+(** Description list *)
+val description : (text * text) list -> block
-(** transforms a string into an anchor name, roughly following
- pandoc's conventions.
+(** [codeblock lang pp code] returns a [Code_block] for [code],
+ written in [lang], as pretty-printed by [pp]. *)
+val codeblock:
+ string -> (Format.formatter -> 'a -> unit) -> 'a -> block
+
+(** {2 Document Elements}
+
+ Remark: [elements] values are list of [element] values, hence
+ you may combined with the [(@)] operator or with the [glue ?sep] utility
+ function (see below).
*)
-val id: string -> string
-(** adds a [H1] header with the given [title] on top of the given elements.
+(** Single Paragraph element *)
+val par : text -> elements
+
+(** Block element *)
+val block : block -> elements
+
+(** Get the content of a file as raw markdown.
+ @raise Sys_error if there's no such file.
+*)
+val rawfile: string -> elements
+
+(** {2 Document Structure} *)
+
+(** Creates a document from a list of elements and optional metadatas.
+ Defaults are:
+ - title: empty
+ - authors: empty list
+ - date: current day, in ISO format
+*)
+val pandoc:
+ ?title:text -> ?authors: text list -> ?date: text -> elements ->
+ pandoc_markdown
+
+(** Adds a [H1] header with the given [title] on top of the given elements.
If name is not explicitly provided,
the header will have as associated anchor [id title]
*)
@@ -117,16 +184,20 @@ val section: ?name:string -> title:string -> elements -> elements
*)
val subsections: elements -> elements list -> elements
-(** returns an internal link relative to the current page *)
-val link_current_page: string -> href
+(** {2 Other Utilities} *)
+
+(** Glue fragments, typically used for combining [text], [block]
+ and [elements].
+ Default separator is empty. The function is tail-recursive. *)
+val glue: ?sep:'a list -> 'a list list -> 'a list
-(** gives a link whose text is the URL itself. *)
-val plain_link: href -> inline
+(** Transforms a string into an anchor name, roughly following
+ pandoc's conventions. This function is automatically used
+ by pretty-printers and smart constructors to normalize section names
+ and local links. *)
+val label: string -> string
-(** [codelines lang pp code] returns a [Code_block] for [code], written
- in [lang], as pretty-printed by [pp]. *)
-val codelines:
- string -> (Format.formatter -> 'a -> unit) -> 'a -> block_element
+(** {2 Pretty-printers} *)
val pp_inline: ?page:string -> Format.formatter -> inline -> unit
diff --git a/src/plugins/markdown-report/eva_coverage.ml b/src/plugins/markdown-report/eva_coverage.ml
index 56b55d11303..d60250838fc 100644
--- a/src/plugins/markdown-report/eva_coverage.ml
+++ b/src/plugins/markdown-report/eva_coverage.ml
@@ -190,7 +190,7 @@ let md_gen () =
let vis = new eva_coverage_vis ~from_entry_point:false in
let stats = vis#compute () in
let summary_whole =
- Markdown.plain_format
+ Markdown.format
"There are %d function definitions that are not stubbed. They represent \
%d statements, of which %d are potentially reachable through EVA, \
resulting in a **statement coverage of %.1f%%** with respect to the \
@@ -203,7 +203,7 @@ let md_gen () =
let vis = new eva_coverage_vis ~from_entry_point:true in
let stats = vis#compute () in
let summary =
- Markdown.plain_format
+ Markdown.format
"There were potentially %d functions syntactically reachable from %s."
stats.syntactic_calls main
in
@@ -211,14 +211,14 @@ let md_gen () =
if stats.indirect_calls = 0 then summary
else
summary @
- Markdown.plain_format
+ Markdown.format
"In addition, %d were found potentially reachable through \
indirect calls."
stats.indirect_calls
in
let summary =
summary @
- Markdown.plain_format
+ Markdown.format
"These functions contain %d statements, \
of which %d are potentially reachable according to EVA, resulting in \
a **statement coverage of %.1f%%** with respect to the perimeter set \
diff --git a/src/plugins/markdown-report/md_gen.ml b/src/plugins/markdown-report/md_gen.ml
index 538ff9f2eb2..7976815caac 100644
--- a/src/plugins/markdown-report/md_gen.ml
+++ b/src/plugins/markdown-report/md_gen.ml
@@ -131,15 +131,12 @@ let section_stubs env =
let anchor = sanitize_anchor s in
let content =
if env.is_draft then insert_marks env anchor
- else begin
- let comment = insert_remark env anchor in
- Block
- [ Text
- [Inline_code s; Plain "has the following specification"];
- codelines
- "acsl" Printer.pp_funspec (Annotations.funspec kf)]
- :: comment
- end
+ else
+ let intro = Markdown.text @@ Markdown.format
+ "`%s` has the following specification" s in
+ let funspec = Markdown.codeblock "acsl"
+ Printer.pp_funspec (Annotations.funspec kf) in
+ Block ( intro @ funspec ) :: insert_remark env anchor
in
H4 ([Inline_code s], Some anchor) :: content)
l
@@ -151,16 +148,12 @@ let section_stubs env =
let content =
if env.is_draft then insert_marks env anchor
else
- (Block
- [ Text
- (Inline_code name ::
- plain_format
- "@[<h>is defined at %a@]" Cil_datatype.Location.pretty loc);
- codelines "c"
- Printer.pp_global
- (GFun (Kernel_function.get_definition kf,loc))
- ])
- :: insert_remark env anchor
+ let intro = Markdown.text @@ Markdown.format
+ "`%s` @[<h>is defined at %a@]"
+ name Cil_datatype.Location.pretty loc in
+ let fundecl = Markdown.codeblock "c"
+ Printer.pp_global (GFun (Kernel_function.get_definition kf,loc)) in
+ Block ( intro @ fundecl ) :: insert_remark env anchor
in
H4 ([Inline_code name], Some anchor) :: content
in
@@ -449,12 +442,11 @@ let gen_section_warnings env =
Plain "They might put additional assumptions on the relevance";
Plain "of the analysis results and must be reviewed carefully";
];
- Text [
- Plain "Note that this does not take into account emitted alarms:";
- Plain "they are reported in";
- Link (plain "the next section",
- Markdown.link_current_page "alarms")
- ]
+ Text (
+ plain "Note that this does not take into account emitted alarms:"@
+ plain "they are reported in"@
+ Markdown.link ~text:(plain "the next section") ~name:"alarms" ()
+ )
];
make_warnings_table warnings
]
@@ -467,33 +459,29 @@ let gen_section_warnings env =
let gen_section_alarms env =
let treat_alarm e kf s ~rank:_ alarm annot (i, sec, content) =
- let kind = plain (Alarms.get_name alarm) in
+ let kind = Alarms.get_name alarm in
let label = "Alarm-" ^ string_of_int i in
- let link = [Link (plain_format "%d" i, link_current_page label)] in
+ let link = link ~text:(format "%d" i) ~name:label () in
let func = plain (Kernel_function.get_name kf) in
let loc = string_of_loc (Cil_datatype.Stmt.loc s) in
let loc_text = plain loc in
let emitter = plain (Emitter.get_name e) in
- let descr = codelines "acsl" Printer.pp_code_annotation annot in
- let sec_title = plain_format "Alarm %d at %s" i loc in
+ let descr = codeblock "acsl" Printer.pp_code_annotation annot in
+ let sec_title = format "Alarm %d at %s" i loc in
let sec_content =
if env.is_draft then
- Block [ descr ] :: insert_marks env label
+ Block descr :: insert_marks env label
else
Block
- [
- Text
- (plain
- "The following ACSL assertion must hold to avoid \
- an undefined behavior ("
- @ kind @ plain ")");
- descr
- ]
+ ( (text @@ format
+ "The following ACSL assertion must hold to avoid \
+ an undefined behavior (%s)" kind)
+ @ descr )
:: insert_remark env label
in
(i+1,
sec @ H2 (sec_title, Some label) :: sec_content,
- [ link; kind; emitter; func; loc_text ] :: content)
+ [ link; plain kind; emitter; func; loc_text ] :: content)
in
let _,sections, content = Alarms.fold treat_alarm (0,[],[]) in
let content = List.rev content in
@@ -563,14 +551,13 @@ let gen_section_callgraph env =
callstacks whose analysis is the most costly."
:: insert_marks env anchor
else
- Block [
- Text [
- Plain "The image below shows the flamegraph (";
- plain_link (URL "http://www.brendangregg.com/flamegraphs.html");
- Plain ") for the chosen entry point."
- ]]
- :: Block [ Text [Image ("Flamegraph visualization.", f)] ]
- :: insert_remark env anchor
+ par (
+ plain "The image below shows the flamegraph (" @
+ url "http://www.brendangregg.com/flamegraphs.html" @
+ plain ") for the chosen entry point."
+ )
+ @ par (image ~alt:"Flamegraph visualization." ~file:f)
+ @ insert_remark env anchor
in
H1 (plain "Flamegraph", Some anchor) :: content
end
diff --git a/src/plugins/markdown-report/sarif_gen.ml b/src/plugins/markdown-report/sarif_gen.ml
index 011fb79325a..5efe92ff894 100644
--- a/src/plugins/markdown-report/sarif_gen.ml
+++ b/src/plugins/markdown-report/sarif_gen.ml
@@ -87,8 +87,8 @@ let make_message alarm annot remark =
let name = Alarms.get_name alarm in
let text = name ^ "." in
let kind = plain (name ^ ":") in
- let descr = codelines "acsl" Printer.pp_code_annotation annot in
- let summary = Block [Text kind; descr] in
+ let descr = codeblock "acsl" Printer.pp_code_annotation annot in
+ let summary = Block (Text kind :: descr) in
let markdown =
match remark with
| [] -> summary :: gen_remark alarm
diff --git a/src/plugins/server/doc.ml b/src/plugins/server/doc.ml
index b484beb24bc..5db96f030f9 100644
--- a/src/plugins/server/doc.ml
+++ b/src/plugins/server/doc.ml
@@ -74,7 +74,7 @@ let page chapter ~title ~filename =
Printf.sprintf "%s/%s/server/%s" Config.datadir name filename in
let intro =
if Sys.file_exists intro
- then [Markdown.raw_markdown intro]
+ then Markdown.rawfile intro
else Markdown.(section ~title []) in
let order = incr order ; !order in
let page = { order ; rootdir ; path ;
diff --git a/src/plugins/server/request.ml b/src/plugins/server/request.ml
index 69daa664bdc..0b1ef3b62f6 100644
--- a/src/plugins/server/request.ml
+++ b/src/plugins/server/request.ml
@@ -312,8 +312,8 @@ let register_sig (type a b) (s : (a,b) signature) (process : rq -> a -> b) =
let caption = Some s.descr in
let header = [ plain "Input", Center; plain "Output", Center] in
let content =
- [[ Syntax.format @@ sy_input s.input ;
- Syntax.format @@ sy_output s.output ]]
+ [[ Syntax.text @@ sy_input s.input ;
+ Syntax.text @@ sy_output s.output ]]
in
let synopsis = Table { caption; header; content } in
let content =
diff --git a/src/plugins/server/syntax.ml b/src/plugins/server/syntax.ml
index fc97bc44c6f..3f69008114a 100644
--- a/src/plugins/server/syntax.ml
+++ b/src/plugins/server/syntax.ml
@@ -55,8 +55,8 @@ type t = { atomic:bool ; text:Markdown.text }
let atom md = { atomic=true ; text=md }
let flow md = { atomic=false ; text=md }
+let text { text } = text
-let format { text } = text
let protect a =
if a.atomic then a.text else Markdown.((Plain "(") :: a.text @ [Plain ")"])
@@ -66,24 +66,22 @@ let publish ~page ~name ~descr ~synopsis ?(details = []) () =
let id = Printf.sprintf "data-%s" name in
let title = Printf.sprintf "`DATA` %s" name in
let href = Doc.href page id in
- let link_title = Printf.sprintf "_%s_" name in
- let link = Markdown.(Link (plain link_title, href)) in
- let syntax =
- Markdown.(
- Text
- (Plain ">" :: link :: Plain "::=" :: synopsis.text))
- in
+ let link_title = Markdown.emph name in
+ let data_link = Markdown.Link(link_title, href) in
+ let syntax = Markdown.(Text (
+ Plain "<" :: data_link :: Plain ">" :: Plain ":=" :: synopsis.text
+ )) in
let content = Markdown.((Block [Text descr; syntax]) :: details) in
let _href = Doc.publish ~page ~name:id ~title ~index:[name] content [] in
- atom @@ [link]
+ atom [data_link]
-let unit = atom @@ [Markdown.Plain "-"]
-let any = atom @@ [Markdown.Emph "any"]
-let int = atom @@ [Markdown.Emph "int"]
-let ident = atom @@ [Markdown.Emph "ident"]
-let string = atom @@ [Markdown.Emph "string"]
-let number = atom @@ [Markdown.Emph "number"]
-let boolean = atom @@ [Markdown.Emph "boolean"]
+let unit = atom [Markdown.Plain "-"]
+let any = atom [Markdown.Emph "any"]
+let int = atom [Markdown.Emph "int"]
+let ident = atom [Markdown.Emph "ident"]
+let string = atom [Markdown.Emph "string"]
+let number = atom [Markdown.Emph "number"]
+let boolean = atom [Markdown.Emph "boolean"]
let escaped name =
Markdown.Inline_code (Printf.sprintf "'%s'" @@ String.escaped name)
@@ -121,13 +119,12 @@ type field = {
let fields ~title (fds : field list) =
let open Markdown in
let caption = Some (plain "Fields description") in
- let header =
- [plain title, Left; plain "Format", Center; plain "Description", Left]
- in
- let content =
- List.map
- (fun f -> [[Markdown.Inline_code f.name]; format f.syntax ; f.descr]) fds
- in
- Markdown.Table { caption; header; content }
+ let header = [
+ plain title, Left;
+ plain "Format", Center;
+ plain "Description", Left
+ ] in
+ let field f = [[Inline_code f.name]; f.syntax.text ; f.descr] in
+ Markdown.Table { caption; header; content = List.map field fds }
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/syntax.mli b/src/plugins/server/syntax.mli
index c56312909ed..33ae244e8f3 100644
--- a/src/plugins/server/syntax.mli
+++ b/src/plugins/server/syntax.mli
@@ -26,7 +26,7 @@
type t
-val format : t -> Markdown.text
+val text : t -> Markdown.text
(** The provided synopsis must be very short, to fit in one line.
Extended definition, like record fields and such, must be detailed in
--
GitLab