Imported Upstream snapshot 8.3~beta0+13298

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 ()