Commit b114f58d authored by Loïc Correnson's avatar Loïc Correnson Committed by Virgile Prevosto
Browse files

[markdown] refactor codeblock smart-constructor

parent f1a0dbfa
......@@ -119,10 +119,18 @@ let link ?text ?page ?name () =
| 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 codeblock ?(lang="") content =
let buffer = Buffer.create 120 in
let fmt = Format.formatter_of_buffer buffer in
Format.pp_open_hvbox fmt 0 ;
Format.kfprintf
(fun fmt ->
Format.pp_close_box fmt () ;
Format.pp_print_flush fmt () ;
let code = Buffer.contents buffer |> String.trim in
let lines = String.split_on_char '\n' code in
[Code_block(lang,lines)]
) fmt content
let text text = [Text text]
let list items = [UL items]
......
......@@ -146,10 +146,11 @@ val enum : block list -> block
(** Description list *)
val description : (text * text) list -> block
(** [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
(** [codeblock lang "...."] returns a [Code_block] for [code],
written in [lang] with the given formatted content.
The code block content placed inside an englobing hv-box, trimed
and finally splitted into lines. *)
val codeblock : ?lang:string -> ('a,Format.formatter,unit,block) format4 -> 'a
(** {2 Document Elements}
......
......@@ -134,7 +134,7 @@ let section_stubs env =
else
let intro = Markdown.text @@ Markdown.format
"`%s` has the following specification" s in
let funspec = Markdown.codeblock "acsl"
let funspec = Markdown.codeblock ~lang:"acsl" "%a"
Printer.pp_funspec (Annotations.funspec kf) in
Block ( intro @ funspec ) :: insert_remark env anchor
in
......@@ -151,7 +151,7 @@ let section_stubs env =
let intro = Markdown.text @@ Markdown.format
"`%s` @[<h>is defined at %a@]"
name Cil_datatype.Location.pretty loc in
let fundecl = Markdown.codeblock "c"
let fundecl = Markdown.codeblock ~lang:"c" "%a"
Printer.pp_global (GFun (Kernel_function.get_definition kf,loc)) in
Block ( intro @ fundecl ) :: insert_remark env anchor
in
......@@ -373,7 +373,7 @@ let section_event is_err env nb event =
H2 (plain title, Some lab)
:: Block (
(text @@ plain "Message:") @
codeblock "log" Format.pp_print_string event.evt_message
codeblock "[%s] %s" event.evt_plugin event.evt_message
)
:: content
......@@ -461,7 +461,7 @@ let gen_section_alarms env =
let loc = string_of_loc @@ Cil_datatype.Stmt.loc s in
let loc_text = plain loc in
let emitter = code (Emitter.get_name e) in
let descr = codeblock "acsl" Printer.pp_code_annotation annot in
let descr = codeblock ~lang:"acsl" "%a" 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
......
......@@ -87,7 +87,7 @@ let make_message alarm annot remark =
let name = Alarms.get_name alarm in
let text = name ^ "." in
let kind = plain (name ^ ":") in
let descr = codeblock "acsl" Printer.pp_code_annotation annot in
let descr = codeblock ~lang:"acsl" "%a" Printer.pp_code_annotation annot in
let summary = Block (Text kind :: descr) in
let markdown =
match remark with
......
......@@ -67,8 +67,8 @@ Table: Warning reported by Frama-C
Message:
```log
out of bounds read. assert \valid_read(data + i);
```
[eva] out of bounds read. assert \valid_read(data + i);
```
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment