diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /tools/coq-tex.ml4 | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'tools/coq-tex.ml4')
-rw-r--r-- | tools/coq-tex.ml4 | 292 |
1 files changed, 0 insertions, 292 deletions
diff --git a/tools/coq-tex.ml4 b/tools/coq-tex.ml4 deleted file mode 100644 index 4c11725c..00000000 --- a/tools/coq-tex.ml4 +++ /dev/null @@ -1,292 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id: coq-tex.ml4 9532 2007-01-24 16:04:29Z bgregoir $ *) - -(* coq-tex - * JCF, 16/1/98 - * adapted from caml-tex (perl script written by Xavier Leroy) - * - * Perl isn't as portable as it pretends to be, and is quite difficult - * to read and maintain... Let us rewrite the stuff in Caml! *) - -let _ = - match Sys.os_type with - | "Unix" -> () - | _ -> begin - print_string "This program only runs under Unix !\n"; - flush stdout; - exit 1 - end - -let linelen = ref 72 -let output = ref "" -let output_specified = ref false -let image = ref "" -let cut_at_blanks = ref false -let verbose = ref false -let slanted = ref false -let hrule = ref false -let small = ref false - -let coq_prompt = Str.regexp "Coq < " -let any_prompt = Str.regexp "^[A-Z0-9a-z_\\$']* < " - -let remove_prompt s = Str.replace_first any_prompt "" s - -(* First pass: extract the Coq phrases to evaluate from [texfile] - * and put them into the file [inputv] *) - -let begin_coq = Str.regexp "\\\\begin{coq_\\(example\\|example\\*\\|example\\#\\|eval\\)}[ \t]*$" -let end_coq = Str.regexp "\\\\end{coq_\\(example\\|example\\*\\|example\\#\\|eval\\)}[ \t]*$" - -let extract texfile inputv = - let chan_in = open_in texfile in - let chan_out = open_out inputv in - let rec inside () = - let s = input_line chan_in in - if Str.string_match end_coq s 0 then - outside () - else begin - output_string chan_out (s ^ "\n"); - inside () - end - and outside () = - let s = input_line chan_in in - if Str.string_match begin_coq s 0 then - inside () - else - outside () - in - try - output_string chan_out - ("Set Printing Width " ^ (string_of_int !linelen) ^".\n"); - outside () - with End_of_file -> - begin close_in chan_in; close_out chan_out end - -(* Second pass: insert the answers of Coq from [coq_output] into the - * TeX file [texfile]. The result goes in file [result]. *) - -let begin_coq_example = - Str.regexp "\\\\begin{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$" -let begin_coq_eval = Str.regexp "\\\\begin{coq_eval}[ \t]*$" -let end_coq_example = Str.regexp "\\\\end{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$" -let end_coq_eval = Str.regexp "\\\\end{coq_eval}[ \t]*$" -let dot_end_line = Str.regexp "\\.[ \t]*\\((\\*.*\\*)\\)?[ \t]*$" - -let has_match r s = - try let _ = Str.search_forward r s 0 in true with Not_found -> false - -let percent = Str.regexp "%" -let bang = Str.regexp "!" -let expos = Str.regexp "^" - -let tex_escaped s = - let rec trans = parser - | [< s1 = (parser - | [< ''_'|'$'|'{'|'}'|'&'|'%'|'#' as c >] -> - "\\" ^ (String.make 1 c) - | [< ''\\' >] -> "{\\char'134}" - | [< ''^' >] -> "{\\char'136}" - | [< ''~' >] -> "{\\char'176}" - | [< '' ' >] -> "~" - | [< ''<' >] -> "{<}" - | [< ''>' >] -> "{>}" - | [< 'c >] -> String.make 1 c); - s2 = trans >] -> s1 ^ s2 - | [< >] -> "" - in - trans (Stream.of_string s) - -let encapsule sl c_out s = - if sl then - Printf.fprintf c_out "\\texttt{\\textit{%s}}\\\\\n" (tex_escaped s) - else - Printf.fprintf c_out "\\texttt{%s}\\\\\n" (tex_escaped s) - -let print_block c_out bl = - List.iter (fun s -> if s="" then () else encapsule !slanted c_out s) bl - -let insert texfile coq_output result = - let c_tex = open_in texfile in - let c_coq = open_in coq_output in - let c_out = open_out result in - (* next_block k : this function reads the next block of Coq output - * removing the k leading prompts. - * it returns the block as a list of string) *) - let last_read = ref "" in - let next_block k = - if !last_read = "" then last_read := input_line c_coq; - (* skip k prompts *) - for i = 1 to k do - last_read := remove_prompt !last_read; - done; - (* read and return the following lines until a prompt is found *) - let rec read_lines () = - let s = input_line c_coq in - if Str.string_match any_prompt s 0 then begin - last_read := s; [] - end else - s :: (read_lines ()) - in - let first = !last_read in first :: (read_lines ()) - in - (* we are just after \end{coq_...} block *) - let rec just_after () = - let s = input_line c_tex in - if Str.string_match begin_coq_example s 0 then begin - inside (Str.matched_group 1 s <> "example*") - (Str.matched_group 1 s <> "example#") 0 false - end - else begin - if !hrule then output_string c_out "\\hrulefill\\\\\n"; - output_string c_out "\\end{flushleft}\n"; - if !small then output_string c_out "\\end{small}\n"; - if Str.string_match begin_coq_eval s 0 then - eval 0 - else begin - output_string c_out (s ^ "\n"); - outside () - end - end - (* we are outside of a \begin{coq_...} ... \end{coq_...} block *) - and outside () = - let s = input_line c_tex in - if Str.string_match begin_coq_example s 0 then begin - if !small then output_string c_out "\\begin{small}\n"; - output_string c_out "\\begin{flushleft}\n"; - if !hrule then output_string c_out "\\hrulefill\\\\\n"; - inside (Str.matched_group 1 s <> "example*") - (Str.matched_group 1 s <> "example#") 0 true - end else if Str.string_match begin_coq_eval s 0 then - eval 0 - else begin - output_string c_out (s ^ "\n"); - outside () - end - (* we are inside a \begin{coq_example?} ... \end{coq_example?} block - * show_answers tells what kind of block it is - * k is the number of lines read until now *) - and inside show_answers show_questions k first_block = - let s = input_line c_tex in - 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); - if has_match dot_end_line s then begin - let bl = next_block (succ k) in - if !verbose then List.iter print_endline bl; - if show_answers then print_block c_out bl; - inside show_answers show_questions 0 false - end else - inside show_answers show_questions (succ k) first_block - end - (* we are inside a \begin{coq_eval} ... \end{coq_eval} block - * k is the number of lines read until now *) - and eval k = - let s = input_line c_tex in - if Str.string_match end_coq_eval s 0 then - outside () - else begin - if !verbose then Printf.printf "Coq < %s\n" s; - if has_match dot_end_line s then - let bl = next_block (succ k) in - if !verbose then List.iter print_endline bl; - eval 0 - else - eval (succ k) - end - in - try - let _ = next_block 0 in (* to skip the Coq banner *) - let _ = next_block 0 in (* to skip the Coq answer to Set Printing Width *) - outside () - with End_of_file -> begin - close_in c_tex; - close_in c_coq; - close_out c_out - end - -(* Process of one TeX file *) - -let rm f = try Sys.remove f with _ -> () - -let one_file texfile = - let inputv = Filename.temp_file "coq_tex" ".v" in - let coq_output = Filename.temp_file "coq_tex" ".coq_output"in - let result = - if !output_specified then - !output - else if Filename.check_suffix texfile ".tex" then - (Filename.chop_suffix texfile ".tex") ^ ".v.tex" - else - texfile ^ ".v.tex" - in - try - (* 1. extract Coq phrases *) - extract texfile inputv; - (* 2. run Coq on input *) - let _ = Sys.command (Printf.sprintf "%s < %s > %s 2>&1" !image inputv - coq_output) - in - (* 3. insert Coq output into original file *) - insert texfile coq_output result; - (* 4. clean up *) - rm inputv; rm coq_output - with e -> begin - rm inputv; rm coq_output; - raise e - end - -(* Parsing of the command line, check of the Coq command and process - * of all the files in the command line, one by one *) - -let files = ref [] - -let parse_cl () = - Arg.parse - [ "-o", Arg.String (fun s -> output_specified := true; output := s), - "output-file Specifiy the resulting LaTeX file"; - "-n", Arg.Int (fun n -> linelen := n), - "line-width Set the line width"; - "-image", Arg.String (fun s -> image := s), - "coq-image Use coq-image as Coq command"; - "-w", Arg.Set cut_at_blanks, - " Try to cut lines at blanks"; - "-v", Arg.Set verbose, - " Verbose mode (show Coq answers on stdout)"; - "-sl", Arg.Set slanted, - " Coq answers in slanted font (only with LaTeX2e)"; - "-hrule", Arg.Set hrule, - " Coq parts are written between 2 horizontal lines"; - "-small", Arg.Set small, - " Coq parts are written in small font" - ] - (fun s -> files := s :: !files) - "coq-tex [options] file ..." - -let main () = - parse_cl (); - if !image = "" then begin - Printf.printf "Warning: preprocessing with default image \"coqtop\"\n"; - image := "coqtop" - end; - if Sys.command (!image ^ " -batch > /dev/null 2>&1") <> 0 then begin - Printf.printf "Error: "; - let _ = Sys.command (!image ^ " -batch") in - exit 1 - end else begin - Printf.printf "Your version of coqtop seems OK\n"; - flush stdout - end; - List.iter one_file (List.rev !files) - -let _ = Printexc.catch main () |