From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:07:52 +0200 Subject: Imported Upstream version 8.4~gamma0+really8.4beta2 --- tools/coq_makefile.ml | 26 ++++++++++++++------------ tools/coqdoc/cpretty.mll | 20 ++++++++++++++------ tools/coqdoc/index.ml | 6 +++--- tools/coqdoc/output.ml | 8 ++++---- tools/win32hack.mllib | 1 + tools/win32hack_filename.ml | 4 ++++ 6 files changed, 40 insertions(+), 25 deletions(-) create mode 100644 tools/win32hack.mllib create mode 100644 tools/win32hack_filename.ml (limited to 'tools') diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index a685d6ea..20117ca6 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -315,10 +315,10 @@ in print "%.vo %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n"; print "%.g: %.v\n\t$(GALLINA) $<\n\n"; - print "%.tex: %.v\n\t$(COQDOC) -latex $< -o $@\n\n"; - print "%.html: %.v %.glob\n\t$(COQDOC) -html $< -o $@\n\n"; - print "%.g.tex: %.v\n\t$(COQDOC) -latex -g $< -o $@\n\n"; - print "%.g.html: %.v %.glob\n\t$(COQDOC) -html -g $< -o $@\n\n"; + print "%.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@\n\n"; + print "%.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html $< -o $@\n\n"; + print "%.g.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@\n\n"; + print "%.g.html: %.v %.glob\n\t$(COQDOC)$(COQDOCFLAGS) -html -g $< -o $@\n\n"; print "%.v.d: %.v\n"; print "\t$(COQDEP) -slash $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; print "%.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*\n\n" @@ -349,11 +349,13 @@ let variables is_install opt (args,defs) = print "\n"; end; (* Coq executables and relative variables *) + if !some_vfile || !some_mlpackfile || !some_mllibfile then + print "COQDEP?=$(COQBIN)coqdep -c\n"; if !some_vfile then begin print "COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n"; print "COQCHKFLAGS?=-silent -o\n"; + print "COQDOCFLAGS?=-interpolate -utf8\n"; print "COQC?=$(COQBIN)coqc\n"; - print "COQDEP?=$(COQBIN)coqdep -c\n"; print "GALLINA?=$(COQBIN)gallina\n"; print "COQDOC?=$(COQBIN)coqdoc\n"; print "COQCHK?=$(COQBIN)coqchk\n\n"; @@ -374,7 +376,7 @@ let variables is_install opt (args,defs) = print "CAMLOPTLINK?=$(OCAMLOPT) -rectypes\n"; print "GRAMMARS?=grammar.cma\n"; print "CAMLP4EXTEND?=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n"; - print "CAMLP4OPTIONS?=\n"; + print "CAMLP4OPTIONS?=-loc loc\n"; print "PP?=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n\n"; end; match is_install with @@ -564,18 +566,18 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other print "gallina: $(GFILES)\n\n"; print "html: $(GLOBFILES) $(VFILES)\n"; print "\t- mkdir -p html\n"; - print "\t$(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES)\n\n"; + print "\t$(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)\n\n"; print "gallinahtml: $(GLOBFILES) $(VFILES)\n"; print "\t- mkdir -p html\n"; - print "\t$(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES)\n\n"; + print "\t$(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)\n\n"; print "all.ps: $(VFILES)\n"; - print "\t$(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n"; + print "\t$(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n"; print "all-gal.ps: $(VFILES)\n"; - print "\t$(COQDOC) -toc -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n"; + print "\t$(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n"; print "all.pdf: $(VFILES)\n"; - print "\t$(COQDOC) -toc -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n"; + print "\t$(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n"; print "all-gal.pdf: $(VFILES)\n"; - print "\t$(COQDOC) -toc -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n"; + print "\t$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n"; print "validate: $(VOFILES)\n"; print "\t$(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))\n\n"; print "beautify: $(VFILES:=.beautified)\n"; diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 89047e83..925f5258 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -306,7 +306,12 @@ let thm_token = let prf_token = "Next" space+ "Obligation" - | "Proof" (space* "." | space+ "with") + | "Proof" (space* "." | space+ "with" | space+ "using") + +let immediate_prf_token = + (* Approximation of a proof term, if not in the prf_token case *) + (* To be checked after prf_token *) + "Proof" space* [^ '.' 'w' 'u'] let def_token = "Definition" @@ -382,7 +387,8 @@ let commands = | ("Hypothesis" | "Hypotheses") | "End" -let end_kw = "Qed" | "Defined" | "Save" | "Admitted" | "Abort" +let end_kw = + immediate_prf_token | "Qed" | "Defined" | "Save" | "Admitted" | "Abort" let extraction = "Extraction" @@ -504,7 +510,7 @@ rule coq_bol = parse output_indented_keyword s lexbuf; let eol= body lexbuf in if eol then coq_bol lexbuf else coq lexbuf } - | space* notation_kw space* + | space* notation_kw { let s = lexeme lexbuf in output_indented_keyword s lexbuf; let eol= start_notation_string lexbuf in @@ -605,7 +611,7 @@ and coq = parse | prf_token { let eol = if not !Cdglobals.gallina then - begin backtrack lexbuf; body_bol lexbuf end + begin backtrack lexbuf; body lexbuf end else let s = lexeme lexbuf in let eol = @@ -631,7 +637,7 @@ and coq = parse Output.ident s (lexeme_start lexbuf); let eol = body lexbuf in if eol then coq_bol lexbuf else coq lexbuf } - | notation_kw space* + | notation_kw { let s = lexeme lexbuf in Output.ident s (lexeme_start lexbuf); let eol= start_notation_string lexbuf in @@ -1096,7 +1102,7 @@ and body = parse if eol then begin if not !Cdglobals.parse_comments then Output.line_break(); body_bol lexbuf end else body lexbuf } - | "where" space* + | "where" { Tokens.flush_sublexer(); Output.ident (lexeme lexbuf) (lexeme_start lexbuf); start_notation_string lexbuf } @@ -1120,6 +1126,8 @@ and body = parse body lexbuf } and start_notation_string = parse + | space { Tokens.flush_sublexer(); Output.char (lexeme_char lexbuf 0); + start_notation_string lexbuf } | '"' (* a true notation *) { Output.sublexer '"' (lexeme_start lexbuf); notation_string lexbuf; diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index c8e7770a..f19433e9 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -62,7 +62,7 @@ let add_def loc1 loc2 ty sp id = for loc = loc1 to loc2 do Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty)) done; - Hashtbl.add deftable id (Ref (!current_library, full_ident sp id, ty)) + Hashtbl.add deftable id (Def (full_ident sp id, ty)) let add_ref m loc m' sp id ty = if Hashtbl.mem reftable (m, loc) then () @@ -289,11 +289,11 @@ 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 + let classify m e = match e with | Def (s,t) -> add_g s m t; add_bt t s m | Ref _ | Mod _ -> () in - Hashtbl.iter classify reftable; + Hashtbl.iter classify deftable; Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules; { idx_name = "global"; idx_entries = sort_entries !gl; diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index e3d5741a..3aed28b4 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -29,14 +29,14 @@ let build_table l = let is_keyword = build_table - [ "AddPath"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "CoFixpoint"; + [ "About"; "AddPath"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "Compute"; "CoFixpoint"; "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example"; - "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint"; + "Export"; "Fact"; "Fix"; "Fixpoint"; "Function"; "Generalizable"; "Global"; "Grammar"; "Goal"; "Hint"; "Hypothesis"; "Hypotheses"; "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive"; "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; "Module"; "Module Type"; "Declare Module"; "Include"; - "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Proof with"; "Qed"; + "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "Proof"; "Proof with"; "Qed"; "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context"; @@ -44,7 +44,7 @@ let is_keyword = "Delimit"; "Bind"; "Open"; "Scope"; "Inline"; "Implicit Arguments"; "Add"; "Strict"; "Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation"; - "subgoal"; + "subgoal"; "vm_compute"; "Opaque"; "Transparent"; (* Program *) "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma"; diff --git a/tools/win32hack.mllib b/tools/win32hack.mllib new file mode 100644 index 00000000..42395f65 --- /dev/null +++ b/tools/win32hack.mllib @@ -0,0 +1 @@ +Win32hack_filename \ No newline at end of file diff --git a/tools/win32hack_filename.ml b/tools/win32hack_filename.ml new file mode 100644 index 00000000..74f70686 --- /dev/null +++ b/tools/win32hack_filename.ml @@ -0,0 +1,4 @@ +(* The mingw32-ocaml cross-compiler currently uses Filename.dir_sep="/". + Let's tweak that... *) + +let _ = Filename.dir_sep.[0] <- '\\' -- cgit v1.2.3