Skip to content

Commit

Permalink
Merge pull request #97 from jrtc27/label-prefix
Browse files Browse the repository at this point in the history
latex: Prefix label names with the specified -latex_prefix
  • Loading branch information
Alasdair authored Sep 28, 2020
2 parents 882850d + 57fd067 commit c79b275
Show file tree
Hide file tree
Showing 2 changed files with 25 additions and 27 deletions.
50 changes: 24 additions & 26 deletions src/latex.ml
Original file line number Diff line number Diff line change
Expand Up @@ -159,7 +159,7 @@ let category_name_simple = function
(* Generate a unique latex identifier from a Sail identifier. We store
a mapping from identifiers to strings in state so we always return
the same latex id for a sail id. *)
let latex_id id =
let latex_id_raw id =
if Bindings.mem id state.generated_names then
Bindings.find id state.generated_names
else
Expand Down Expand Up @@ -197,10 +197,25 @@ let latex_id id =
state.generated_names <- Bindings.add id str state.generated_names;
str

let refcode_string str =
Str.global_replace (Str.regexp "_") "zy" (Util.zencode_string str)
let latex_cat_id cat id = !opt_prefix ^ category_name cat ^ latex_id_raw id

let refcode_id id = refcode_string (string_of_id id)
let rec app_code (E_aux (exp, _)) =
match exp with
| E_app (f, [exp]) when Id.compare f (mk_id "Some") = 0 -> app_code exp
| E_app (f, [exp]) -> latex_id_raw f ^ app_code exp
| E_app (f, _) -> latex_id_raw f
| E_id id -> latex_id_raw id
| _ -> ""

let refcode_cat_string cat str =
let refcode_str = Str.global_replace (Str.regexp "_") "zy" (Util.zencode_string str) in
!opt_prefix ^ category_name_val cat ^ refcode_str

let refcode_cat_id prefix id = refcode_cat_string prefix (string_of_id id)

let refcode_id = refcode_cat_id Val

let refcode_string = refcode_cat_string Val

let inline_code str = sprintf "\\lstinline{%s}" str

Expand Down Expand Up @@ -231,7 +246,7 @@ let latex_of_markdown str =
| Bold elems -> sprintf "\\textbf{%s}" (format elems)
| Ref (r, "THIS", alt, _) ->
begin match state.this with
| Some id -> sprintf "\\hyperref[%s]{%s}" (refcode_string (string_of_id id)) (replace_this alt)
| Some id -> sprintf "\\hyperref[%s]{%s}" (refcode_id id) (replace_this alt)
| None -> failwith "Cannot create link to THIS"
end
| Ref (r, name, alt, _) ->
Expand Down Expand Up @@ -337,42 +352,25 @@ let doc_spec_simple (VS_aux (VS_val_spec (ts, id, ext, is_cast), _)) =

let rec latex_command cat id no_loc ((l, _) as annot) =
state.this <- Some id;
let labelname = match cat with
| Val -> sprintf "%s" (refcode_id id)
| _ -> sprintf "%s%s" (category_name cat) (refcode_id id)
in
(* To avoid problems with verbatim environments in commands, we have
to put the sail code for each command in a separate file. *)
let code_file = category_name cat ^ Util.file_encode_string (string_of_id id) ^ ".tex" in
let chan = open_out (Filename.concat !opt_directory code_file) in
let doc = if cat = Val then no_loc else latex_loc no_loc l in
output_string chan (Pretty_print_sail.to_string doc);
close_out chan;
let command = sprintf "\\%s%s%s" !opt_prefix (category_name cat) (latex_id id) in
let command = sprintf "\\%s" (latex_cat_id cat id) in
if StringSet.mem command state.commands then
(Reporting.warn "" l ("Multiple instances of " ^ string_of_id id ^ " only generating latex for the first"); empty)
else
begin
state.commands <- StringSet.add command state.commands;

ksprintf string "\\newcommand{%s}{\\saildoclabelled{%s}{\\saildoc%s{" command labelname (category_name_simple cat)
ksprintf string "\\newcommand{%s}{\\saildoclabelled{%s}{\\saildoc%s{" command (refcode_cat_id cat id) (category_name_simple cat)
^^ docstring l ^^ string "}{"
^^ ksprintf string "\\lstinputlisting[language=sail]{%s}}}}" (Filename.concat !opt_directory code_file)
end

let latex_label str id =
string (Printf.sprintf "\\label{%s:%s}" str (Util.zencode_string (string_of_id id)))

let counter = ref 0

let rec app_code (E_aux (exp, _)) =
match exp with
| E_app (f, [exp]) when Id.compare f (mk_id "Some") = 0 -> app_code exp
| E_app (f, [exp]) -> latex_id f ^ app_code exp
| E_app (f, _) -> latex_id f
| E_id id -> latex_id id
| _ -> ""

let latex_funcls def =
let module StringMap = Map.Make(String) in
let counter = ref 0 in
Expand Down Expand Up @@ -498,14 +496,14 @@ let defs (Defs defs) =
identifiers then outputs the correct mangled command. *)
let id_command cat ids =
sprintf "\\newcommand{\\%s%s}[1]{\n " !opt_prefix (category_name cat)
^ Util.string_of_list "%\n " (fun id -> sprintf "\\ifstrequal{#1}{%s}{\\%s%s%s}{}" (string_of_id id) !opt_prefix (category_name cat) (latex_id id))
^ Util.string_of_list "%\n " (fun id -> sprintf "\\ifstrequal{#1}{%s}{\\%s}{}" (string_of_id id) (latex_cat_id cat id))
(IdSet.elements ids)
^ "}"
|> string
in
let ref_command cat ids =
sprintf "\\newcommand{\\%sref%s}[2]{\n " !opt_prefix (category_name cat)
^ Util.string_of_list "%\n " (fun id -> sprintf "\\ifstrequal{#1}{%s}{\\hyperref[%s%s]{#2}}{}" (string_of_id id) (category_name_val cat) (refcode_id id))
^ Util.string_of_list "%\n " (fun id -> sprintf "\\ifstrequal{#1}{%s}{\\hyperref[%s]{#2}}{}" (string_of_id id) (refcode_cat_id cat id))
(IdSet.elements ids)
^ "}"
|> string
Expand Down
2 changes: 1 addition & 1 deletion src/sail.ml
Original file line number Diff line number Diff line change
Expand Up @@ -162,7 +162,7 @@ let options = Arg.align ([
" pretty print the input to LaTeX");
( "-latex_prefix",
Arg.String (fun prefix -> Latex.opt_prefix := prefix),
"<prefix> set a custom prefix for generated LaTeX macro command (default sail)");
"<prefix> set a custom prefix for generated LaTeX labels and macro commands (default sail)");
( "-latex_full_valspecs",
Arg.Clear Latex.opt_simple_val,
" print full valspecs in LaTeX output");
Expand Down

0 comments on commit c79b275

Please sign in to comment.