Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
7bfe9929
Commit
7bfe9929
authored
6 years ago
by
Virgile Prevosto
Browse files
Options
Downloads
Patches
Plain Diff
[output] work around a pandoc/latex issue over anchors' names
parent
34619b9f
No related branches found
Branches containing commit
No related tags found
Tags containing commit
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/plugins/markdown-report/md_gen.ml
+15
-6
15 additions, 6 deletions
src/plugins/markdown-report/md_gen.ml
with
15 additions
and
6 deletions
src/plugins/markdown-report/md_gen.ml
+
15
−
6
View file @
7bfe9929
...
...
@@ -10,6 +10,13 @@ let insert_remark_opt env anchor placeholder =
let
insert_remark
env
anchor
=
insert_remark_opt
env
anchor
[]
(* apparently, pandoc, or at least its latex output,
does not like anchors beginning with _ *)
let
sanitize_anchor
s
=
if
s
=
""
then
"a"
else
if
s
.
[
0
]
=
'
_'
then
"a"
^
s
else
s
let
all_eva_domains
=
[
"-eva-apron-box"
,
"box domain of the Apron library"
;
"-eva-apron-oct"
,
"octagon domain of the Apron library"
;
...
...
@@ -104,10 +111,11 @@ let section_stubs env =
(
fun
s
->
String
.
length
s
<>
0
&&
s
.
[
0
]
<>
'
@
'
&&
s
.
[
0
]
<>
'
-
'
)
(
fun
s
->
let
kf
=
Globals
.
Functions
.
find_by_name
s
in
let
anchor
=
sanitize_anchor
s
in
let
content
=
if
env
.
is_draft
then
insert_marks
env
s
if
env
.
is_draft
then
insert_marks
env
anchor
else
begin
let
comment
=
insert_remark
env
s
in
let
comment
=
insert_remark
env
anchor
in
Block
[
Text
[
Inline_code
s
;
Plain
"has the following specification"
];
...
...
@@ -116,14 +124,15 @@ let section_stubs env =
::
comment
end
in
H4
([
Inline_code
s
]
,
Some
s
)
::
content
)
H4
([
Inline_code
s
]
,
Some
anchor
)
::
content
)
l
in
let
describe_func
kf
=
let
name
=
Kernel_function
.
get_name
kf
in
let
anchor
=
sanitize_anchor
name
in
let
loc
=
Kernel_function
.
get_location
kf
in
let
content
=
if
env
.
is_draft
then
insert_marks
env
name
if
env
.
is_draft
then
insert_marks
env
anchor
else
(
Block
[
Text
...
...
@@ -134,9 +143,9 @@ let section_stubs env =
Printer
.
pp_global
(
GFun
(
Kernel_function
.
get_definition
kf
,
loc
))
])
::
insert_remark
env
name
::
insert_remark
env
anchor
in
H4
([
Inline_code
name
]
,
Some
name
)
::
content
H4
([
Inline_code
name
]
,
Some
anchor
)
::
content
in
let
content
=
if
stubbed_kf
<>
[]
then
begin
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment