From: Claudio Sacerdoti Coen Date: Fri, 14 Dec 2018 23:15:58 +0000 (+0100) Subject: On-going porting to lablgtk3 X-Git-Tag: make_still_working~229^2~1^2~36 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=f34f2623a3133e235331d0c0c1830ec213dd09f1 On-going porting to lablgtk3 --- diff --git a/matita/.merlin b/matita/.merlin new file mode 100644 index 000000000..92f60a69a --- /dev/null +++ b/matita/.merlin @@ -0,0 +1,9 @@ +S components/* +S matita + +B components/* +B matita + +PKG lablgtk3 helm-content helm-ng_disambiguation helm-content_pres helm-ng_extraction helm-disambiguation helm-ng_kernel helm-extlib helm-ng_library helm-getter helm-ng_paramodulation helm-grafite helm-ng_refiner helm-grafite_engine helm-ng_tactics helm-grafite_parser helm-registry helm-library helm-syntax_extensions helm-logger helm-thread helm-ng_cic_content helm-xml + +FLG -rectypes diff --git a/matita/components/METAS/meta.helm-content_pres.src b/matita/components/METAS/meta.helm-content_pres.src index f9540fa62..0e361298e 100644 --- a/matita/components/METAS/meta.helm-content_pres.src +++ b/matita/components/METAS/meta.helm-content_pres.src @@ -1,4 +1,4 @@ -requires="helm-content helm-syntax_extensions camlp5.gramlib ulex08 helm-grafite" +requires="helm-content helm-syntax_extensions camlp5.gramlib ulex-camlp5 helm-grafite" version="0.0.1" archive(byte)="content_pres.cma" archive(native)="content_pres.cmxa" diff --git a/matita/components/METAS/meta.helm-grafite_parser.src b/matita/components/METAS/meta.helm-grafite_parser.src index 91bfdab4c..c415c72b0 100644 --- a/matita/components/METAS/meta.helm-grafite_parser.src +++ b/matita/components/METAS/meta.helm-grafite_parser.src @@ -1,4 +1,4 @@ -requires="helm-grafite ulex08 helm-ng_disambiguation helm-ng_library helm-content_pres" +requires="helm-grafite ulex-camlp5 helm-ng_disambiguation helm-ng_library helm-content_pres" version="0.0.1" archive(byte)="grafite_parser.cma" archive(native)="grafite_parser.cmxa" diff --git a/matita/components/content/.depend.opt b/matita/components/content/.depend.opt index 9c0b365c6..7bb00ba9b 100644 --- a/matita/components/content/.depend.opt +++ b/matita/components/content/.depend.opt @@ -1,9 +1,14 @@ -content.cmx : content.cmi content.cmi : -notationEnv.cmx : notationUtil.cmx notationPt.cmx notationEnv.cmi +notationUtil.cmi : notationPt.cmx notationEnv.cmi : notationPt.cmx -notationPp.cmx : notationPt.cmx notationEnv.cmx notationPp.cmi notationPp.cmi : notationPt.cmx notationEnv.cmi +notationPt.cmo : notationPt.cmx : +content.cmo : content.cmi +content.cmx : content.cmi +notationUtil.cmo : notationPt.cmx notationUtil.cmi notationUtil.cmx : notationPt.cmx notationUtil.cmi -notationUtil.cmi : notationPt.cmx +notationEnv.cmo : notationUtil.cmi notationPt.cmx notationEnv.cmi +notationEnv.cmx : notationUtil.cmx notationPt.cmx notationEnv.cmi +notationPp.cmo : notationPt.cmx notationEnv.cmi notationPp.cmi +notationPp.cmx : notationPt.cmx notationEnv.cmx notationPp.cmi diff --git a/matita/components/content_pres/.depend.opt b/matita/components/content_pres/.depend.opt index 211b4fc51..4deb6e591 100644 --- a/matita/components/content_pres/.depend.opt +++ b/matita/components/content_pres/.depend.opt @@ -1,24 +1,38 @@ -box.cmx : renderingAttrs.cmx box.cmi +renderingAttrs.cmi : +cicNotationLexer.cmi : +cicNotationParser.cmi : +mpresentation.cmi : box.cmi : -boxPp.cmx : renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \ - boxPp.cmi +content2presMatcher.cmi : +termContentPres.cmi : cicNotationParser.cmi boxPp.cmi : mpresentation.cmi cicNotationPres.cmi box.cmi +cicNotationPres.cmi : mpresentation.cmi box.cmi +content2pres.cmi : termContentPres.cmi cicNotationPres.cmi +renderingAttrs.cmo : renderingAttrs.cmi +renderingAttrs.cmx : renderingAttrs.cmi +cicNotationLexer.cmo : cicNotationLexer.cmi cicNotationLexer.cmx : cicNotationLexer.cmi -cicNotationLexer.cmi : +cicNotationParser.cmo : cicNotationLexer.cmi cicNotationParser.cmi cicNotationParser.cmx : cicNotationLexer.cmx cicNotationParser.cmi -cicNotationParser.cmi : +mpresentation.cmo : mpresentation.cmi +mpresentation.cmx : mpresentation.cmi +box.cmo : renderingAttrs.cmi box.cmi +box.cmx : renderingAttrs.cmx box.cmi +content2presMatcher.cmo : content2presMatcher.cmi +content2presMatcher.cmx : content2presMatcher.cmi +termContentPres.cmo : renderingAttrs.cmi content2presMatcher.cmi \ + cicNotationParser.cmi termContentPres.cmi +termContentPres.cmx : renderingAttrs.cmx content2presMatcher.cmx \ + cicNotationParser.cmx termContentPres.cmi +boxPp.cmo : renderingAttrs.cmi mpresentation.cmi cicNotationPres.cmi box.cmi \ + boxPp.cmi +boxPp.cmx : renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \ + boxPp.cmi +cicNotationPres.cmo : renderingAttrs.cmi mpresentation.cmi box.cmi \ + cicNotationPres.cmi cicNotationPres.cmx : renderingAttrs.cmx mpresentation.cmx box.cmx \ cicNotationPres.cmi -cicNotationPres.cmi : mpresentation.cmi box.cmi +content2pres.cmo : termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \ + cicNotationPres.cmi box.cmi content2pres.cmi content2pres.cmx : termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \ cicNotationPres.cmx box.cmx content2pres.cmi -content2pres.cmi : termContentPres.cmi cicNotationPres.cmi -content2presMatcher.cmx : content2presMatcher.cmi -content2presMatcher.cmi : -mpresentation.cmx : mpresentation.cmi -mpresentation.cmi : -renderingAttrs.cmx : renderingAttrs.cmi -renderingAttrs.cmi : -termContentPres.cmx : renderingAttrs.cmx content2presMatcher.cmx \ - cicNotationParser.cmx termContentPres.cmi -termContentPres.cmi : cicNotationParser.cmi diff --git a/matita/components/content_pres/Makefile b/matita/components/content_pres/Makefile index 655ffbe8f..1f4ede959 100644 --- a/matita/components/content_pres/Makefile +++ b/matita/components/content_pres/Makefile @@ -39,7 +39,7 @@ include ../Makefile.common # soon as we have ocaml 3.09 everywhere and "loc" occurrences are replaced by # "_loc" occurrences UTF8DIR := $(shell $(OCAMLFIND) query helm-syntax_extensions) -ULEXDIR := $(shell $(OCAMLFIND) query ulex08) +ULEXDIR := $(shell $(OCAMLFIND) query ulex-camlp5) MY_SYNTAXOPTIONS = -pp "camlp5o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc" cicNotationLexer.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) cicNotationParser.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) diff --git a/matita/components/disambiguation/.depend.opt b/matita/components/disambiguation/.depend.opt index 1f1711ae7..735bea7f7 100644 --- a/matita/components/disambiguation/.depend.opt +++ b/matita/components/disambiguation/.depend.opt @@ -1,7 +1,11 @@ -disambiguate.cmx : disambiguateTypes.cmx disambiguate.cmi +disambiguateTypes.cmi : disambiguate.cmi : disambiguateTypes.cmi +multiPassDisambiguator.cmi : disambiguateTypes.cmi disambiguate.cmi +disambiguateTypes.cmo : disambiguateTypes.cmi disambiguateTypes.cmx : disambiguateTypes.cmi -disambiguateTypes.cmi : +disambiguate.cmo : disambiguateTypes.cmi disambiguate.cmi +disambiguate.cmx : disambiguateTypes.cmx disambiguate.cmi +multiPassDisambiguator.cmo : disambiguateTypes.cmi disambiguate.cmi \ + multiPassDisambiguator.cmi multiPassDisambiguator.cmx : disambiguateTypes.cmx disambiguate.cmx \ multiPassDisambiguator.cmi -multiPassDisambiguator.cmi : disambiguateTypes.cmi disambiguate.cmi diff --git a/matita/components/extlib/.depend.opt b/matita/components/extlib/.depend.opt index 12de49274..e7b0a3bc7 100644 --- a/matita/components/extlib/.depend.opt +++ b/matita/components/extlib/.depend.opt @@ -1,18 +1,27 @@ -componentsConf.cmx : componentsConf.cmi componentsConf.cmi : -discrimination_tree.cmx : trie.cmx hExtlib.cmx discrimination_tree.cmi +hExtlib.cmi : +hMarshal.cmi : +patternMatcher.cmi : +hLog.cmi : +trie.cmi : discrimination_tree.cmi : -graphvizPp.cmx : graphvizPp.cmi +hTopoSort.cmi : graphvizPp.cmi : +componentsConf.cmo : componentsConf.cmi +componentsConf.cmx : componentsConf.cmi +hExtlib.cmo : hExtlib.cmi hExtlib.cmx : hExtlib.cmi -hExtlib.cmi : -hLog.cmx : hLog.cmi -hLog.cmi : +hMarshal.cmo : hExtlib.cmi hMarshal.cmi hMarshal.cmx : hExtlib.cmx hMarshal.cmi -hMarshal.cmi : -hTopoSort.cmx : hTopoSort.cmi -hTopoSort.cmi : +patternMatcher.cmo : patternMatcher.cmi patternMatcher.cmx : patternMatcher.cmi -patternMatcher.cmi : +hLog.cmo : hLog.cmi +hLog.cmx : hLog.cmi +trie.cmo : trie.cmi trie.cmx : trie.cmi -trie.cmi : +discrimination_tree.cmo : trie.cmi hExtlib.cmi discrimination_tree.cmi +discrimination_tree.cmx : trie.cmx hExtlib.cmx discrimination_tree.cmi +hTopoSort.cmo : hTopoSort.cmi +hTopoSort.cmx : hTopoSort.cmi +graphvizPp.cmo : graphvizPp.cmi +graphvizPp.cmx : graphvizPp.cmi diff --git a/matita/components/extlib/hExtlib.ml b/matita/components/extlib/hExtlib.ml index 8871a35df..576101053 100644 --- a/matita/components/extlib/hExtlib.ml +++ b/matita/components/extlib/hExtlib.ml @@ -460,12 +460,12 @@ let input_file fname = let input_all ic = let size = 10240 in let buf = Buffer.create size in - let s = String.create size in + let s = Bytes.create size in (try while true do let bytes = input ic s 0 size in if bytes = 0 then raise End_of_file - else Buffer.add_substring buf s 0 bytes + else Buffer.add_subbytes buf s 0 bytes done with End_of_file -> ()); Buffer.contents buf diff --git a/matita/components/extlib/hMarshal.ml b/matita/components/extlib/hMarshal.ml index cb4976e7d..c61977894 100644 --- a/matita/components/extlib/hMarshal.ml +++ b/matita/components/extlib/hMarshal.ml @@ -46,8 +46,8 @@ let save ~fmt ~version ~fname data = HExtlib.chmod 0o664 fname let expect ic fname s = - let len = String.length s in - let buf = String.create len in + let len = Bytes.length s in + let buf = Bytes.create len in really_input ic buf 0 len; if buf <> s then raise (Corrupt_file fname) @@ -61,8 +61,8 @@ let load ~fmt ~version ~fname = if fmt' <> Hashtbl.hash fmt then raise (Format_mismatch fname); let version' = input_binary_int ic in (* field 2 *) if version' <> version then raise (Version_mismatch fname); - expect ic fname fmt; (* field 3 *) - expect ic fname (string_of_int version); (* field 4 *) + expect ic fname (Bytes.of_string fmt); (* field 3 *) + expect ic fname (Bytes.of_string (string_of_int version)); (* field 4 *) let checksum' = input_binary_int ic in (* field 5 *) let marshalled' = HExtlib.input_all ic in (* field 6 *) if checksum' <> Hashtbl.hash marshalled' then diff --git a/matita/components/getter/.depend.opt b/matita/components/getter/.depend.opt index 1d016d277..7c2b60586 100644 --- a/matita/components/getter/.depend.opt +++ b/matita/components/getter/.depend.opt @@ -1,23 +1,38 @@ -http_getter.cmx : http_getter_wget.cmx http_getter_types.cmx \ - http_getter_storage.cmx http_getter_misc.cmx http_getter_logger.cmx \ - http_getter_env.cmx http_getter_const.cmx http_getter_common.cmx \ - http_getter.cmi -http_getter.cmi : http_getter_types.cmx -http_getter_common.cmx : http_getter_types.cmx http_getter_misc.cmx \ - http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi -http_getter_common.cmi : http_getter_types.cmx -http_getter_const.cmx : http_getter_const.cmi +http_getter_wget.cmi : +http_getter_logger.cmi : +http_getter_misc.cmi : http_getter_const.cmi : -http_getter_env.cmx : http_getter_types.cmx http_getter_misc.cmx \ - http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi http_getter_env.cmi : http_getter_types.cmx +http_getter_storage.cmi : +http_getter_common.cmi : http_getter_types.cmx +http_getter.cmi : http_getter_types.cmx +http_getter_types.cmo : +http_getter_types.cmx : +http_getter_wget.cmo : http_getter_types.cmx http_getter_wget.cmi +http_getter_wget.cmx : http_getter_types.cmx http_getter_wget.cmi +http_getter_logger.cmo : http_getter_logger.cmi http_getter_logger.cmx : http_getter_logger.cmi -http_getter_logger.cmi : +http_getter_misc.cmo : http_getter_logger.cmi http_getter_misc.cmi http_getter_misc.cmx : http_getter_logger.cmx http_getter_misc.cmi -http_getter_misc.cmi : +http_getter_const.cmo : http_getter_const.cmi +http_getter_const.cmx : http_getter_const.cmi +http_getter_env.cmo : http_getter_types.cmx http_getter_misc.cmi \ + http_getter_logger.cmi http_getter_const.cmi http_getter_env.cmi +http_getter_env.cmx : http_getter_types.cmx http_getter_misc.cmx \ + http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi +http_getter_storage.cmo : http_getter_wget.cmi http_getter_types.cmx \ + http_getter_misc.cmi http_getter_env.cmi http_getter_storage.cmi http_getter_storage.cmx : http_getter_wget.cmx http_getter_types.cmx \ http_getter_misc.cmx http_getter_env.cmx http_getter_storage.cmi -http_getter_storage.cmi : -http_getter_types.cmx : -http_getter_wget.cmx : http_getter_types.cmx http_getter_wget.cmi -http_getter_wget.cmi : +http_getter_common.cmo : http_getter_types.cmx http_getter_misc.cmi \ + http_getter_logger.cmi http_getter_env.cmi http_getter_common.cmi +http_getter_common.cmx : http_getter_types.cmx http_getter_misc.cmx \ + http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi +http_getter.cmo : http_getter_wget.cmi http_getter_types.cmx \ + http_getter_storage.cmi http_getter_misc.cmi http_getter_logger.cmi \ + http_getter_env.cmi http_getter_const.cmi http_getter_common.cmi \ + http_getter.cmi +http_getter.cmx : http_getter_wget.cmx http_getter_types.cmx \ + http_getter_storage.cmx http_getter_misc.cmx http_getter_logger.cmx \ + http_getter_env.cmx http_getter_const.cmx http_getter_common.cmx \ + http_getter.cmi diff --git a/matita/components/getter/http_getter_misc.ml b/matita/components/getter/http_getter_misc.ml index f7dffd066..d67dceff1 100644 --- a/matita/components/getter/http_getter_misc.ml +++ b/matita/components/getter/http_getter_misc.ml @@ -67,12 +67,12 @@ let iter_buf_size = 10240 let iter_file_data f fname = let ic = open_in fname in - let buf = String.create iter_buf_size in + let buf = Bytes.create iter_buf_size in try while true do let bytes = input ic buf 0 iter_buf_size in if bytes = 0 then raise End_of_file; - f (String.sub buf 0 bytes) + f (Bytes.to_string (Bytes.sub buf 0 bytes)) done with End_of_file -> close_in ic @@ -93,7 +93,7 @@ let cp src dst = let ic = open_in src in try let oc = open_out dst in - let buf = String.create bufsiz in + let buf = Bytes.create bufsiz in (try while true do let bytes = input ic buf 0 bufsiz in @@ -137,7 +137,7 @@ let wget ?output url = (let oc = open_out (match output with Some f -> f | None -> Filename.basename url) in - Http_user_agent.get_iter (fun data -> output_string oc data) url; + Http_user_agent.get_iter (fun data -> output_bytes oc data) url; close_out oc) | scheme -> (* unsupported scheme *) failwith ("Http_getter_misc.wget: unsupported scheme: " ^ scheme) @@ -147,7 +147,7 @@ let gzip ?(keep = false) ?output fname = Http_getter_logger.log ~level:3 (sprintf "gzipping %s (keep: %b, output: %s)" fname keep output); let (ic, oc) = (open_in fname, Gzip.open_out output) in - let buf = String.create bufsiz in + let buf = Bytes.create bufsiz in (try while true do let bytes = input ic buf 0 bufsiz in @@ -179,7 +179,7 @@ let gunzip ?(keep = false) ?output fname = try let ic = Gzip.open_in_chan zic in let oc = open_out output in - let buf = String.create bufsiz in + let buf = Bytes.create bufsiz in (try while true do let bytes = Gzip.input ic buf 0 bufsiz in @@ -240,11 +240,11 @@ let http_get url = let fname = Pcre.replace ~rex:file_scheme_RE url in try let size = (Unix.stat fname).Unix.st_size in - let buf = String.create size in + let buf = Bytes.create size in let ic = open_in fname in really_input ic buf 0 size ; close_in ic; - Some buf + Some (Bytes.to_string buf) with Unix.Unix_error (Unix.ENOENT, "stat", _) -> None end else (* other URL, pass it to Http_user_agent *) try @@ -298,11 +298,11 @@ let extension s = let temp_file_of_uri uri = let flat_string s s' c = - let cs = String.copy s in + let cs = Bytes.of_string s in for i = 0 to (String.length s) - 1 do if String.contains s' s.[i] then cs.[i] <- c done; - cs + Bytes.to_string cs in let user = try Unix.getlogin () with _ -> "" in Filename.open_temp_file (user ^ flat_string uri ".-=:;!?/&" '_') "" diff --git a/matita/components/getter/http_getter_wget.ml b/matita/components/getter/http_getter_wget.ml index 571479d78..0f44f07d5 100644 --- a/matita/components/getter/http_getter_wget.ml +++ b/matita/components/getter/http_getter_wget.ml @@ -40,7 +40,7 @@ let get url = let get_and_save url dest_filename = let out_channel = open_out dest_filename in (try - Http_user_agent.get_iter (output_string out_channel) url; + Http_user_agent.get_iter (output_bytes out_channel) url; with exn -> close_out out_channel; Sys.remove dest_filename; @@ -49,11 +49,11 @@ let get_and_save url dest_filename = let get_and_save_to_tmp url = let flat_string s s' c = - let cs = String.copy s in + let cs = Bytes.of_string s in for i = 0 to (String.length s) - 1 do if String.contains s' s.[i] then cs.[i] <- c done; - cs + Bytes.to_string cs in let user = try Unix.getlogin () with _ -> "" in let tmp_file = diff --git a/matita/components/grafite/.depend.opt b/matita/components/grafite/.depend.opt index 5dabb8012..4a1ca42e9 100644 --- a/matita/components/grafite/.depend.opt +++ b/matita/components/grafite/.depend.opt @@ -1,3 +1,5 @@ +grafiteAstPp.cmi : grafiteAst.cmx +grafiteAst.cmo : grafiteAst.cmx : +grafiteAstPp.cmo : grafiteAst.cmx grafiteAstPp.cmi grafiteAstPp.cmx : grafiteAst.cmx grafiteAstPp.cmi -grafiteAstPp.cmi : grafiteAst.cmx diff --git a/matita/components/grafite_engine/.depend.opt b/matita/components/grafite_engine/.depend.opt index 696b45881..e6d4942c6 100644 --- a/matita/components/grafite_engine/.depend.opt +++ b/matita/components/grafite_engine/.depend.opt @@ -1,7 +1,11 @@ -grafiteEngine.cmx : nCicCoercDeclaration.cmx grafiteTypes.cmx \ - grafiteEngine.cmi +grafiteTypes.cmi : +nCicCoercDeclaration.cmi : grafiteTypes.cmi grafiteEngine.cmi : grafiteTypes.cmi +grafiteTypes.cmo : grafiteTypes.cmi grafiteTypes.cmx : grafiteTypes.cmi -grafiteTypes.cmi : +nCicCoercDeclaration.cmo : grafiteTypes.cmi nCicCoercDeclaration.cmi nCicCoercDeclaration.cmx : grafiteTypes.cmx nCicCoercDeclaration.cmi -nCicCoercDeclaration.cmi : grafiteTypes.cmi +grafiteEngine.cmo : nCicCoercDeclaration.cmi grafiteTypes.cmi \ + grafiteEngine.cmi +grafiteEngine.cmx : nCicCoercDeclaration.cmx grafiteTypes.cmx \ + grafiteEngine.cmi diff --git a/matita/components/grafite_parser/.depend.opt b/matita/components/grafite_parser/.depend.opt index e0e6dac9c..752b0d88d 100644 --- a/matita/components/grafite_parser/.depend.opt +++ b/matita/components/grafite_parser/.depend.opt @@ -1,4 +1,6 @@ -grafiteParser.cmx : grafiteParser.cmi grafiteParser.cmi : -print_grammar.cmx : print_grammar.cmi print_grammar.cmi : grafiteParser.cmi +grafiteParser.cmo : grafiteParser.cmi +grafiteParser.cmx : grafiteParser.cmi +print_grammar.cmo : print_grammar.cmi +print_grammar.cmx : print_grammar.cmi diff --git a/matita/components/grafite_parser/Makefile b/matita/components/grafite_parser/Makefile index 164153916..3bf2dfa62 100644 --- a/matita/components/grafite_parser/Makefile +++ b/matita/components/grafite_parser/Makefile @@ -14,7 +14,7 @@ clean: # soon as we have ocaml 3.09 everywhere and "loc" occurrences are replaced by # "_loc" occurrences UTF8DIR = $(shell $(OCAMLFIND) query helm-syntax_extensions) -ULEXDIR = $(shell $(OCAMLFIND) query ulex08) +ULEXDIR = $(shell $(OCAMLFIND) query ulex-camlp5) MY_SYNTAXOPTIONS = -pp "camlp5o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc" grafiteParser.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) grafiteParser.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS) diff --git a/matita/components/library/.depend.opt b/matita/components/library/.depend.opt index 27ecf9383..6f2769b94 100644 --- a/matita/components/library/.depend.opt +++ b/matita/components/library/.depend.opt @@ -1,6 +1,9 @@ -librarian.cmx : librarian.cmi librarian.cmi : -libraryClean.cmx : libraryClean.cmi +libraryMisc.cmi : libraryClean.cmi : +librarian.cmo : librarian.cmi +librarian.cmx : librarian.cmi +libraryMisc.cmo : libraryMisc.cmi libraryMisc.cmx : libraryMisc.cmi -libraryMisc.cmi : +libraryClean.cmo : libraryClean.cmi +libraryClean.cmx : libraryClean.cmi diff --git a/matita/components/logger/.depend.opt b/matita/components/logger/.depend.opt index ed934897f..d1b4c3716 100644 --- a/matita/components/logger/.depend.opt +++ b/matita/components/logger/.depend.opt @@ -1,2 +1,3 @@ -helmLogger.cmx : helmLogger.cmi helmLogger.cmi : +helmLogger.cmo : helmLogger.cmi +helmLogger.cmx : helmLogger.cmi diff --git a/matita/components/ng_cic_content/.depend.opt b/matita/components/ng_cic_content/.depend.opt index df8d6d635..01e2f5b1e 100644 --- a/matita/components/ng_cic_content/.depend.opt +++ b/matita/components/ng_cic_content/.depend.opt @@ -1,4 +1,6 @@ -interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi +ncic2astMatcher.cmi : interpretations.cmi : +ncic2astMatcher.cmo : ncic2astMatcher.cmi ncic2astMatcher.cmx : ncic2astMatcher.cmi -ncic2astMatcher.cmi : +interpretations.cmo : ncic2astMatcher.cmi interpretations.cmi +interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi diff --git a/matita/components/ng_disambiguation/.depend.opt b/matita/components/ng_disambiguation/.depend.opt index d5eef6bc0..79fd839b2 100644 --- a/matita/components/ng_disambiguation/.depend.opt +++ b/matita/components/ng_disambiguation/.depend.opt @@ -1,9 +1,14 @@ -disambiguateChoices.cmx : nnumber_notation.cmx disambiguateChoices.cmi +nnumber_notation.cmi : disambiguateChoices.cmi : -grafiteDisambiguate.cmx : nCicDisambiguate.cmx disambiguateChoices.cmx \ - grafiteDisambiguate.cmi -grafiteDisambiguate.cmi : -nCicDisambiguate.cmx : nCicDisambiguate.cmi nCicDisambiguate.cmi : +grafiteDisambiguate.cmi : +nnumber_notation.cmo : nnumber_notation.cmi nnumber_notation.cmx : nnumber_notation.cmi -nnumber_notation.cmi : +disambiguateChoices.cmo : nnumber_notation.cmi disambiguateChoices.cmi +disambiguateChoices.cmx : nnumber_notation.cmx disambiguateChoices.cmi +nCicDisambiguate.cmo : nCicDisambiguate.cmi +nCicDisambiguate.cmx : nCicDisambiguate.cmi +grafiteDisambiguate.cmo : nCicDisambiguate.cmi disambiguateChoices.cmi \ + grafiteDisambiguate.cmi +grafiteDisambiguate.cmx : nCicDisambiguate.cmx disambiguateChoices.cmx \ + grafiteDisambiguate.cmi diff --git a/matita/components/ng_extraction/.depend.opt b/matita/components/ng_extraction/.depend.opt index 03f5f9a00..968d8ffe9 100644 --- a/matita/components/ng_extraction/.depend.opt +++ b/matita/components/ng_extraction/.depend.opt @@ -1,21 +1,34 @@ -common.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ - common.cmi -common.cmi : ocamlExtractionTable.cmi mlutil.cmi miniml.cmx coq.cmi -coq.cmx : coq.cmi +nCicExtraction.cmi : coq.cmi : -extraction.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ - common.cmx extraction.cmi +ocamlExtractionTable.cmi : miniml.cmx coq.cmi +mlutil.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi +common.cmi : ocamlExtractionTable.cmi mlutil.cmi miniml.cmx coq.cmi extraction.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi +ocaml.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi +ocamlExtraction.cmi : ocamlExtractionTable.cmi +miniml.cmo : coq.cmi miniml.cmx : coq.cmx -mlutil.cmx : ocamlExtractionTable.cmx miniml.cmx coq.cmx mlutil.cmi -mlutil.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi +nCicExtraction.cmo : nCicExtraction.cmi nCicExtraction.cmx : nCicExtraction.cmi -nCicExtraction.cmi : +coq.cmo : coq.cmi +coq.cmx : coq.cmi +ocamlExtractionTable.cmo : miniml.cmx coq.cmi ocamlExtractionTable.cmi +ocamlExtractionTable.cmx : miniml.cmx coq.cmx ocamlExtractionTable.cmi +mlutil.cmo : ocamlExtractionTable.cmi miniml.cmx coq.cmi mlutil.cmi +mlutil.cmx : ocamlExtractionTable.cmx miniml.cmx coq.cmx mlutil.cmi +common.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmx coq.cmi \ + common.cmi +common.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ + common.cmi +extraction.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmx coq.cmi \ + common.cmi extraction.cmi +extraction.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ + common.cmx extraction.cmi +ocaml.cmo : ocamlExtractionTable.cmi mlutil.cmi miniml.cmx coq.cmi \ + common.cmi ocaml.cmi ocaml.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \ common.cmx ocaml.cmi -ocaml.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi +ocamlExtraction.cmo : ocamlExtractionTable.cmi ocaml.cmi extraction.cmi \ + coq.cmi ocamlExtraction.cmi ocamlExtraction.cmx : ocamlExtractionTable.cmx ocaml.cmx extraction.cmx \ coq.cmx ocamlExtraction.cmi -ocamlExtraction.cmi : ocamlExtractionTable.cmi -ocamlExtractionTable.cmx : miniml.cmx coq.cmx ocamlExtractionTable.cmi -ocamlExtractionTable.cmi : miniml.cmx coq.cmi diff --git a/matita/components/ng_extraction/coq.ml b/matita/components/ng_extraction/coq.ml index f68562c20..130f7ebdf 100644 --- a/matita/components/ng_extraction/coq.ml +++ b/matita/components/ng_extraction/coq.ml @@ -25,7 +25,7 @@ let cut_ident skip_quote s = numpart (n-1) n' else if code_of_0 <= c && c <= code_of_9 then numpart (n-1) (n-1) - else if skip_quote & (c = Char.code '\'' || c = Char.code '_') then + else if skip_quote && (c = Char.code '\'' || c = Char.code '_') then numpart (n-1) (n-1) else n' @@ -34,9 +34,9 @@ let cut_ident skip_quote s = let forget_subscript id = let numstart = cut_ident false id in - let newid = String.make (numstart+1) '0' in + let newid = Bytes.make (numstart+1) '0' in String.blit id 0 newid 0 numstart; - newid + Bytes.to_string newid (* Namegen.ml *) @@ -58,18 +58,18 @@ let lift_subscript id = add (carrypos-1) end else begin - let newid = String.copy id in - String.fill newid (carrypos+1) (len-1-carrypos) '0'; + let newid = Bytes.of_string id in + Bytes.fill newid (carrypos+1) (len-1-carrypos) '0'; newid.[carrypos] <- Char.chr (Char.code c + 1); - newid + Bytes.to_string newid end else begin - let newid = id^"0" in + let newid = Bytes.of_string (id^"0") in if carrypos < len-1 then begin - String.fill newid (carrypos+1) (len-1-carrypos) '0'; + Bytes.fill newid (carrypos+1) (len-1-carrypos) '0'; newid.[carrypos+1] <- '1' end; - newid + Bytes.to_string newid end in add (len-1) diff --git a/matita/components/ng_extraction/nCicExtraction.ml b/matita/components/ng_extraction/nCicExtraction.ml index 12261145e..18b7086f5 100644 --- a/matita/components/ng_extraction/nCicExtraction.ml +++ b/matita/components/ng_extraction/nCicExtraction.ml @@ -844,7 +844,7 @@ let object_of_constant status ~metasenv ref bo ty = (fun p1 n -> HExtlib.map_option (fun (_,k) -> (*CSC: BUG here, clashes*) - String.uncapitalize (fst n),k) p1) + String.uncapitalize_ascii (fst n),k) p1) ctx0 ctx in let bo = typ_of status ~metasenv ctx bo in @@ -962,15 +962,15 @@ let (|>) f g = fun x -> g (f x) ;; -let curry f x y = +(*let curry f x y = f (x, y) -;; +;;*) let uncurry f (x, y) = f x y ;; -let rec char_list_of_string s = +let char_list_of_string s = let l = String.length s in let rec aux buffer s = function @@ -1013,8 +1013,10 @@ let rec capitalize_marked_positions s = | [] -> s | x::xs -> if x < String.length s then - let c = Char.uppercase (String.get s x) in - let _ = String.set s x c in + let c = Char.uppercase_ascii (String.get s x) in + let b = Bytes.of_string s in + let _ = Bytes.set b x c in + let s = Bytes.to_string b in capitalize_marked_positions s xs else capitalize_marked_positions s xs @@ -1028,12 +1030,12 @@ let contract_underscores_and_capitalise = let idiomatic_haskell_type_name_of_string = contract_underscores_and_capitalise |> - String.capitalize + String.capitalize_ascii ;; let idiomatic_haskell_term_name_of_string = contract_underscores_and_capitalise |> - String.uncapitalize + String.uncapitalize_ascii ;; let classify_reference status ref = @@ -1223,7 +1225,7 @@ let rec pp_obj status (_,ref,obj_kind) = ) il) (* inductive and records missing *) -let rec infos_of (info,_,obj_kind) = +let infos_of (info,_,obj_kind) = info @ match obj_kind with LetRec l -> List.concat (List.map (fun (infos,_,_) -> infos) l) diff --git a/matita/components/ng_kernel/.depend b/matita/components/ng_kernel/.depend index 16e1dcf8e..13791fbad 100644 --- a/matita/components/ng_kernel/.depend +++ b/matita/components/ng_kernel/.depend @@ -30,8 +30,8 @@ nCicUntrusted.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ nCicUntrusted.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi nCicUntrusted.cmi : nCic.cmo -nCicUtils.cmo : nReference.cmi nCic.cmo nCicUtils.cmi -nCicUtils.cmx : nReference.cmx nCic.cmx nCicUtils.cmi +nCicUtils.cmo : nCic.cmo nCicUtils.cmi +nCicUtils.cmx : nCic.cmx nCicUtils.cmi nCicUtils.cmi : nCic.cmo nReference.cmo : nUri.cmi nReference.cmi nReference.cmx : nUri.cmx nReference.cmi diff --git a/matita/components/ng_kernel/.depend.opt b/matita/components/ng_kernel/.depend.opt index fe2e99a30..5b0507784 100644 --- a/matita/components/ng_kernel/.depend.opt +++ b/matita/components/ng_kernel/.depend.opt @@ -1,25 +1,41 @@ -nCic.cmx : nUri.cmx nReference.cmx -nCicEnvironment.cmx : nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi +nUri.cmi : +nReference.cmi : nUri.cmi +nCicUtils.cmi : nCic.cmx +nCicSubstitution.cmi : nCic.cmx nCicEnvironment.cmi : nUri.cmi nReference.cmi nCic.cmx -nCicPp.cmx : nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \ - nCicEnvironment.cmx nCic.cmx nCicPp.cmi -nCicPp.cmi : nReference.cmi nCic.cmx -nCicReduction.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ - nCicEnvironment.cmx nCic.cmx nCicReduction.cmi nCicReduction.cmi : nCic.cmx +nCicTypeChecker.cmi : nUri.cmi nReference.cmi nCic.cmx +nCicUntrusted.cmi : nCic.cmx +nCicPp.cmi : nReference.cmi nCic.cmx +nCic.cmo : nUri.cmi nReference.cmi +nCic.cmx : nUri.cmx nReference.cmx +nUri.cmo : nUri.cmi +nUri.cmx : nUri.cmi +nReference.cmo : nUri.cmi nReference.cmi +nReference.cmx : nUri.cmx nReference.cmi +nCicUtils.cmo : nReference.cmi nCic.cmx nCicUtils.cmi +nCicUtils.cmx : nReference.cmx nCic.cmx nCicUtils.cmi +nCicSubstitution.cmo : nReference.cmi nCicUtils.cmi nCic.cmx \ + nCicSubstitution.cmi nCicSubstitution.cmx : nReference.cmx nCicUtils.cmx nCic.cmx \ nCicSubstitution.cmi -nCicSubstitution.cmi : nCic.cmx +nCicEnvironment.cmo : nUri.cmi nReference.cmi nCic.cmx nCicEnvironment.cmi +nCicEnvironment.cmx : nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi +nCicReduction.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ + nCicEnvironment.cmi nCic.cmx nCicReduction.cmi +nCicReduction.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ + nCicEnvironment.cmx nCic.cmx nCicReduction.cmi +nCicTypeChecker.cmo : nUri.cmi nReference.cmi nCicUtils.cmi \ + nCicSubstitution.cmi nCicReduction.cmi nCicEnvironment.cmi nCic.cmx \ + nCicTypeChecker.cmi nCicTypeChecker.cmx : nUri.cmx nReference.cmx nCicUtils.cmx \ nCicSubstitution.cmx nCicReduction.cmx nCicEnvironment.cmx nCic.cmx \ nCicTypeChecker.cmi -nCicTypeChecker.cmi : nUri.cmi nReference.cmi nCic.cmx +nCicUntrusted.cmo : nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ + nCicReduction.cmi nCicEnvironment.cmi nCic.cmx nCicUntrusted.cmi nCicUntrusted.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi -nCicUntrusted.cmi : nCic.cmx -nCicUtils.cmx : nReference.cmx nCic.cmx nCicUtils.cmi -nCicUtils.cmi : nCic.cmx -nReference.cmx : nUri.cmx nReference.cmi -nReference.cmi : nUri.cmi -nUri.cmx : nUri.cmi -nUri.cmi : +nCicPp.cmo : nUri.cmi nReference.cmi nCicSubstitution.cmi nCicReduction.cmi \ + nCicEnvironment.cmi nCic.cmx nCicPp.cmi +nCicPp.cmx : nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \ + nCicEnvironment.cmx nCic.cmx nCicPp.cmi diff --git a/matita/components/ng_kernel/nCicSubstitution.ml b/matita/components/ng_kernel/nCicSubstitution.ml index 0ca566cc3..2e382f434 100644 --- a/matita/components/ng_kernel/nCicSubstitution.ml +++ b/matita/components/ng_kernel/nCicSubstitution.ml @@ -14,8 +14,6 @@ module C = NCic module Ref = NReference -let debug_print = fun _ -> ();; - let lift_from status ?(no_implicit=true) k n = let rec liftaux k = function | C.Rel m as t -> if m < k then t else C.Rel (m + n) diff --git a/matita/components/ng_kernel/nCicUtils.ml b/matita/components/ng_kernel/nCicUtils.ml index f22e02a7e..398df307e 100644 --- a/matita/components/ng_kernel/nCicUtils.ml +++ b/matita/components/ng_kernel/nCicUtils.ml @@ -12,7 +12,6 @@ (* $Id$ *) module C = NCic -module Ref = NReference exception Subst_not_found of int exception Meta_not_found of int diff --git a/matita/components/ng_library/.depend.opt b/matita/components/ng_library/.depend.opt index 07d53f5dd..a571a865c 100644 --- a/matita/components/ng_library/.depend.opt +++ b/matita/components/ng_library/.depend.opt @@ -1,2 +1,3 @@ -nCicLibrary.cmx : nCicLibrary.cmi nCicLibrary.cmi : +nCicLibrary.cmo : nCicLibrary.cmi +nCicLibrary.cmx : nCicLibrary.cmi diff --git a/matita/components/ng_paramodulation/.depend.opt b/matita/components/ng_paramodulation/.depend.opt index 6e58a4ca9..5f4f1cc56 100644 --- a/matita/components/ng_paramodulation/.depend.opt +++ b/matita/components/ng_paramodulation/.depend.opt @@ -1,29 +1,45 @@ -foSubst.cmx : terms.cmx foSubst.cmi +terms.cmi : +pp.cmi : terms.cmi foSubst.cmi : terms.cmi -foUnif.cmx : terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi -foUnif.cmi : terms.cmi orderings.cmi -foUtils.cmx : terms.cmx orderings.cmx foSubst.cmx foUtils.cmi +orderings.cmi : terms.cmi foUtils.cmi : terms.cmi orderings.cmi -index.cmx : terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx index.cmi +foUnif.cmi : terms.cmi orderings.cmi index.cmi : terms.cmi orderings.cmi -nCicBlob.cmx : terms.cmx foUtils.cmx nCicBlob.cmi +superposition.cmi : terms.cmi orderings.cmi index.cmi +stats.cmi : terms.cmi orderings.cmi +paramod.cmi : terms.cmi orderings.cmi nCicBlob.cmi : terms.cmi -nCicParamod.cmx : terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \ - nCicBlob.cmx nCicParamod.cmi -nCicParamod.cmi : terms.cmi -nCicProof.cmx : terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi nCicProof.cmi : terms.cmi -orderings.cmx : terms.cmx pp.cmx foSubst.cmx orderings.cmi -orderings.cmi : terms.cmi -paramod.cmx : terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \ - foUtils.cmx foUnif.cmx paramod.cmi -paramod.cmi : terms.cmi orderings.cmi +nCicParamod.cmi : terms.cmi +terms.cmo : terms.cmi +terms.cmx : terms.cmi +pp.cmo : terms.cmi pp.cmi pp.cmx : terms.cmx pp.cmi -pp.cmi : terms.cmi -stats.cmx : terms.cmx stats.cmi -stats.cmi : terms.cmi orderings.cmi +foSubst.cmo : terms.cmi foSubst.cmi +foSubst.cmx : terms.cmx foSubst.cmi +orderings.cmo : terms.cmi pp.cmi foSubst.cmi orderings.cmi +orderings.cmx : terms.cmx pp.cmx foSubst.cmx orderings.cmi +foUtils.cmo : terms.cmi orderings.cmi foSubst.cmi foUtils.cmi +foUtils.cmx : terms.cmx orderings.cmx foSubst.cmx foUtils.cmi +foUnif.cmo : terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi +foUnif.cmx : terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi +index.cmo : terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi index.cmi +index.cmx : terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx index.cmi +superposition.cmo : terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \ + foUnif.cmi foSubst.cmi superposition.cmi superposition.cmx : terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \ foUnif.cmx foSubst.cmx superposition.cmi -superposition.cmi : terms.cmi orderings.cmi index.cmi -terms.cmx : terms.cmi -terms.cmi : +stats.cmo : terms.cmi stats.cmi +stats.cmx : terms.cmx stats.cmi +paramod.cmo : terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \ + foUtils.cmi foUnif.cmi paramod.cmi +paramod.cmx : terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \ + foUtils.cmx foUnif.cmx paramod.cmi +nCicBlob.cmo : terms.cmi foUtils.cmi nCicBlob.cmi +nCicBlob.cmx : terms.cmx foUtils.cmx nCicBlob.cmi +nCicProof.cmo : terms.cmi pp.cmi nCicBlob.cmi foSubst.cmi nCicProof.cmi +nCicProof.cmx : terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi +nCicParamod.cmo : terms.cmi pp.cmi paramod.cmi orderings.cmi nCicProof.cmi \ + nCicBlob.cmi nCicParamod.cmi +nCicParamod.cmx : terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \ + nCicBlob.cmx nCicParamod.cmi diff --git a/matita/components/ng_refiner/.depend.opt b/matita/components/ng_refiner/.depend.opt index dab873890..d8295760a 100644 --- a/matita/components/ng_refiner/.depend.opt +++ b/matita/components/ng_refiner/.depend.opt @@ -1,17 +1,27 @@ -nCicCoercion.cmx : nDiscriminationTree.cmx nCicUnifHint.cmx \ - nCicMetaSubst.cmx nCicCoercion.cmi -nCicCoercion.cmi : nCicUnifHint.cmi -nCicMetaSubst.cmx : nCicMetaSubst.cmi +nDiscriminationTree.cmi : nCicMetaSubst.cmi : -nCicRefineUtil.cmx : nCicMetaSubst.cmx nCicRefineUtil.cmi +nCicUnifHint.cmi : +nCicCoercion.cmi : nCicUnifHint.cmi nCicRefineUtil.cmi : -nCicRefiner.cmx : nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \ - nCicCoercion.cmx nCicRefiner.cmi +nCicUnification.cmi : nCicCoercion.cmi nCicRefiner.cmi : nCicCoercion.cmi +nDiscriminationTree.cmo : nDiscriminationTree.cmi +nDiscriminationTree.cmx : nDiscriminationTree.cmi +nCicMetaSubst.cmo : nCicMetaSubst.cmi +nCicMetaSubst.cmx : nCicMetaSubst.cmi +nCicUnifHint.cmo : nDiscriminationTree.cmi nCicMetaSubst.cmi \ + nCicUnifHint.cmi nCicUnifHint.cmx : nDiscriminationTree.cmx nCicMetaSubst.cmx \ nCicUnifHint.cmi -nCicUnifHint.cmi : +nCicCoercion.cmo : nDiscriminationTree.cmi nCicUnifHint.cmi \ + nCicMetaSubst.cmi nCicCoercion.cmi +nCicCoercion.cmx : nDiscriminationTree.cmx nCicUnifHint.cmx \ + nCicMetaSubst.cmx nCicCoercion.cmi +nCicRefineUtil.cmo : nCicMetaSubst.cmi nCicRefineUtil.cmi +nCicRefineUtil.cmx : nCicMetaSubst.cmx nCicRefineUtil.cmi +nCicUnification.cmo : nCicUnifHint.cmi nCicMetaSubst.cmi nCicUnification.cmi nCicUnification.cmx : nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi -nCicUnification.cmi : nCicCoercion.cmi -nDiscriminationTree.cmx : nDiscriminationTree.cmi -nDiscriminationTree.cmi : +nCicRefiner.cmo : nCicUnification.cmi nCicRefineUtil.cmi nCicMetaSubst.cmi \ + nCicCoercion.cmi nCicRefiner.cmi +nCicRefiner.cmx : nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \ + nCicCoercion.cmx nCicRefiner.cmi diff --git a/matita/components/ng_tactics/.depend.opt b/matita/components/ng_tactics/.depend.opt index c8999df5a..e8ca8210e 100644 --- a/matita/components/ng_tactics/.depend.opt +++ b/matita/components/ng_tactics/.depend.opt @@ -1,19 +1,30 @@ -continuationals.cmx : continuationals.cmi continuationals.cmi : -nCicElim.cmx : nCicElim.cmi -nCicElim.cmi : -nCicTacReduction.cmx : nCicTacReduction.cmi nCicTacReduction.cmi : -nDestructTac.cmx : nTactics.cmx nTacStatus.cmx continuationals.cmx \ - nDestructTac.cmi +nTacStatus.cmi : continuationals.cmi +nCicElim.cmi : +nTactics.cmi : nTacStatus.cmi +nnAuto.cmi : nTacStatus.cmi nDestructTac.cmi : nTacStatus.cmi -nInversion.cmx : nTactics.cmx nTacStatus.cmx nCicElim.cmx \ - continuationals.cmx nInversion.cmi nInversion.cmi : nTacStatus.cmi +continuationals.cmo : continuationals.cmi +continuationals.cmx : continuationals.cmi +nCicTacReduction.cmo : nCicTacReduction.cmi +nCicTacReduction.cmx : nCicTacReduction.cmi +nTacStatus.cmo : nCicTacReduction.cmi continuationals.cmi nTacStatus.cmi nTacStatus.cmx : nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi -nTacStatus.cmi : continuationals.cmi +nCicElim.cmo : nCicElim.cmi +nCicElim.cmx : nCicElim.cmi +nTactics.cmo : nTacStatus.cmi nCicElim.cmi continuationals.cmi nTactics.cmi nTactics.cmx : nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi -nTactics.cmi : nTacStatus.cmi +nnAuto.cmo : nTactics.cmi nTacStatus.cmi nCicTacReduction.cmi \ + continuationals.cmi nnAuto.cmi nnAuto.cmx : nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \ continuationals.cmx nnAuto.cmi -nnAuto.cmi : nTacStatus.cmi +nDestructTac.cmo : nTactics.cmi nTacStatus.cmi continuationals.cmi \ + nDestructTac.cmi +nDestructTac.cmx : nTactics.cmx nTacStatus.cmx continuationals.cmx \ + nDestructTac.cmi +nInversion.cmo : nTactics.cmi nTacStatus.cmi nCicElim.cmi \ + continuationals.cmi nInversion.cmi +nInversion.cmx : nTactics.cmx nTacStatus.cmx nCicElim.cmx \ + continuationals.cmx nInversion.cmi diff --git a/matita/components/registry/.depend.opt b/matita/components/registry/.depend.opt index f28210446..67113e67f 100644 --- a/matita/components/registry/.depend.opt +++ b/matita/components/registry/.depend.opt @@ -1,2 +1,3 @@ -helm_registry.cmx : helm_registry.cmi helm_registry.cmi : +helm_registry.cmo : helm_registry.cmi +helm_registry.cmx : helm_registry.cmi diff --git a/matita/components/registry/helm_registry.ml b/matita/components/registry/helm_registry.ml index 08b1bb76f..43037aac0 100644 --- a/matita/components/registry/helm_registry.ml +++ b/matita/components/registry/helm_registry.ml @@ -145,7 +145,7 @@ let set' ?(replace=false) registry ~key ~value = let unset registry = Hashtbl.remove registry -let env_var_of_key s = String.uppercase (Str.global_replace dot_rex "_" s) +let env_var_of_key s = String.uppercase_ascii (Str.global_replace dot_rex "_" s) let singleton = function | [] -> diff --git a/matita/components/syntax_extensions/.depend.opt b/matita/components/syntax_extensions/.depend.opt index 98ac1d844..24f371ca7 100644 --- a/matita/components/syntax_extensions/.depend.opt +++ b/matita/components/syntax_extensions/.depend.opt @@ -1,3 +1,5 @@ -utf8Macro.cmx : utf8MacroTable.cmx utf8Macro.cmi utf8Macro.cmi : +utf8MacroTable.cmo : utf8MacroTable.cmx : +utf8Macro.cmo : utf8MacroTable.cmx utf8Macro.cmi +utf8Macro.cmx : utf8MacroTable.cmx utf8Macro.cmi diff --git a/matita/components/thread/.depend.opt b/matita/components/thread/.depend.opt index 8ee8dbbec..d68336af1 100644 --- a/matita/components/thread/.depend.opt +++ b/matita/components/thread/.depend.opt @@ -1,4 +1,6 @@ -extThread.cmx : extThread.cmi +threadSafe.cmi : extThread.cmi : +threadSafe.cmo : threadSafe.cmi threadSafe.cmx : threadSafe.cmi -threadSafe.cmi : +extThread.cmo : extThread.cmi +extThread.cmx : extThread.cmi diff --git a/matita/components/xml/.depend.opt b/matita/components/xml/.depend.opt index 36a543808..fd3f626b9 100644 --- a/matita/components/xml/.depend.opt +++ b/matita/components/xml/.depend.opt @@ -1,4 +1,6 @@ -xml.cmx : xml.cmi xml.cmi : -xmlPushParser.cmx : xmlPushParser.cmi xmlPushParser.cmi : +xml.cmo : xml.cmi +xml.cmx : xml.cmi +xmlPushParser.cmo : xmlPushParser.cmi +xmlPushParser.cmx : xmlPushParser.cmi diff --git a/matita/components/xml/xml.ml b/matita/components/xml/xml.ml index 0e3a4bcc2..9696fa4bc 100644 --- a/matita/components/xml/xml.ml +++ b/matita/components/xml/xml.ml @@ -104,7 +104,7 @@ let pp_to_outchan strm oc = ;; let pp_to_gzipchan strm oc = - pp_gen (fun s -> Gzip.output oc s 0 (String.length s)) strm + pp_gen (fun s -> Gzip.output oc (Bytes.of_string s) 0 (String.length s)) strm ;; (** pretty printer to string *) diff --git a/matita/components/xml/xmlPushParser.ml b/matita/components/xml/xmlPushParser.ml index 4f57e1242..b809068f5 100644 --- a/matita/components/xml/xmlPushParser.ml +++ b/matita/components/xml/xmlPushParser.ml @@ -94,12 +94,12 @@ let parse expat_parser = aux (`Channel ic); close_in ic | `Gzip_channel ic -> - let buf = String.create gzip_bufsize in + let buf = Bytes.create gzip_bufsize in (try while true do let bytes = Gzip.input ic buf 0 gzip_bufsize in if bytes = 0 then raise End_of_file; - parse_fun (String.sub buf 0 bytes) + parse_fun (Bytes.to_string (Bytes.sub buf 0 bytes)) done with End_of_file -> final expat_parser) | `Gzip_file fname -> diff --git a/matita/configure.ac b/matita/configure.ac index 0670278be..36f787c66 100644 --- a/matita/configure.ac +++ b/matita/configure.ac @@ -24,11 +24,11 @@ if test $HAVE_OCAMLFIND = "yes"; then else AC_MSG_ERROR(could not find ocamlfind) fi -AC_CHECK_PROG(HAVE_LABLGLADECC, lablgladecc2, yes, no) +AC_CHECK_PROG(HAVE_LABLGLADECC, lablgladecc, yes, no) if test $HAVE_LABLGLADECC = "yes"; then - LABLGLADECC="lablgladecc2" + LABLGLADECC="lablgladecc" else - AC_MSG_ERROR(could not find lablgladecc2) + AC_MSG_ERROR(could not find lablgladecc) fi AC_CHECK_PROG(HAVE_CAMLP5O, camlp5o, yes, no) if test $HAVE_CAMLP5O = "yes"; then @@ -40,16 +40,17 @@ fi # look for METAS dir LIBSPATH="`pwd`/components" -OCAMLPATH="$LIBSPATH/METAS" +OCAMLPATHL="$LIBSPATH/METAS" +OCAMLPATH="$OCAMLPATHL:$OCAMLPATH" # creating META.* echo -n "creating METAs ... " -for f in $OCAMLPATH/meta.*.src; do +for f in $OCAMLPATHL/meta.*.src; do basename=`basename $f` metaname=`echo $basename | sed 's/meta\.\(.*\)\.src/\1/'` dirname=`echo $metaname | sed 's/^helm-//'` - metafile="$OCAMLPATH/META.$metaname" + metafile="$OCAMLPATHL/META.$metaname" cp $f $metafile echo "directory=\"$LIBSPATH/$dirname\"" >> $metafile done @@ -57,20 +58,21 @@ echo "done" # (libs) findlib requisites +#gdome2 \ +#mysql \ FINDLIB_LIBSREQUIRES="\ expat \ -gdome2 \ http \ -lablgtk2 \ -lablgtk2.sourceview2 \ -mysql \ +lablgtk3 \ +lablgtk3.sourceview3 \ netstring \ -ulex08 \ +ulex-camlp5 \ zip \ " # (Matita) findlib requisites +#lablgtk3.glade \ FINDLIB_COMREQUIRES="\ helm-disambiguation \ helm-grafite \ @@ -87,9 +89,9 @@ $FINDLIB_COMREQUIRES \ " FINDLIB_REQUIRES="\ $FINDLIB_CREQUIRES \ -lablgtk2.glade \ -lablgtk2.sourceview2 \ +lablgtk3.sourceview3 \ " + for r in $FINDLIB_LIBSREQUIRES $FINDLIB_REQUIRES do AC_MSG_CHECKING(for $r ocaml library) diff --git a/matita/matita/.depend b/matita/matita/.depend index 271861428..e6ef08473 100644 --- a/matita/matita/.depend +++ b/matita/matita/.depend @@ -37,6 +37,8 @@ matitaGui.cmx : matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ matitaMathView.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \ matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi matitaGui.cmi : matitaGuiTypes.cmi +matitaGuiInit.cmo : +matitaGuiInit.cmx : matitaGuiTypes.cmi : matitaGeneratedGui.cmo applyTransformation.cmi matitaInit.cmo : matitaExcPp.cmi buildTimeConf.cmo matitaInit.cmi matitaInit.cmx : matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi diff --git a/matita/matita/.depend.opt b/matita/matita/.depend.opt index 5c7d0715a..6de02fb28 100644 --- a/matita/matita/.depend.opt +++ b/matita/matita/.depend.opt @@ -21,6 +21,7 @@ matitaGui.cmx : matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ matitaMathView.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \ matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi matitaGui.cmi : matitaGuiTypes.cmi +matitaGuiInit.cmx : matitaGuiTypes.cmi : matitaGeneratedGui.cmx applyTransformation.cmi matitaInit.cmx : matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi matitaInit.cmi : diff --git a/matita/matita/Makefile b/matita/matita/Makefile index caf0f82ff..210920abe 100644 --- a/matita/matita/Makefile +++ b/matita/matita/Makefile @@ -11,7 +11,7 @@ else ANNOTOPTION = endif -OCAML_FLAGS = -pp $(CAMLP5O) -rectypes $(ANNOTOPTION) +OCAML_FLAGS = -pp $(CAMLP5O) -rectypes $(ANNOTOPTION) -w -52 OCAMLDEP_FLAGS = -pp $(CAMLP5O) PKGS = -package "$(MATITA_REQUIRES)" CPKGS = -package "$(MATITA_CREQUIRES)" @@ -61,7 +61,7 @@ MAINCMLI = \ matitaclean.mli \ $(NULL) # objects for matita (GTK GUI) -ML = buildTimeConf.ml matitaGeneratedGui.ml $(MLI:%.mli=%.ml) +ML = buildTimeConf.ml matitaGuiInit.ml matitaGeneratedGui.ml $(MLI:%.mli=%.ml) # objects for matitac (batch compiler) CML = buildTimeConf.ml $(CMLI:%.mli=%.ml) MAINCML = $(MAINCMLI:%.mli=%.ml) @@ -142,11 +142,10 @@ matitaclean: matitac matitaclean.opt: matitac.opt $(H)test -f $@ || ln -s $< $@ -matitaGeneratedGui.ml: matita.glade.utf8 - $(H)$(LABLGLADECC) -embed $< > matitaGeneratedGui.ml +matitaGeneratedGui.ml: matita.ui + #$(H)$(LABLGLADECC) -embed $< > matitaGeneratedGui.ml + $(H)$(LABLGLADECC) $< > matitaGeneratedGui.ml -matita.glade.utf8: matita.glade - $(H)xmllint --encode UTF8 $< > $@ .PHONY: clean clean: @@ -162,7 +161,6 @@ clean: .PHONY: distclean distclean: clean $(H)$(MAKE) -C dist/ clean - $(H)rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli $(H)rm -f buildTimeConf.ml $(H)rm -f matita.glade.bak matita.gladep.bak $(H)rm -f matita.conf.xml.sample @@ -204,7 +202,7 @@ cleantests.opt: $(foreach d,$(TEST_DIRS_OPT),$(d)-cleantests-opt) # {{{ Distribution stuff -dist_pre: matitaGeneratedGui.ml +dist_pre: $(MAKE) -C dist/ dist_pre WHERE = $(DESTDIR)/$(RT_BASE_DIR) diff --git a/matita/matita/cicMathView.ml b/matita/matita/cicMathView.ml index e06e0055d..ceb2e1f0d 100644 --- a/matita/matita/cicMathView.ml +++ b/matita/matita/cicMathView.ml @@ -28,7 +28,7 @@ open Printf open GrafiteTypes open MatitaGtkMisc open MatitaGuiTypes -open GtkSourceView2 +open GtkSourceView3 let matita_script_current = ref (fun _ -> (assert false : < advance: ?statement:string -> unit -> unit; status: GrafiteTypes.status >));; let register_matita_script_current f = matita_script_current := f;; @@ -174,9 +174,9 @@ let string_of_dom_node node = *) class clickableMathView obj = -let text_width = 80 in +(*let text_width = 80 in*) object (self) - inherit GSourceView2.source_view obj + inherit GSourceView3.source_view obj method strings_of_selection = (assert false : (paste_kind * string) list) @@ -690,7 +690,7 @@ let cicMathView (*?auto_indent ?highlight_current_line ?indent_on_tab ?indent_wi Gobject.set_params (Gobject.try_cast obj "GtkSourceView") pl; new _cicMathView obj)(*)) ?auto_indent ?highlight_current_line ?indent_on_tab ?indent_width ?insert_spaces_instead_of_tabs ?right_margin_position ?show_line_marks ?show_line_numbers ?show_right_margin ?smart_home_end ?tab_width ?editable ?cursor_visible ?justification ?wrap_mode ?accepts_tab ?border_width*) [] ?width ?height ?packing ?show () :> cicMathView) -let screenshot status sequents metasenv subst (filename as ofn) = +let screenshot status sequents metasenv subst (filename (*as ofn*)) = () (*MATITA 1.0 let w = GWindow.window ~title:"screenshot" () in let width = 500 in diff --git a/matita/matita/matita.ui b/matita/matita/matita.ui new file mode 100644 index 000000000..3ea0c2dd9 --- /dev/null +++ b/matita/matita/matita.ui @@ -0,0 +1,2980 @@ + + + + + + 600 + 400 + True + False + Auto + dialog + south-east + + + True + False + vertical + + + True + False + 2 + + + True + True + in + + + True + False + + + True + False + 3 + 3 + + + + + + + True + True + 0 + + + + + True + False + vertical + + + True + True + False + + + True + False + 0 + 0 + + + True + False + 2 + + + True + False + gtk-go-up + + + False + False + 0 + + + + + True + False + True + + + False + False + 1 + + + + + + + + + True + True + 0 + + + + + True + True + False + + + True + False + gtk-go-down + + + + + True + True + 1 + + + + + False + False + 1 + + + + + True + True + 0 + + + + + True + False + + + False + True + 3 + 1 + + + + + True + False + + + True + False + Last: + 0 + + + True + True + 0 + + + + + True + False + 4 + 4 + end + + + gtk-media-pause + True + True + True + False + True + + + False + False + 0 + + + + + gtk-media-play + True + True + True + False + True + + + False + False + 1 + + + + + gtk-media-next + True + True + True + False + True + + + False + False + 2 + + + + + gtk-close + True + True + True + False + True + + + False + False + 3 + + + + + True + True + 1 + + + + + False + True + 2 + + + + + + + 500 + 480 + True + False + Cic browser + center-on-parent + 500 + 480 + True + + + True + False + + + True + False + vertical + + + True + False + + + True + False + _File + True + + + False + + + True + False + _New + True + + + + + True + False + Open _Location ... + True + + + + + + True + False + + + + + True + False + _Quit + True + + + + + + + + + True + False + _Edit + True + + + False + + + True + False + _Copy + True + + + + + + + + + False + False + 0 + + + + + True + False + 0 + 0 + none + + + True + False + + + True + True + False + none + + + True + False + gtk-new + + + + + False + False + 0 + + + + + True + True + False + none + + + True + False + gtk-go-back + + + + + False + False + 1 + + + + + True + True + False + none + + + True + False + gtk-go-forward + + + + + False + False + 2 + + + + + True + True + True + False + refresh + none + + + True + False + gtk-refresh + + + + + False + False + 3 + + + + + True + True + True + False + home + none + + + True + False + gtk-home + + + + + False + False + 4 + + + + + True + False + gtk-jump-to + 2 + + + False + False + 3 + 5 + + + + + True + False + + + True + True + True + ● + + + True + True + 0 + + + + + True + True + 6 + + + + + + + False + True + 1 + + + + + True + True + + + True + True + + + + + True + False + MathView + + + False + + + + + True + True + in + + + True + True + False + + + + + + + + 1 + + + + + True + False + WhelpResult + + + 1 + False + + + + + True + True + + + True + False + none + + + True + False + gtk-missing-image + + + + + + + 2 + + + + + True + False + WhelpEasterEgg + + + 2 + False + + + + + True + True + + + 3 + + + + + True + False + Graph + + + 3 + False + + + + + True + False + vertical + + + True + True + 3 + in + + + True + True + 0 + + + + + True + False + 4 + 4 + + + True + False + vertical + + + True + True + 0 + + + + + True + True + True + + + True + True + 1 + + + + + True + True + False + + + True + False + 0 + 0 + + + True + False + 2 + + + True + False + gtk-find + + + False + False + 0 + + + + + True + False + Search + True + + + False + False + 1 + + + + + + + + + False + False + 2 + + + + + False + True + 1 + + + + + 4 + + + + + True + False + SearchText + + + 4 + False + + + + + True + True + 3 + + + + + + + + + False + DUMMY + False + True + center + dialog + + + True + False + vertical + + + True + False + end + + + gtk-cancel + True + True + True + False + True + + + False + False + 0 + + + + + gtk-ok + True + True + True + False + True + + + False + False + 1 + + + + + False + False + end + 0 + + + + + True + False + DUMMY + center + + + False + False + 2 + + + + + + ConfirmationDialogCancelButton + ConfirmationDialogOkButton + + + + 450 + 400 + False + title + True + dialog + + + True + False + vertical + + + True + False + end + + + gtk-help + True + True + True + False + True + + + False + False + 0 + + + + + True + True + True + False + + + True + False + 0 + 0 + + + True + False + 2 + + + True + False + gtk-zoom-in + + + False + False + 0 + + + + + True + False + More + True + + + False + False + 1 + + + + + + + + + False + False + 1 + + + + + gtk-cancel + True + True + True + True + False + True + + + False + False + 2 + + + + + gtk-ok + True + True + True + False + True + + + False + False + 3 + + + + + False + False + end + 0 + + + + + True + False + vertical + + + True + False + some informative message here ... + + + False + False + 0 + + + + + True + True + in + + + True + True + False + + + + + + + + True + True + 1 + + + + + False + True + 2 + + + + + + button6 + disambiguationErrorsMoreErrors + disambiguationErrorsCancelButton + disambiguationErrorsOkButton + + + + True + False + DUMMY + dialog + + + True + False + vertical + + + True + False + end + + + gtk-cancel + True + True + True + False + True + + + False + False + 0 + + + + + gtk-ok + True + True + True + False + True + + + False + False + 1 + + + + + False + False + end + 0 + + + + + True + False + DUMMY + + + False + False + 2 + + + + + + EmptyDialogCancelButton + EmptyDialogOkButton + + + + False + 5 + Find & Replace + False + mouse + dialog + + + True + False + 3 + 2 + 5 + + + True + False + Find: + 0 + + + + + + + + + True + False + Replace with: + 0 + + + 1 + 2 + + + + + + + True + True + True + True + True + + + 1 + 2 + + + + + + True + True + + + 1 + 2 + 1 + 2 + + + + + + True + False + 5 + + + True + False + vertical + + + True + True + 0 + + + + + gtk-find + True + True + False + True + + + False + False + 1 + + + + + True + True + False + + + True + False + 0 + 0 + + + True + False + 2 + + + True + False + gtk-find-and-replace + + + False + False + 0 + + + + + True + False + _Replace + True + + + False + False + 1 + + + + + + + + + False + False + 2 + + + + + gtk-cancel + True + True + False + True + + + False + False + 3 + + + + + 2 + 2 + 3 + 5 + + + + + + + False + Matita + + + True + False + + + True + False + vertical + + + True + False + + + True + False + _File + True + + + False + + + True + False + _New + True + + + + + + True + False + _Open... + True + + + + + + True + False + _Save + True + + + + + + True + False + _Save as... + True + + + + + + True + False + + + + + True + False + _Close + True + + + + + + True + False + _Quit + True + + + + + + + + + + True + False + _Edit + True + + + False + + + True + False + False + _Undo + True + + + + + + True + False + False + _Redo + True + + + + + + True + False + + + + + True + False + Cut + True + + + + + + True + False + Copy + True + + + + + + True + False + Paste + True + + + + + + True + False + Paste as pattern + True + + + + + True + False + Paste Unicode as TeX + True + + + + + True + False + Auto-expand TeX Macros + True + True + + + + + True + False + Delete + True + + + + + True + False + + + + + True + False + Select _All + True + + + + + True + False + + + + + True + False + Find and replace... + True + + + + + + True + False + + + + + True + False + Next ligature + True + + + + + + True + False + Edit with e_xternal editor + True + + + + + + + + + True + False + _Script + True + + + False + + + True + False + Execute 1 phrase + True + + + + + + True + False + Retract 1 phrase + True + + + + + + True + False + + + + + True + False + Execute all + True + + + + + + True + False + Retract all + True + + + + + + True + False + + + + + True + False + Execute until cursor + True + + + + + + + + + + True + False + _View + True + + + False + + + True + False + New CIC _browser + True + + + + + + True + False + + + + + True + False + _Fullscreen + True + + + + + + True + False + Natural deduction palette + True + + + + + + True + False + + + + + True + False + Zoom in + True + + + + + + True + False + Zoom out + True + + + + + + True + False + Normal size + True + + + + + + True + False + + + + + True + False + Pretty print notation + True + True + + + + + True + False + Hide coercions + True + True + + + + + True + False + + + + + True + False + Coercions Graph + True + + + + + True + False + Hints database + True + + + + + True + False + Terms grammar + True + + + + + True + False + TeX/UTF-8 table + True + + + + + + + + + True + False + _Debug + True + + + False + + + True + False + + + + + + + + + True + False + _Help + True + + + False + + + True + False + Contents + True + + + + + + True + False + About + True + + + + + + + + + False + False + 0 + + + + + True + False + + + True + True + + + True + False + 2 + + + True + False + top + + + True + False + vertical + + + True + True + + + True + False + vertical + + + True + True + True + + + True + False + Implication (⇒<sub>i</sub>) + True + + + + + True + True + 0 + + + + + True + True + True + + + True + False + Conjunction (∧<sub>i</sub>) + True + + + + + True + True + 1 + + + + + True + True + True + + + True + False + Disjunction left (∨<sub>i-l</sub>) + True + + + + + True + True + 2 + + + + + True + True + True + + + True + False + Disjunction right (∨<sub>i-r</sub>) + True + + + + + True + True + 3 + + + + + True + True + True + + + True + False + Negation (¬<sub>i</sub>) + True + + + + + True + True + 4 + + + + + True + True + True + + + True + False + Top (⊤<sub>i</sub>) + True + + + + + True + True + 5 + + + + + True + True + True + + + True + False + Universal (∀<sub>i</sub>) + True + + + + + True + True + 6 + + + + + True + True + True + + + True + False + Existential (∃<sub>i</sub>) + True + + + + + True + True + 7 + + + + + + + True + False + Introduction rules + + + + + False + True + 0 + + + + + True + True + + + True + False + vertical + + + True + True + True + + + True + False + Implication (⇒<sub>e</sub>) + True + + + + + True + True + 0 + + + + + True + True + True + + + True + False + Conjunction left (∧<sub>e-l</sub>) + True + + + + + True + True + 1 + + + + + True + True + True + + + True + False + Conjunction right (∧<sub>e-r</sub>) + True + + + + + True + True + 2 + + + + + True + True + True + + + True + False + Disjunction (∨<sub>e</sub>) + True + + + + + True + True + 3 + + + + + True + True + True + + + True + False + Negation (¬<sub>e</sub>) + True + + + + + True + True + 4 + + + + + True + True + True + + + True + False + Bottom (⊥<sub>e</sub>) + True + + + + + True + True + 5 + + + + + True + True + True + + + True + False + Universal (∀<sub>e</sub>) + True + + + + + True + True + 6 + + + + + True + True + True + + + True + False + Existential (∃<sub>e</sub>) + True + + + + + True + True + 7 + + + + + + + True + False + Elimination rules + + + + + False + True + 1 + + + + + True + True + + + True + False + vertical + + + Reduction to Absurdity (RAA) + True + True + True + + + True + True + 0 + + + + + Use lemma (lem) + True + True + True + + + True + True + 1 + + + + + Discharge (discharge) + True + True + True + + + True + True + 2 + + + + + + + True + False + Misc rules + + + + + False + True + 2 + + + + + + + False + True + 0 + + + + + 400 + True + False + vertical + + + True + False + + + True + False + both + + + True + False + + + True + True + False + Retract all + none + + + True + False + gtk-goto-top + + + + + + + False + False + + + + + True + False + + + True + True + False + Retract 1 phrase + none + + + True + False + gtk-go-up + + + + + + + False + False + + + + + True + False + + + True + True + False + Execute until cursor + none + + + True + False + gtk-jump-to + + + + + + + False + False + + + + + True + False + + + True + True + False + Execute 1 phrase + none + + + True + False + gtk-go-down + + + + + + + False + False + + + + + True + False + + + True + True + False + Execute all + none + + + True + False + gtk-goto-bottom + + + + + + + False + False + + + + + True + True + 0 + + + + + True + False + vertical + both + + + True + False + + + True + True + False + none + + + True + False + gtk-stop + + + + + + + False + False + + + + + False + True + 1 + + + + + False + False + 0 + + + + + True + True + True + + + True + True + 1 + + + + + True + True + 1 + + + + + False + True + + + + + 250 + 500 + True + True + 380 + + + True + True + True + + + False + True + + + + + True + False + + + True + True + never + in + + + True + True + False + char + False + + + + + True + True + 0 + + + + + True + True + + + + + True + True + + + + + True + True + 0 + + + + + True + True + 1 + + + + + True + False + + + True + False + + + True + True + 0 + + + + + True + False + False + + + True + False + gtk-missing-image + + + + + True + False + label14 + + + False + + + + + True + False + gtk-missing-image + + + 1 + + + + + True + False + label15 + + + 1 + False + + + + + True + False + gtk-missing-image + + + 2 + + + + + True + False + label16 + + + 2 + False + + + + + False + True + 1 + + + + + False + False + 2 + + + + + + + + + False + DUMMY + dialog + + + True + False + vertical + + + True + False + end + + + gtk-cancel + True + True + True + False + True + + + False + False + 0 + + + + + gtk-ok + True + True + True + False + True + + + False + False + 1 + + + + + False + False + end + 0 + + + + + True + False + DUMMY + + + False + False + 2 + + + + + True + True + in + + + True + True + + + + + False + True + 3 + + + + + + TextDialogCancelButton + TextDialogOkButton + + + + 280 + False + Uri choice + True + center + dialog + + + True + False + vertical + 4 + + + True + False + end + + + gtk-cancel + True + True + True + False + True + + + False + False + 0 + + + + + True + True + True + False + + + True + False + 0 + 0 + + + True + False + 2 + + + True + False + gtk-index + + + False + False + 0 + + + + + True + False + Try _Selected + True + + + False + False + 1 + + + + + + + + + False + False + 1 + + + + + Try Constants + True + False + True + True + False + True + + + False + False + 2 + + + + + gtk-copy + True + True + False + True + + + False + False + 3 + + + + + True + True + True + False + + + True + False + 0 + 0 + + + True + False + 2 + + + True + False + gtk-ok + + + False + False + 0 + + + + + True + False + bla bla bla + True + + + False + False + 1 + + + + + + + + + False + False + 4 + + + + + gtk-go-forward + True + True + True + False + True + + + False + False + 5 + + + + + False + False + end + 0 + + + + + True + False + vertical + 3 + + + True + False + some informative message here ... + + + False + False + 0 + + + + + 400 + True + True + + + True + True + False + + + + + + + + True + True + 1 + + + + + True + False + + + True + False + URI: + + + False + False + 0 + + + + + True + True + + + True + True + 1 + + + + + False + True + 2 + + + + + False + True + 2 + + + + + + UriChoiceAbortButton + + + diff --git a/matita/matita/matitaGtkMisc.ml b/matita/matita/matitaGtkMisc.ml index aaf297da2..202270430 100644 --- a/matita/matita/matitaGtkMisc.ml +++ b/matita/matita/matitaGtkMisc.ml @@ -254,16 +254,16 @@ class type gui = let popup_message ~title ~message ~buttons ~callback ?(message_type=`QUESTION) ?parent ?(use_markup=true) - ?(destroy_with_parent=true) ?(allow_grow=false) ?(allow_shrink=false) - ?icon ?(modal=true) ?(resizable=false) ?screen ?type_hint - ?(position=`CENTER_ON_PARENT) ?wm_name ?wm_class ?border_width ?width + ?(destroy_with_parent=true) ?icon ?(modal=true) ?(resizable=false) + ?screen ?type_hint + ?(position=`CENTER_ON_PARENT) ?wmclass ?border_width ?width ?height ?(show=true) () = let m = GWindow.message_dialog ~message ~use_markup ~message_type ~buttons ?parent ~destroy_with_parent - ~title ~allow_grow ~allow_shrink ?icon ~modal ~resizable ?screen - ?type_hint ~position ?wm_name ?wm_class ?border_width ?width ?height + ~title ?icon ~modal ~resizable ?screen + ?type_hint ~position ?wmclass ?border_width ?width ?height ~show () in ignore(m#connect#response @@ -275,17 +275,17 @@ let popup_message let popup_message_lowlevel ~title ~message ?(no_separator=true) ~callback ~message_type ~buttons - ?parent ?(destroy_with_parent=true) ?(allow_grow=false) ?(allow_shrink=false) + ?parent ?(destroy_with_parent=true) ?icon ?(modal=true) ?(resizable=false) ?screen ?type_hint - ?(position=`CENTER_ON_PARENT) ?wm_name ?wm_class ?border_width ?width + ?(position=`CENTER_ON_PARENT) ?wmclass ?border_width ?width ?height ?(show=true) () = let m = GWindow.dialog ~no_separator ?parent ~destroy_with_parent - ~title ~allow_grow ~allow_shrink ?icon ~modal ~resizable ?screen - ?type_hint ~position ?wm_name ?wm_class ?border_width ?width ?height + ~title ?icon ~modal ~resizable ?screen + ?type_hint ~position ?wmclass ?border_width ?width ?height ~show:false () in let stock = @@ -415,7 +415,7 @@ let escape_pango_markup text = let matita_lang = let source_language_manager = - GSourceView2.source_language_manager ~default:true in + GSourceView3.source_language_manager ~default:true in source_language_manager#set_search_path (BuildTimeConf.runtime_base_dir :: source_language_manager#search_path); diff --git a/matita/matita/matitaGtkMisc.mli b/matita/matita/matitaGtkMisc.mli index 05a724136..cf4ce93a9 100644 --- a/matita/matita/matitaGtkMisc.mli +++ b/matita/matita/matitaGtkMisc.mli @@ -151,4 +151,4 @@ val utf8_string_length: string -> int val escape_pango_markup: string -> string -val matita_lang: GSourceView2.source_language +val matita_lang: GSourceView3.source_language diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index 94e3e751d..d8de328ef 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -255,7 +255,7 @@ class interpErrorModel = exception UseLibrary;; let interactive_error_interp ~all_passes - (source_buffer:GSourceView2.source_buffer) notify_exn offset errorll filename + (source_buffer:GSourceView3.source_buffer) notify_exn offset errorll filename = (* hook to save a script for each disambiguation error *) if false then @@ -409,7 +409,6 @@ class gui () = let main = new mainWin () in let sequents_viewer = MatitaMathView.sequentsViewer_instance main#sequentsNotebook in - let fileSel = new fileSelectionWin () in let findRepl = new findReplWin () in let keyBindingBoxes = (* event boxes which should receive global key events *) [ main#mainWinEventBox ] @@ -517,16 +516,10 @@ class gui () = ~callback:(fun _ -> hide_find_Repl ();true)); connect_menu_item main#undoMenuItem (fun () -> (MatitaScript.current ())#safe_undo); -(*CSC: XXX - ignore(source_view#source_buffer#connect#can_undo - ~callback:main#undoMenuItem#misc#set_sensitive); -*) main#undoMenuItem#misc#set_sensitive true; + main#undoMenuItem#misc#set_sensitive false; connect_menu_item main#redoMenuItem (fun () -> (MatitaScript.current ())#safe_redo); -(*CSC: XXX - ignore(source_view#source_buffer#connect#can_redo - ~callback:main#redoMenuItem#misc#set_sensitive); -*) main#redoMenuItem#misc#set_sensitive true; + main#redoMenuItem#misc#set_sensitive false; connect_menu_item main#editMenu (fun () -> main#copyMenuItem#misc#set_sensitive (MatitaScript.current ())#canCopy; @@ -573,7 +566,7 @@ class gui () = GtkThread.sync (fun () -> ()) () in let worker_thread = ref None in - let notify_exn (source_view : GSourceView2.source_view) exn = + let notify_exn (source_view : GSourceView3.source_view) exn = let floc, msg = MatitaExcPp.to_string exn in begin match floc with @@ -666,32 +659,6 @@ class gui () = with exc -> script#source_view#misc#grab_focus (); raise exc in - (* file selection win *) - ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true)); - ignore (fileSel#fileSelectionWin#connect#response (fun event -> - let return r = - chosen_file <- r; - fileSel#fileSelectionWin#misc#hide (); - GMain.Main.quit () - in - match event with - | `OK -> - let fname = fileSel#fileSelectionWin#filename in - if Sys.file_exists fname then - begin - if HExtlib.is_regular fname && not (_only_directory) then - return (Some fname) - else if _only_directory && HExtlib.is_dir fname then - return (Some fname) - end - else - begin - if _ok_not_exists then - return (Some fname) - end - | `CANCEL -> return None - | `HELP -> () - | `DELETE_EVENT -> return None)); (* menus *) List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem ]; (* console *) @@ -875,6 +842,10 @@ class gui () = current_page <- page; let script = MatitaScript.at_page page in script#activate; + main#undoMenuItem#misc#set_sensitive + script#source_view#source_buffer#can_undo ; + main#redoMenuItem#misc#set_sensitive + script#source_view#source_buffer#can_redo ; main#saveMenuItem#misc#set_sensitive script#has_name)) method private externalEditor () = @@ -1045,7 +1016,6 @@ class gui () = self#main#saveMenuItem#misc#set_sensitive true method private console = console - method private fileSel = fileSel method private findRepl = findRepl method main = main @@ -1060,20 +1030,46 @@ class gui () = (fun _ -> callback ();true)); self#addKeyBinding GdkKeysyms._q callback + method private chooseFileOrDir ok_not_exists only_directory = + let fileSel = GWindow.file_chooser_dialog + ~action:`OPEN + ~title:"Select file" + ~modal:true + ~type_hint:`DIALOG + ~position:`CENTER + () in + fileSel#add_select_button_stock `OPEN `OK; + fileSel#add_button_stock `CANCEL `CANCEL; + ignore (fileSel#set_current_folder(Sys.getcwd ())) ; + let res = + let rec aux () = + match fileSel#run () with + | `OK -> + (match fileSel#filename with + None -> aux () + | Some fname -> + if Sys.file_exists fname then + begin + if HExtlib.is_regular fname && not (only_directory) then + Some fname + else if only_directory && HExtlib.is_dir fname then + Some fname + else + aux () + end + else if ok_not_exists then Some fname else aux ()) + | `CANCEL -> None + | `DELETE_EVENT -> None in + aux () in + fileSel#destroy () ; + res + method private chooseFile ?(ok_not_exists = false) () = - _ok_not_exists <- ok_not_exists; - _only_directory <- false; - fileSel#fileSelectionWin#show (); - GtkThread.main (); - chosen_file + self#chooseFileOrDir ok_not_exists false method private chooseDir ?(ok_not_exists = false) () = - _ok_not_exists <- ok_not_exists; - _only_directory <- true; - fileSel#fileSelectionWin#show (); - GtkThread.main (); (* we should check that this is a directory *) - chosen_file + self#chooseFileOrDir ok_not_exists true end @@ -1269,6 +1265,4 @@ let _ = interactive_uri_choice ~selection_mode ?ok_label:ok ~title ~msg ()); Disambiguate.set_choose_interp_callback (interactive_interp_choice ()); (* gtk initialization *) - GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *) - ignore (GMain.Main.init ()) - + GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file (* loads gtk rc *) diff --git a/matita/matita/matitaGuiInit.ml b/matita/matita/matitaGuiInit.ml new file mode 100644 index 000000000..be9d65abf --- /dev/null +++ b/matita/matita/matitaGuiInit.ml @@ -0,0 +1 @@ +ignore (GMain.Main.init ()) diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index ea9683e18..390257422 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -242,12 +242,12 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in - let gui = MatitaMisc.get_gui () in + let _gui = MatitaMisc.get_gui () in let win = new MatitaGeneratedGui.browserWin () in let _ = win#browserUri#misc#grab_focus () in let gviz = LablGraphviz.graphviz ~packing:win#graphScrolledWin#add () in let searchText = - GSourceView2.source_view ~auto_indent:false ~editable:false () + GSourceView3.source_view ~auto_indent:false ~editable:false () in let _ = win#scrolledwinContent#add (searchText :> GObj.widget); @@ -486,8 +486,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private redraw_gviz ?center_on () = if Sys.command "which dot" = 0 then let tmpfile, oc = Filename.open_temp_file "matita" ".dot" in - let fmt = Format.formatter_of_out_channel oc in - (* MATITA 1.0 MetadataDeps.DepGraph.render fmt gviz_graph;*) + (* MATITA 1.0 let fmt = Format.formatter_of_out_channel oc in + MetadataDeps.DepGraph.render fmt gviz_graph;*) close_out oc; gviz#load_graph_from_file ~gviz_cmd:"tred | dot" tmpfile; (match center_on with diff --git a/matita/matita/matitaMisc.ml b/matita/matita/matitaMisc.ml index fe6fd3557..e612b8803 100644 --- a/matita/matita/matitaMisc.ml +++ b/matita/matita/matitaMisc.ml @@ -78,7 +78,7 @@ class shell_history size = let decr x = let x' = x - 1 in if x' < 0 then size + x' else x' in let incr x = (x + 1) mod size in object (self) - val data = Array.create size "" + val data = Array.make size "" inherit basic_history (0, -1 , -1) @@ -106,7 +106,7 @@ class shell_history size = class ['a] browser_history ?memento size init = object (self) initializer match memento with Some m -> self#load m | _ -> () - val data = Array.create size init + val data = Array.make size init inherit basic_history (0, 0, 0) diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index de78194f0..33296d232 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -251,7 +251,7 @@ let fresh_script_id = *) class script ~(parent:GBin.scrolled_window) ~tab_label () = let source_view = - GSourceView2.source_view + GSourceView3.source_view ~auto_indent:true ~insert_spaces_instead_of_tabs:true ~tab_width:2 ~right_margin_position:80 ~show_right_margin:true @@ -260,6 +260,12 @@ let source_view = () in let buffer = source_view#buffer in let source_buffer = source_view#source_buffer in +let _ = + source_buffer#connect#notify_can_undo + ~callback:(MatitaMisc.get_gui ())#main#undoMenuItem#misc#set_sensitive in +let _ = + source_buffer#connect#notify_can_redo + ~callback:(MatitaMisc.get_gui ())#main#redoMenuItem#misc#set_sensitive in let similarsymbols_tag_name = "similarsymbolos" in let similarsymbols_tag = `NAME similarsymbols_tag_name in let initial_statuses current baseuri = @@ -376,16 +382,14 @@ object (self) | _ -> assert false in let add_menu_item = let i = ref 2 in (* last occupied position *) - fun ?label ?stock () -> + fun ~label -> incr i; - GMenu.image_menu_item ?label ?stock ~packing:(menu#insert ~pos:!i) - () - in - let copy = add_menu_item ~stock:`COPY () in - let cut = add_menu_item ~stock:`CUT () in - let delete = add_menu_item ~stock:`DELETE () in - let paste = add_menu_item ~stock:`PASTE () in - let paste_pattern = add_menu_item ~label:"Paste as pattern" () in + GMenu.menu_item ~label ~packing:(menu#insert ~pos:!i) () in + let copy = add_menu_item ~label:"Copy" in + let cut = add_menu_item ~label:"Cut" in + let delete = add_menu_item ~label:"Delete" in + let paste = add_menu_item ~label:"Paste" in + let paste_pattern = add_menu_item ~label:"Paste as pattern" in copy#misc#set_sensitive self#canCopy; cut#misc#set_sensitive self#canCut; delete#misc#set_sensitive self#canDelete; @@ -397,24 +401,22 @@ object (self) MatitaGtkMisc.connect_menu_item paste self#paste; MatitaGtkMisc.connect_menu_item paste_pattern self#pastePattern; let new_undoMenuItem = - GMenu.image_menu_item - ~image:(GMisc.image ~stock:`UNDO ()) + GMenu.menu_item ~use_mnemonic:true ~label:"_Undo" ~packing:(menu#insert ~pos:0) () in new_undoMenuItem#misc#set_sensitive - (undoMenuItem#misc#get_flag `SENSITIVE); + undoMenuItem#misc#sensitive; menu#remove (undoMenuItem :> GMenu.menu_item); MatitaGtkMisc.connect_menu_item new_undoMenuItem (fun () -> self#safe_undo); let new_redoMenuItem = - GMenu.image_menu_item - ~image:(GMisc.image ~stock:`REDO ()) + GMenu.menu_item ~use_mnemonic:true ~label:"_Redo" ~packing:(menu#insert ~pos:1) () in new_redoMenuItem#misc#set_sensitive - (redoMenuItem#misc#get_flag `SENSITIVE); + redoMenuItem#misc#sensitive; menu#remove (redoMenuItem :> GMenu.menu_item); MatitaGtkMisc.connect_menu_item new_redoMenuItem (fun () -> self#safe_redo))); diff --git a/matita/matita/matitaScript.mli b/matita/matita/matitaScript.mli index 9958170d9..ca4b2f86d 100644 --- a/matita/matita/matitaScript.mli +++ b/matita/matita/matitaScript.mli @@ -91,7 +91,7 @@ object (** misc *) method clean_dirty_lock: unit method set_star: bool -> unit - method source_view: GSourceView2.source_view + method source_view: GSourceView3.source_view method has_parent: GObj.widget -> bool (* debug *)