diff options
author | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-22 12:55:46 +0200 |
---|---|---|
committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-27 21:42:01 +0200 |
commit | b20d52da0d040fe37bb75b0b739ad7686f9af127 (patch) | |
tree | 6d8612f3a528dab9dd44add1ba26323fd8a41ce7 | |
parent | 4e84e83911c1cf7613a35b921b1e68e097f84b5a (diff) |
Warning 29: non escaped end of line may be non portable
-rw-r--r-- | ide/coqide_ui.ml | 284 | ||||
-rw-r--r-- | ide/ide_slave.ml | 4 | ||||
-rw-r--r-- | interp/constrintern.ml | 6 | ||||
-rw-r--r-- | tools/coq_makefile.ml | 116 | ||||
-rw-r--r-- | toplevel/usage.ml | 2 |
5 files changed, 206 insertions, 206 deletions
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index 2ae18593a..91c281c8d 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -28,148 +28,148 @@ let list_queries menu li = res_buf let init () = - let theui = Printf.sprintf "<ui> -<menubar name='CoqIde MenuBar'> - <menu action='File'> - <menuitem action='New' /> - <menuitem action='Open' /> - <menuitem action='Save' /> - <menuitem action='Save as' /> - <menuitem action='Save all' /> - <menuitem action='Revert all buffers' /> - <menuitem action='Close buffer' /> - <menuitem action='Print...' /> - <menu action='Export to'> - <menuitem action='Html' /> - <menuitem action='Latex' /> - <menuitem action='Dvi' /> - <menuitem action='Pdf' /> - <menuitem action='Ps' /> - </menu> - <menuitem action='Rehighlight' /> - %s - </menu> - <menu name='Edit' action='Edit'> - <menuitem action='Undo' /> - <menuitem action='Redo' /> - <separator /> - <menuitem action='Cut' /> - <menuitem action='Copy' /> - <menuitem action='Paste' /> - <separator /> - <menuitem action='Find' /> - <menuitem action='Find Next' /> - <menuitem action='Find Previous' /> - <menuitem action='Complete Word' /> - <separator /> - <menuitem action='External editor' /> - <separator /> - <menuitem name='Prefs' action='Preferences' /> - </menu> - <menu name='View' action='View'> - <menuitem action='Previous tab' /> - <menuitem action='Next tab' /> - <separator/> - <menuitem action='Zoom in' /> - <menuitem action='Zoom out' /> - <menuitem action='Zoom fit' /> - <separator/> - <menuitem action='Show Toolbar' /> - <menuitem action='Query Pane' /> - <separator/> - <menuitem action='Display implicit arguments' /> - <menuitem action='Display coercions' /> - <menuitem action='Display raw matching expressions' /> - <menuitem action='Display notations' /> - <menuitem action='Display all basic low-level contents' /> - <menuitem action='Display existential variable instances' /> - <menuitem action='Display universe levels' /> - <menuitem action='Display all low-level contents' /> - </menu> - <menu action='Navigation'> - <menuitem action='Forward' /> - <menuitem action='Backward' /> - <menuitem action='Go to' /> - <menuitem action='Start' /> - <menuitem action='End' /> - <menuitem action='Interrupt' /> - <menuitem action='Previous' /> - <menuitem action='Next' /> - </menu> - <menu action='Try Tactics'> - <menuitem action='auto' /> - <menuitem action='auto with *' /> - <menuitem action='eauto' /> - <menuitem action='eauto with *' /> - <menuitem action='intuition' /> - <menuitem action='omega' /> - <menuitem action='simpl' /> - <menuitem action='tauto' /> - <menuitem action='trivial' /> - <menuitem action='Wizard' /> - <separator /> - %s - </menu> - <menu action='Templates'> - <menuitem action='Lemma' /> - <menuitem action='Theorem' /> - <menuitem action='Definition' /> - <menuitem action='Inductive' /> - <menuitem action='Fixpoint' /> - <menuitem action='Scheme' /> - <menuitem action='match' /> - <separator /> - %s - </menu> - <menu action='Queries'> - <menuitem action='Search' /> - <menuitem action='Check' /> - <menuitem action='Print' /> - <menuitem action='About' /> - <menuitem action='Locate' /> - <menuitem action='Print Assumptions' /> - <separator /> - %s - </menu> - <menu name='Tools' action='Tools'> - <menuitem action='Comment' /> - <menuitem action='Uncomment' /> - <separator /> - <menuitem action='Coqtop arguments' /> - </menu> - <menu action='Compile'> - <menuitem action='Compile buffer' /> - <menuitem action='Make' /> - <menuitem action='Next error' /> - <menuitem action='Make makefile' /> - </menu> - <menu action='Windows'> - <menuitem action='Detach View' /> - </menu> - <menu name='Help' action='Help'> - <menuitem action='Browse Coq Manual' /> - <menuitem action='Browse Coq Library' /> - <menuitem action='Help for keyword' /> - <menuitem action='Help for μPG mode' /> - <separator /> - <menuitem name='Abt' action='About Coq' /> - </menu> -</menubar> -<toolbar name='CoqIde ToolBar'> - <toolitem action='Save' /> - <toolitem action='Close buffer' /> - <toolitem action='Forward' /> - <toolitem action='Backward' /> - <toolitem action='Go to' /> - <toolitem action='Start' /> - <toolitem action='End' /> - <toolitem action='Force' /> - <toolitem action='Interrupt' /> - <toolitem action='Previous' /> - <toolitem action='Next' /> - <toolitem action='Wizard' /> -</toolbar> -</ui>" + let theui = Printf.sprintf "<ui>\ +\n<menubar name='CoqIde MenuBar'>\ +\n <menu action='File'>\ +\n <menuitem action='New' />\ +\n <menuitem action='Open' />\ +\n <menuitem action='Save' />\ +\n <menuitem action='Save as' />\ +\n <menuitem action='Save all' />\ +\n <menuitem action='Revert all buffers' />\ +\n <menuitem action='Close buffer' />\ +\n <menuitem action='Print...' />\ +\n <menu action='Export to'>\ +\n <menuitem action='Html' />\ +\n <menuitem action='Latex' />\ +\n <menuitem action='Dvi' />\ +\n <menuitem action='Pdf' />\ +\n <menuitem action='Ps' />\ +\n </menu>\ +\n <menuitem action='Rehighlight' />\ +\n %s\ +\n </menu>\ +\n <menu name='Edit' action='Edit'>\ +\n <menuitem action='Undo' />\ +\n <menuitem action='Redo' />\ +\n <separator />\ +\n <menuitem action='Cut' />\ +\n <menuitem action='Copy' />\ +\n <menuitem action='Paste' />\ +\n <separator />\ +\n <menuitem action='Find' />\ +\n <menuitem action='Find Next' />\ +\n <menuitem action='Find Previous' />\ +\n <menuitem action='Complete Word' />\ +\n <separator />\ +\n <menuitem action='External editor' />\ +\n <separator />\ +\n <menuitem name='Prefs' action='Preferences' />\ +\n </menu>\ +\n <menu name='View' action='View'>\ +\n <menuitem action='Previous tab' />\ +\n <menuitem action='Next tab' />\ +\n <separator/>\ +\n <menuitem action='Zoom in' />\ +\n <menuitem action='Zoom out' />\ +\n <menuitem action='Zoom fit' />\ +\n <separator/>\ +\n <menuitem action='Show Toolbar' />\ +\n <menuitem action='Query Pane' />\ +\n <separator/>\ +\n <menuitem action='Display implicit arguments' />\ +\n <menuitem action='Display coercions' />\ +\n <menuitem action='Display raw matching expressions' />\ +\n <menuitem action='Display notations' />\ +\n <menuitem action='Display all basic low-level contents' />\ +\n <menuitem action='Display existential variable instances' />\ +\n <menuitem action='Display universe levels' />\ +\n <menuitem action='Display all low-level contents' />\ +\n </menu>\ +\n <menu action='Navigation'>\ +\n <menuitem action='Forward' />\ +\n <menuitem action='Backward' />\ +\n <menuitem action='Go to' />\ +\n <menuitem action='Start' />\ +\n <menuitem action='End' />\ +\n <menuitem action='Interrupt' />\ +\n <menuitem action='Previous' />\ +\n <menuitem action='Next' />\ +\n </menu>\ +\n <menu action='Try Tactics'>\ +\n <menuitem action='auto' />\ +\n <menuitem action='auto with *' />\ +\n <menuitem action='eauto' />\ +\n <menuitem action='eauto with *' />\ +\n <menuitem action='intuition' />\ +\n <menuitem action='omega' />\ +\n <menuitem action='simpl' />\ +\n <menuitem action='tauto' />\ +\n <menuitem action='trivial' />\ +\n <menuitem action='Wizard' />\ +\n <separator />\ +\n %s\ +\n </menu>\ +\n <menu action='Templates'>\ +\n <menuitem action='Lemma' />\ +\n <menuitem action='Theorem' />\ +\n <menuitem action='Definition' />\ +\n <menuitem action='Inductive' />\ +\n <menuitem action='Fixpoint' />\ +\n <menuitem action='Scheme' />\ +\n <menuitem action='match' />\ +\n <separator />\ +\n %s\ +\n </menu>\ +\n <menu action='Queries'>\ +\n <menuitem action='Search' />\ +\n <menuitem action='Check' />\ +\n <menuitem action='Print' />\ +\n <menuitem action='About' />\ +\n <menuitem action='Locate' />\ +\n <menuitem action='Print Assumptions' />\ +\n <separator />\ +\n %s\ +\n </menu>\ +\n <menu name='Tools' action='Tools'>\ +\n <menuitem action='Comment' />\ +\n <menuitem action='Uncomment' />\ +\n <separator />\ +\n <menuitem action='Coqtop arguments' />\ +\n </menu>\ +\n <menu action='Compile'>\ +\n <menuitem action='Compile buffer' />\ +\n <menuitem action='Make' />\ +\n <menuitem action='Next error' />\ +\n <menuitem action='Make makefile' />\ +\n </menu>\ +\n <menu action='Windows'>\ +\n <menuitem action='Detach View' />\ +\n </menu>\ +\n <menu name='Help' action='Help'>\ +\n <menuitem action='Browse Coq Manual' />\ +\n <menuitem action='Browse Coq Library' />\ +\n <menuitem action='Help for keyword' />\ +\n <menuitem action='Help for μPG mode' />\ +\n <separator />\ +\n <menuitem name='Abt' action='About Coq' />\ +\n </menu>\ +\n</menubar>\ +\n<toolbar name='CoqIde ToolBar'>\ +\n <toolitem action='Save' />\ +\n <toolitem action='Close buffer' />\ +\n <toolitem action='Forward' />\ +\n <toolitem action='Backward' />\ +\n <toolitem action='Go to' />\ +\n <toolitem action='Start' />\ +\n <toolitem action='End' />\ +\n <toolitem action='Force' />\ +\n <toolitem action='Interrupt' />\ +\n <toolitem action='Previous' />\ +\n <toolitem action='Next' />\ +\n <toolitem action='Wizard' />\ +\n</toolbar>\ +\n</ui>" (if Coq_config.gtk_platform <> `QUARTZ then "<menuitem action='Quit' />" else "") (Buffer.contents (list_items "Tactic" Coq_commands.tactics)) (Buffer.contents (list_items "Template" Coq_commands.commands)) diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index ca0ef38d3..dbfe4256b 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -512,5 +512,5 @@ let () = Coqtop.toploop_init := (fun args -> let () = Coqtop.toploop_run := loop let () = Usage.add_to_usage "coqidetop" -" --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format - --help-XML-protocol print the documentation of the XML protocol used by CoqIDE\n" +" --xml_format=Ppcmds serialize pretty printing messages using the std_ppcmds format\ +\n --help-XML-protocol print the documentation of the XML protocol used by CoqIDE\n" diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 389880c5c..3f99a3c7c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -855,9 +855,9 @@ let intern_qualid loc qid intern env lvar us args = | Some _, GApp (loc, GRef (loc', ref, None), arg) -> GApp (loc, GRef (loc', ref, us), arg) | Some _, _ -> - user_err ~loc (str "Notation " ++ pr_qualid qid ++ - str " cannot have a universe instance, its expanded head - does not start with a reference") + user_err ~loc (str "Notation " ++ pr_qualid qid + ++ str " cannot have a universe instance," + ++ str " its expanded head does not start with a reference") in c, projapp, args2 diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index ed89bda2c..4875cb62b 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -56,48 +56,48 @@ let lib_dirs = let usage () = - output_string stderr "Usage summary: - -coq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}] - ... [any] ... [-extra[-phony] result dependencies command] - ... [-I dir] ... [-R physicalpath logicalpath] - ... [-Q physicalpath logicalpath] ... [VARIABLE = value] - ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file] - [-h] [--help] - -[file.v]: Coq file to be compiled -[file.ml[i4]?]: Objective Caml file to be compiled -[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml - library/module -[any] : subdirectory that should be \"made\" and has a Makefile itself - to do so. Very fragile and discouraged. -[-extra result dependencies command]: add target \"result\" with command - \"command\" and dependencies \"dependencies\". If \"result\" is not - generic (do not contains a %), \"result\" is built by _make all_ and - deleted by _make clean_. -[-extra-phony result dependencies command]: add a PHONY target \"result\" - with command \"command\" and dependencies \"dependencies\". Note that - _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as - as a dependencies of an already defined target \"foo\". -[-I dir]: look for Objective Caml dependencies in \"dir\" -[-R physicalpath logicalpath]: look for Coq dependencies resursively - starting from \"physicalpath\". The logical path associated to the - physical path is \"logicalpath\". -[-Q physicalpath logicalpath]: look for Coq dependencies starting from - \"physicalpath\". The logical path associated to the physical path - is \"logicalpath\". -[VARIABLE = value]: Add the variable definition \"VARIABLE=value\" -[-byte]: compile with byte-code version of coq -[-opt]: compile with native-code version of coq -[-arg opt]: send option \"opt\" to coqc -[-install opt]: where opt is \"user\" to force install into user directory, - \"none\" to build a makefile with no install target or - \"global\" to force install in $COQLIB directory -[-f file]: take the contents of file as arguments -[-o file]: output should go in file file - Output file outside the current directory is forbidden. -[-h]: print this usage summary -[--help]: equivalent to [-h]\n"; + output_string stderr "Usage summary:\ +\n\ +\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\ +\n ... [any] ... [-extra[-phony] result dependencies command]\ +\n ... [-I dir] ... [-R physicalpath logicalpath]\ +\n ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\ +\n ... [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\ +\n [-h] [--help]\ +\n\ +\n[file.v]: Coq file to be compiled\ +\n[file.ml[i4]?]: Objective Caml file to be compiled\ +\n[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml\ +\n library/module\ +\n[any] : subdirectory that should be \"made\" and has a Makefile itself\ +\n to do so. Very fragile and discouraged.\ +\n[-extra result dependencies command]: add target \"result\" with command\ +\n \"command\" and dependencies \"dependencies\". If \"result\" is not\ +\n generic (do not contains a %), \"result\" is built by _make all_ and\ +\n deleted by _make clean_.\ +\n[-extra-phony result dependencies command]: add a PHONY target \"result\"\ +\n with command \"command\" and dependencies \"dependencies\". Note that\ +\n _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as\ +\n as a dependencies of an already defined target \"foo\".\ +\n[-I dir]: look for Objective Caml dependencies in \"dir\"\ +\n[-R physicalpath logicalpath]: look for Coq dependencies resursively\ +\n starting from \"physicalpath\". The logical path associated to the\ +\n physical path is \"logicalpath\".\ +\n[-Q physicalpath logicalpath]: look for Coq dependencies starting from\ +\n \"physicalpath\". The logical path associated to the physical path\ +\n is \"logicalpath\".\ +\n[VARIABLE = value]: Add the variable definition \"VARIABLE=value\"\ +\n[-byte]: compile with byte-code version of coq\ +\n[-opt]: compile with native-code version of coq\ +\n[-arg opt]: send option \"opt\" to coqc\ +\n[-install opt]: where opt is \"user\" to force install into user directory,\ +\n \"none\" to build a makefile with no install target or\ +\n \"global\" to force install in $COQLIB directory\ +\n[-f file]: take the contents of file as arguments\ +\n[-o file]: output should go in file file\ +\n Output file outside the current directory is forbidden.\ +\n[-h]: print this usage summary\ +\n[--help]: equivalent to [-h]\n"; exit 1 let is_genrule r = (* generic rule (like bar%foo: ...) *) @@ -264,8 +264,8 @@ let where_put_doc = function then physical_dir_of_logical_dir pr else - let () = prerr_string "Warning: -Q options don't have a correct common prefix, - install-doc will put anything in $INSTALLDEFAULTROOT\n" in + let () = prerr_string ("Warning: -Q options don't have a correct common prefix," + ^ " install-doc will put anything in $INSTALLDEFAULTROOT\n") in "$(INSTALLDEFAULTROOT)" |_,inc_i,((_,lp,_)::q as inc_r) -> let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) lp q in @@ -277,8 +277,8 @@ let where_put_doc = function then physical_dir_of_logical_dir pr else - let () = prerr_string "Warning: -R/-Q options don't have a correct common prefix, - install-doc will put anything in $INSTALLDEFAULTROOT\n" in + let () = prerr_string ("Warning: -R/-Q options don't have a correct common prefix," + ^ " install-doc will put anything in $INSTALLDEFAULTROOT\n") in "$(INSTALLDEFAULTROOT)" let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function @@ -518,8 +518,8 @@ let variables is_install opt (args,defs) = if !some_ml4file || !some_mlfile || !some_mlifile then begin print "COQSRCLIBS?=" ; List.iter (fun c -> print "-I \"$(COQLIB)"; print c ; print "\" \\\n") lib_dirs ; - List.iter (fun c -> print " \\ - -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n"; + List.iter (fun c -> print " \\\ +\n -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n"; print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n"; print "CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread -safe-string\n"; print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread -safe-string\n"; @@ -529,8 +529,8 @@ let variables is_install opt (args,defs) = print "CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)\n"; print "GRAMMARS?=grammar.cma\n"; print "CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo\n"; - print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \\ - $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n"; + print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \\\ +\n $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n"; end; match is_install with | Project_file.NoInstall -> () @@ -816,14 +816,14 @@ let all_target (vfiles, (_,_,_,_,mlpackfiles as mlfiles), sps, sds) inc = let banner () = print (Printf.sprintf -"############################################################################# -## v # The Coq Proof Assistant ## -## <O___,, # INRIA - CNRS - LIX - LRI - PPS ## -## \\VV/ # ## -## // # Makefile automagically generated by coq_makefile V%s ## -############################################################################# - -" (Coq_config.version ^ String.make (10 - String.length Coq_config.version) ' ')) +"#############################################################################\ +\n## v # The Coq Proof Assistant ##\ +\n## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##\ +\n## \\VV/ # ##\ +\n## // # Makefile automagically generated by coq_makefile V%s ##\ +\n#############################################################################\ +\n\n" +(Coq_config.version ^ String.make (10 - String.length Coq_config.version) ' ')) let warning () = print "# WARNING\n#\n"; diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 66f782ffb..e457ca61d 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -83,7 +83,7 @@ let print_usage_channel co command = \n -m, --memory display total heap size at program exit\ \n (use environment variable\ \n OCAML_GC_STATS=\"/tmp/gclog.txt\"\ -\n for full Gc stats dump) +\n for full Gc stats dump)\ \n -native-compiler precompile files for the native_compute machinery\ \n -h, -help, --help print this list of options\ \n"; |