From bf12eb93f3f6a6a824a10878878fadd59745aae0 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 29 Dec 2012 10:57:43 +0100 Subject: Imported Upstream version 8.4pl1dfsg --- tools/coq_makefile.ml | 16 ++- tools/coq_tex.ml | 295 +++++++++++++++++++++++++++++++++++++++++++++++++ tools/coq_tex.ml4 | 290 ------------------------------------------------ tools/coqdep_common.ml | 6 +- tools/coqdoc/index.ml | 34 +++--- tools/coqdoc/index.mli | 3 +- tools/coqdoc/output.ml | 53 +++------ tools/fake_ide.ml | 2 +- 8 files changed, 346 insertions(+), 353 deletions(-) create mode 100644 tools/coq_tex.ml delete mode 100644 tools/coq_tex.ml4 (limited to 'tools') diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index eedbf422..6f0071a4 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -222,7 +222,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in print "\n"; end; print "install:"; - if (not_empty cmxsfiles) then print "$(if ifeq '$(HASNATDYNLINK)' 'true',install-natdynlink)"; + if (not_empty cmxsfiles) then print "$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink)"; print "\n"; if not_empty vfiles then install_include_by_root "VOFILES" vfiles inc; if (not_empty cmofiles) then @@ -291,18 +291,18 @@ let implicit () = print "%.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; print "%.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; print "%.ml4.d: %.ml4\n"; - print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "\t$(COQDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in let ml_rules () = print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; print "%.ml.d: %.ml\n"; print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in let cmxs_rules () = + print "%.cmxs: %.cmxa\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n"; print "%.cmxs: %.cmx\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n" in let mllib_rules () = print "%.cma: | %.mllib\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; print "%.cmxa: | %.mllib\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; - print "%.cmxs: %.cmxa\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n"; print "%.mllib.d: %.mllib\n"; print "\t$(COQDEP) -slash $(COQLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in let mlpack_rules () = @@ -411,7 +411,7 @@ let parameters () = print "# DSTROOT to specify a prefix to install path.\n\n"; print "# Here is a hack to make $(eval $(shell works:\n"; print "define donewline\n\n\nendef\n"; - print "includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr '\\n' '@'; })))\n"; + print "includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\\r' | tr '\\n' '@'; })))\n"; print "$(call includecmdwithout@,$(COQBIN)coqtop -config)\n\n" let include_dirs (inc_i,inc_r) = @@ -543,14 +543,18 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other print "CMXSFILES=$(CMXFILES:.cmx=.cmxs) $(CMXAFILES:.cmxa=.cmxs)\n"; classify_files_by_root "CMXSFILES" (l1@l2) inc; end; - print "\n"; + print "ifeq '$(HASNATDYNLINK)' 'true'\n"; + print "HASNATDYNLINK_OR_EMPTY := yes\n"; + print "else\n"; + print "HASNATDYNLINK_OR_EMPTY :=\n"; + print "endif\n\n"; section "Definition of the toplevel targets."; print "all: "; if !some_vfile then print "$(VOFILES) "; if !some_mlfile || !some_ml4file || !some_mlpackfile then print "$(CMOFILES) "; if !some_mllibfile then print "$(CMAFILES) "; if !some_mlfile || !some_ml4file || !some_mllibfile || !some_mlpackfile - then print "$(if ifeq '$(HASNATDYNLINK)' 'true',$(CMXSFILES)) "; + then print "$(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES)) "; print_list "\\\n " other_targets; print "\n\n"; if !some_mlifile then begin diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml new file mode 100644 index 00000000..350b59aa --- /dev/null +++ b/tools/coq_tex.ml @@ -0,0 +1,295 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + 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 dollar = "\\$" and backslash = "\\\\" and expon = "\\^" in + let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>]") in + let adapt_delim = function + | "_" | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c + | "\\" -> "{\\char'134}" + | "^" -> "{\\char'136}" + | "~" -> "{\\char'176}" + | " " -> "~" + | "<" -> "{<}" + | ">" -> "{>}" + | _ -> assert false + in + let adapt = function + | Str.Text s -> s + | Str.Delim s -> adapt_delim s + in + String.concat "" (List.map adapt (Str.full_split delims 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"; + "-boot", Arg.Set boot, + " Launch coqtop with the -boot option" + ] + (fun s -> files := s :: !files) + "coq-tex [options] file ..." + +let find_coqtop () = + let prog = Sys.executable_name in + try + let size = String.length prog in + let i = Str.search_backward (Str.regexp_string "coq-tex") prog (size-7) in + (String.sub prog 0 i)^"coqtop"^(String.sub prog (i+7) (size-i-7)) + with Not_found -> begin + Printf.printf "Warning: preprocessing with default image \"coqtop\"\n"; + "coqtop" + end + +let main () = + parse_cl (); + if !image = "" then image := Filename.quote (find_coqtop ()); + if !boot then image := !image ^ " -boot"; + if Sys.command (!image ^ " -batch -silent") <> 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 () diff --git a/tools/coq_tex.ml4 b/tools/coq_tex.ml4 deleted file mode 100644 index 1a9b9c73..00000000 --- a/tools/coq_tex.ml4 +++ /dev/null @@ -1,290 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* () - | _ -> 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 () diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index c929e559..4977a94c 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -288,7 +288,7 @@ let canonize f = | (f,_) :: _ -> escape f | _ -> escape f -let traite_fichier_Coq verbose f = +let rec traite_fichier_Coq verbose f = try let chan = open_in f in let buf = Lexing.from_channel chan in @@ -347,7 +347,9 @@ let traite_fichier_Coq verbose f = addQueue deja_vu_v [str]; try let file_str = Hashtbl.find vKnown [str] in - printf " %s.v" (canonize file_str) + let canon = canonize file_str in + printf " %s.v" canon; + traite_fichier_Coq true (canon ^ ".v") with Not_found -> () end | AddLoadPath _ | AddRecLoadPath _ -> (* TODO *) () diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index d319ce72..14447b06 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -35,17 +35,18 @@ type entry_type = type index_entry = | Def of string * entry_type | Ref of coq_module * string * entry_type - | Mod of coq_module * string let current_type : entry_type ref = ref Library let current_library = ref "" (** refers to the file being parsed *) -(** [deftable] stores only definitions and is used to interpolate idents - inside comments, which are not globalized otherwise. *) - +(** [deftable] stores only definitions and is used to build the index *) let deftable = Hashtbl.create 97 +(** [byidtable] is used to interpolate idents inside comments, which are not + globalized otherwise. *) +let byidtable = Hashtbl.create 97 + (** [reftable] stores references and definitions *) let reftable = Hashtbl.create 97 @@ -59,25 +60,25 @@ let full_ident sp id = else "" let add_def loc1 loc2 ty sp id = + let fullid = full_ident sp id in + let def = Def (fullid, ty) in for loc = loc1 to loc2 do - Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty)) + Hashtbl.add reftable (!current_library, loc) def done; - Hashtbl.add deftable id (Def (full_ident sp id, ty)) + Hashtbl.add deftable !current_library (fullid, ty); + Hashtbl.add byidtable id (!current_library, fullid, ty) let add_ref m loc m' sp id ty = + let fullid = full_ident sp id in if Hashtbl.mem reftable (m, loc) then () - else Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty)); + else Hashtbl.add reftable (m, loc) (Ref (m', fullid, ty)); let idx = if id = "<>" then m' else id in - if Hashtbl.mem deftable idx then () - else Hashtbl.add deftable idx (Ref (m', full_ident sp id, ty)) - -let add_mod m loc m' id = - Hashtbl.add reftable (m, loc) (Mod (m', id)); - Hashtbl.add deftable m (Mod (m', id)) + if Hashtbl.mem byidtable idx then () + else Hashtbl.add byidtable idx (m', fullid, ty) let find m l = Hashtbl.find reftable (m, l) -let find_string m s = Hashtbl.find deftable s +let find_string m s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t) (*s Manipulating path prefixes *) @@ -289,10 +290,7 @@ let all_entries () = let l = try Hashtbl.find bt t with Not_found -> [] in Hashtbl.replace bt t ((s,m) :: l) in - let classify m e = match e with - | Def (s,t) -> add_g s m t; add_bt t s m - | Ref _ | Mod _ -> () - in + let classify m (s,t) = (add_g s m t; add_bt t s m) in Hashtbl.iter classify deftable; Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules; { idx_name = "global"; diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index 8c658a90..0f62a086 100644 --- a/tools/coqdoc/index.mli +++ b/tools/coqdoc/index.mli @@ -34,10 +34,11 @@ val type_name : entry_type -> string type index_entry = | Def of string * entry_type | Ref of coq_module * string * entry_type - | Mod of coq_module * string +(* Find what symbol coqtop said is located at loc in the source file *) val find : coq_module -> loc -> index_entry +(* Find what data is referred to by some string in some coq module *) val find_string : coq_module -> string -> index_entry val add_module : coq_module -> unit diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index cd33528a..0dc86bc8 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -126,9 +126,12 @@ let initialize_texmacs () = let token_tree_texmacs = ref (initialize_texmacs ()) +let token_tree_latex = ref Tokens.empty_ttree +let token_tree_html = ref Tokens.empty_ttree + let initialize_tex_html () = let if_utf8 = if !Cdglobals.utf8 then fun x -> Some x else fun _ -> None in - List.fold_right (fun (s,l,l') (tt,tt') -> + let (tree_latex, tree_html) = List.fold_right (fun (s,l,l') (tt,tt') -> (Tokens.ttree_add tt s l, match l' with None -> tt' | Some l' -> Tokens.ttree_add tt' s l')) [ "*" , "\\ensuremath{\\times}", if_utf8 "×"; @@ -151,10 +154,9 @@ let initialize_tex_html () = "Π", "\\ensuremath{\\Pi}", if_utf8 "Π"; "λ", "\\ensuremath{\\lambda}", if_utf8 "λ"; (* "fun", "\\ensuremath{\\lambda}" ? *) - ] (Tokens.empty_ttree,Tokens.empty_ttree) - -let token_tree_latex = ref (fst (initialize_tex_html ())) -let token_tree_html = ref (snd (initialize_tex_html ())) + ] (Tokens.empty_ttree,Tokens.empty_ttree) in + token_tree_latex := tree_latex; + token_tree_html := tree_html let add_printing_token s (t1,t2) = (match t1 with None -> () | Some t1 -> @@ -325,9 +327,6 @@ module Latex = struct let space = 0.5 *. (float n) in printf "\\coqdocindent{%2.2fem}\n" space - let module_ref m s = - printf "\\coqdocmodule{%s}{%s}" m (escaped s) - let ident_ref m fid typ s = let id = if fid <> "" then (m ^ "." ^ fid) else m in match find_module m with @@ -356,12 +355,8 @@ module Latex = struct let reference s = function | Def (fullid,typ) -> defref (get_module false) fullid typ s - | Mod (m,s') when s = s' -> - module_ref m s | Ref (m,fullid,typ) -> ident_ref m fullid typ s - | Mod _ -> - printf "\\coqdocvar{%s}" (escaped s) (*s The sublexer buffers symbol characters and attached uninterpreted ident and try to apply special translation such as, @@ -389,6 +384,7 @@ module Latex = struct last_was_in := false let initialize () = + initialize_tex_html (); Tokens.token_tree := token_tree_latex; Tokens.outfun := output_sublexer_string @@ -534,10 +530,7 @@ module Html = struct end let trailer () = - if !index && (get_module false) <> "Index" then - printf "\n\n
\n
Index" !index_name; - if !header_trailer then - if !footer_file_spec then + if !header_trailer && !footer_file_spec then let cin = Pervasives.open_in !footer_file in try while true do @@ -545,12 +538,14 @@ module Html = struct printf "%s\n" s done with End_of_file -> Pervasives.close_in cin - else - begin - printf "
This page has been generated by "; - printf "coqdoc\n" Coq_config.wwwcoq; - printf "
\n\n\n\n\n" - end + else + begin + if !index && (get_module false) <> "Index" then + printf "\n\n
\n
Index" !index_name; + printf "
This page has been generated by "; + printf "coqdoc\n" Coq_config.wwwcoq; + printf "
\n\n\n\n\n" + end let start_module () = let ln = !lib_name in @@ -620,15 +615,6 @@ module Html = struct | Some n -> n | None -> addr) - let module_ref m s = - match find_module m with - | Local -> - printf "%s" m s - | External m when !externals -> - printf "%s" m s - | External _ | Unknown -> - output_string s - let ident_ref m fid typ s = match find_module m with | Local -> @@ -645,12 +631,8 @@ module Html = struct | Def (fullid,ty) -> printf "" fullid; printf "%s" (type_name ty) s - | Mod (m,s') when s = s' -> - module_ref m s | Ref (m,fullid,ty) -> ident_ref m fullid (type_name ty) s - | Mod _ -> - printf "%s" s let output_sublexer_string doescape issymbchar tag s = let s = if doescape then escaped s else s in @@ -667,6 +649,7 @@ module Html = struct Tokens.output_tagged_symbol_char tag c let initialize () = + initialize_tex_html(); Tokens.token_tree := token_tree_html; Tokens.outfun := output_sublexer_string diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 1e889639..22a36ede 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -21,7 +21,7 @@ let eval_call (call:'a Ide_intf.call) = Xml_utils.print_xml (snd !coqtop) xml_query; flush (snd !coqtop); let xml_answer = Xml_parser.parse p (Xml_parser.SChannel (fst !coqtop)) in - let res = Ide_intf.to_answer xml_answer in + let res = Ide_intf.to_answer xml_answer call in prerr_endline (Ide_intf.pr_full_value call res); match res with Interface.Fail _ -> exit 1 | _ -> () -- cgit v1.2.3