diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/latex.ml | 23 | ||||
| -rw-r--r-- | src/sail.ml | 12 |
2 files changed, 17 insertions, 18 deletions
diff --git a/src/latex.ml b/src/latex.ml index f6aed63c..e42bb3f5 100644 --- a/src/latex.ml +++ b/src/latex.ml @@ -114,24 +114,16 @@ let latex_loc no_loc l = | _ -> docstring l ^^ no_loc -let latex_code ?label:(label=None) no_loc ((l, _) as annot) = - let open_listing = match label with - | None -> "\\begin{lstlisting}" - | Some l -> Printf.sprintf "\\begin{lstlisting}[label={%s}]" l - in - docstring l - ^^ string open_listing ^^ hardline - ^^ latex_loc no_loc l - ^^ string "\\end{lstlisting}" - module StringSet = Set.Make(String) let commands = ref StringSet.empty +let latex_dir = ref "" + let rec latex_command ?prefix:(prefix="") ?label:(label=None) cmd no_loc ((l, _) as annot) = let labelling = match label with | None -> "" - | Some l -> Printf.sprintf "\\phantomsection\\label{%s%s}" prefix l + | Some l -> Printf.sprintf "\\label{%s%s}" prefix l in let cmd = prefix ^ cmd in if StringSet.mem cmd !commands then @@ -139,11 +131,10 @@ let rec latex_command ?prefix:(prefix="") ?label:(label=None) cmd no_loc ((l, _) else begin commands := StringSet.add cmd !commands; - docstring l - ^^ string (Printf.sprintf "\\newsavebox{\\box%s}\n\\begin{lrbox}{\\box%s}\n\\begin{lstlisting}" cmd cmd) ^^ hardline - ^^ latex_loc no_loc l - ^^ string "\\end{lstlisting}\n\\end{lrbox}" ^^ hardline - ^^ string (Printf.sprintf "\\newcommand{\\sail%s}{\\begin{sail}\\usebox{\\box%s}%s\\end{sail}}" cmd cmd labelling) + let oc = open_out (cmd ^ "_sail.tex") in + output_string oc (Pretty_print_sail.to_string (latex_loc no_loc l)); + close_out oc; + string (Printf.sprintf "\\newcommand{\\sail%s}{%s " cmd labelling) ^^ (docstring l) ^^ string (Printf.sprintf "\\lstinputlisting{%s/%s_sail.tex}}" !latex_dir cmd) end let latex_command_id ?prefix:(prefix="") id no_loc annot = diff --git a/src/sail.ml b/src/sail.ml index 65473d86..006c0e58 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -310,8 +310,16 @@ let main() = (if !(opt_print_latex) then begin - let out = match !opt_file_out with None -> "out.tex" | Some s -> s ^ ".tex" in - let chan = open_out out in + let latex_dir = match !opt_file_out with None -> "sail_latex" | Some s -> s in + try + if not (Sys.is_directory latex_dir) then begin + prerr_endline ("Failure: latex output directory exists but is not a directory: " ^ latex_dir); + exit 1 + end + with Sys_error(_) -> Unix.mkdir latex_dir 0o755; + Sys.chdir latex_dir; + let chan = open_out "commands.tex" in + Latex.latex_dir := latex_dir; output_string chan (Pretty_print_sail.to_string (Latex.latex_defs ast)); close_out chan end |