Skip to content

Commit 1413188

Browse files
committed
Remove warnings, specific exception handling, and update example
1 parent a70d42d commit 1413188

2 files changed

Lines changed: 12 additions & 6 deletions

File tree

resources/tests/EasyCrypt_GenDoc_Tutorial.ec

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -104,6 +104,8 @@ type w.
104104
(* This comment is excluded from the generated documentation file *)
105105
(*& This comment is excluded from the generated documentation file &*)
106106
(*^ This comment is excluded from the generated documentation file ^*)
107+
However, anything outside these nested comments (but within
108+
the documentation comment, of course) is included.
107109
&*)
108110
type x.
109111

@@ -122,8 +124,9 @@ type y.
122124
formatted using (a non-standard dialect of) Markdown.
123125
The following is supported.
124126

125-
As first non-blank character on a line:
126-
- \! indicates a heading;
127+
As first non-blank character on a line (followed by a space):
128+
- \! indicates a heading (one for largest heading, two for second-largest
129+
heading, etc.);
127130
- \*, \+, or \- indicate an item of an unordered list;
128131
- \# indicates an item of an ordered list; and
129132
- \> indicates (a line of) a blockquote.
@@ -152,7 +155,7 @@ type z.
152155
- `Op` (or `Operator`),
153156
- `Ax` (or `Axiom`),
154157
- `Lem` (or `Lemma`),
155-
-`ModTy` (or `ModuleType`),
158+
- `ModTy` (or `ModuleType`),
156159
- `Mod` (or `Module`), and
157160
- `Th` (or `Theory`).
158161

src/ecDoc.ml

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,11 +9,13 @@ let styles_file : string =
99
Filename.concat Sites.doc "styles.css"
1010

1111
let stdlib_doc_dp (th : string) : string =
12-
""
12+
match th with
13+
| _ -> ""
1314

1415
(* -------------------------------------------------------------------- *)
1516
let from_stdlib (th : string) : bool =
16-
false
17+
match th with
18+
| _ -> false
1719

1820
(* -------------------------------------------------------------------- *)
1921
let c_filename ?(ext : string option) (nms : string list) =
@@ -100,7 +102,8 @@ let md_href_format (rth : string) (env : EcEnv.env) (hr : Markdown.href) : Html_
100102
let rec try_lookup = function
101103
| [] -> failwith (Printf.sprintf "No item/entity found with name `%s'." tname)
102104
| ik :: iks ->
103-
try itemkind_str_pl ik, itemkind_lookup_path ik tqs env with _ -> try_lookup iks
105+
try itemkind_str_pl ik, itemkind_lookup_path ik tqs env
106+
with EcEnv.LookupFailure _ -> try_lookup iks
104107
in
105108
let iks = [`Type; `Operator; `Axiom; `Lemma; `ModuleType; `Module; `Theory] in
106109
try_lookup iks

0 commit comments

Comments
 (0)