diff options
Diffstat (limited to 'tools/coq_tex.ml')
-rw-r--r-- | tools/coq_tex.ml | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml index ca21f706..383a68df 100644 --- a/tools/coq_tex.ml +++ b/tools/coq_tex.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -79,7 +79,7 @@ let expos = Str.regexp "^" let tex_escaped s = let dollar = "\\$" and backslash = "\\\\" and expon = "\\^" in - let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>]") in + let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>']") in let adapt_delim = function | "_" | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c | "\\" -> "{\\char'134}" @@ -88,6 +88,7 @@ let tex_escaped s = | " " -> "~" | "<" -> "{<}" | ">" -> "{>}" + | "'" -> "{\\textquotesingle}" | _ -> assert false in let adapt = function @@ -116,7 +117,7 @@ let insert texfile coq_output result = let next_block k = if !last_read = "" then last_read := input_line c_coq; (* skip k prompts *) - for i = 1 to k do + for _i = 1 to k do last_read := remove_prompt !last_read; done; (* read and return the following lines until a prompt is found *) @@ -170,9 +171,10 @@ let insert texfile coq_output result = if Str.string_match end_coq_example s 0 then begin just_after () end else begin - if !verbose then Printf.printf "Coq < %s\n" s; - if (not first_block) & k=0 then output_string c_out "\\medskip\n"; - if show_questions then encapsule false c_out ("Coq < " ^ s); + let prompt = if k = 0 then "Coq < " else " " in + if !verbose then Printf.printf "%s%s\n" prompt s; + if (not first_block) && k=0 then output_string c_out "\\medskip\n"; + if show_questions then encapsule false c_out (prompt ^ s); if has_match dot_end_line s then begin let bl = next_block (succ k) in if !verbose then List.iter print_endline bl; @@ -209,7 +211,7 @@ let insert texfile coq_output result = (* Process of one TeX file *) -let rm f = try Sys.remove f with _ -> () +let rm f = try Sys.remove f with any -> () let one_file texfile = let inputv = Filename.temp_file "coq_tex" ".v" in @@ -233,9 +235,9 @@ let one_file texfile = insert texfile coq_output result; (* 4. clean up *) rm inputv; rm coq_output - with e -> begin + with reraise -> begin rm inputv; rm coq_output; - raise e + raise reraise end (* Parsing of the command line, check of the Coq command and process |