On-going porting to lablgtk3

diff --git a/matita/.merlin b/matita/.merlin
new file mode 100644 (file)
index 0000000..92f60a6
--- /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 f9540fa62e0bb230e1d8bbd0b43eea407aa85e08..0e361298efce8ce8fa94a11eec55aefe30cc9ae8 100644 (file)
--- 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 91bfdab4c0c5c3c396f523505daa5b1eaa4f0f5c..c415c72b00fba8fe64ba4a4abaee39f593217d23 100644 (file)
--- 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 9c0b365c6a3ee363406a84761e14ee85ce710069..7bb00ba9b9ba6f280bb4ebbbe066b02343b3a08b 100644 (file)
--- 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 211b4fc51200e2b3cf63db3bf38852b77c370dda..4deb6e591a8c9b1118318f7a7264800d533fbece 100644 (file)
--- 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 655ffbe8f766f828ae20571cf6c76207aa250231..1f4ede959fdfff29a0a9aab3121673d5512883a8 100644 (file)
--- 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 1f1711ae7f14eaf50a6f86c6fc91f58a0c7ce4a1..735bea7f72c4ccf1beef11818a346a3d4c3d6e6a 100644 (file)
--- 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 12de49274a4db6fba23ff7191d8503ed1e943560..e7b0a3bc74142a75bb82718931527b2b33db82e2 100644 (file)
--- 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 8871a35df0cc30f3bf1a4e27aacd9216c9097dd0..5761010531eca5fe6a0b40c57eee94c0d2a8daa7 100644 (file)
--- 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 cb4976e7d42cebf853748145e98ff0c3b17669b5..c61977894196571ed0dcd0f19653c5dfb2414342 100644 (file)
--- 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 1d016d277ad431861b42fafb78ffdd2011480674..7c2b605861ee7340a4908ed5d3085ccbc0a7d401 100644 (file)
--- 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 f7dffd0663b45f9437cf2a1aedcc4a36ab57fed5..d67dceff1120141ae0a7d78869c40b268962f99e 100644 (file)
--- 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 571479d78e1c949ff569fb202a1a45d96f4428c4..0f44f07d590c083fa183dc969cf356175517a7aa 100644 (file)
--- 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 5dabb8012003194da1d473cc5a561e1d99bf65d2..4a1ca42e9e7b83203739006eb1df032ce7c8629d 100644 (file)
--- 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 696b4588179e989a2ae83a739c57852e3d51d8f6..e6d4942c67b319e5e52866b737ef24ee4091860e 100644 (file)
--- 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 e0e6dac9c2dcb31f52f80b9b237789c528f048cf..752b0d88d5ca9ccf9f59da28b6578d37e2a58763 100644 (file)
--- 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 164153916cd8f45dd309cec10d7035c3c51143ec..3bf2dfa6259b4dc86b613f1a3f70b30f6928809e 100644 (file)
--- 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 27ecf93835014baa578b3cd07a7cb09b8cb5a687..6f2769b943d3b17c0eaa88d03ff693cda70b64e2 100644 (file)
--- 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 ed934897fdbd39b817c5b6303e596f74dff221d2..d1b4c37162663daab85eee7845f39b2422456992 100644 (file)
--- 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 df8d6d6357841ca9eecfae3246d3df739c1c1f16..01e2f5b1ef6d52b1677f749f6a30ec2eb6ed65db 100644 (file)
--- 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 d5eef6bc06265d73f5d3443041b60c587a92931f..79fd839b24f42bc72c2f7a9221dfa9fc047acb37 100644 (file)
--- 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 03f5f9a002277b547522f2e78ba6bf18a21afeea..968d8ffe9355dad2b602be5a4861ee71b475fabb 100644 (file)
--- 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 f68562c2037ee23072d29082c1c129b266af8144..130f7ebdfc10c3c818a6939d5a71e2a1f0a24257 100644 (file)
--- 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 12261145e6bafdc77288daf0a4eb1ed463bd909a..18b7086f513b93da9380c01996fca8d6c0dcd6de 100644 (file)
--- 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 16e1dcf8edade0d71a2481812957a86b8d18c2f8..13791fbad834173a4e927266ba84dcb079f143d6 100644 (file)
--- 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 fe2e99a30a19e52306717451f3e19f28c3269e36..5b05077847c163d3e2d4080466d09e98b971641a 100644 (file)
--- 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 0ca566cc3df4f30d44c53df1c8be3fa03b235eb2..2e382f43417ba985ac8e13da8f812b90575bf1e4 100644 (file)
--- 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 f22e02a7eaa1da016bc202e3afa4793578eec86a..398df307ed7202cadf92ecc843dd3d7b89a165ef 100644 (file)
--- 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 07d53f5dd0b86ddb9d895e15e2c8914d08d5ceac..a571a865c12712184f2df7cb39b8afb4191c4cf5 100644 (file)
--- 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 6e58a4ca97e3980902a3a626518ab1b8284b8b2c..5f4f1cc562e40087cacaebc42ee367dc784ebae6 100644 (file)
--- 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 dab8738901678689b5c7753b5a95b2e45cf09bc4..d8295760aff118a07e4066718ff8146fb64f0228 100644 (file)
--- 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 c8999df5a2a69629233c9ad4d8ff3f228bd7f33f..e8ca8210ee825eaece6fe84e2aea51b7174d36ad 100644 (file)
--- 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 f282104465c4bc6d90927ebb77b2a2fe5e48e67f..67113e67f7af0c0d4e8e6ae696d91d217f620df6 100644 (file)
--- 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 08b1bb76f893320db7ca6db238bfacb0c16634c2..43037aac01c746102444e80f69dddb47db6b12bd 100644 (file)
--- 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 98ac1d844e00cb9bd07f41a86482f326bdaf4fb4..24f371ca742c7b4096f789b860086f44071a5f11 100644 (file)
--- 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 8ee8dbbec0891bf4392eaef92a3ed399c547a59a..d68336af1a35a681ba34e0177059c71c6f4380c3 100644 (file)
--- 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 36a5438084a6137a7f9158f4fc45a2e82c40d60d..fd3f626b9b5ccd97b800d84a81bba82e49aa134c 100644 (file)
--- 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 0e3a4bcc24a91fbb447869ce8bdbebe64593e076..9696fa4bc84102cb953792f8ee6521747805d1ed 100644 (file)
--- 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 4f57e124227b398d68fc88e2078be5a9796740a1..b809068f54e3130ec48cf617c45b40f30d24d2ad 100644 (file)
--- 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 0670278bea925f9bf05a9eb11658c633d43775a6..36f787c66b7e7e3ccb096dd46532ba1f8dfb0634 100644 (file)
--- 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 27186142894d2fef684349d97626d42049016b21..e6ef084730932f0530148998f1fdc74b9013eb4f 100644 (file)
--- 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 5c7d0715ae4df145104d4cd4a5db2d7384bd1328..6de02fb28dab99aba2381388f0d91cd8a86b39f1 100644 (file)
--- 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 caf0f82ff4c7a682ff9f25485f8a312c7da85413..210920abe280e144ba9e1f864479bbb6f90f017d 100644 (file)
--- 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 e06e0055d6da93d8ea9531fceca880048f5d3609..ceb2e1f0df193b19d96ce856e895390c421419e0 100644 (file)
--- 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 (file)
index 0000000..3ea0c2d
--- /dev/null
+++ b/matita/matita/matita.ui
@@ -0,0 +1,2980 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!-- Generated with glade 3.22.1 -->
+<interface>
+  <requires lib="gtk+" version="3.20"/>
+  <object class="GtkWindow" id="AutoWin">
+    <property name="width_request">600</property>
+    <property name="height_request">400</property>
+    <property name="visible">True</property>
+    <property name="can_focus">False</property>
+    <property name="title" translatable="yes">Auto</property>
+    <property name="type_hint">dialog</property>
+    <property name="gravity">south-east</property>
+    <child>
+      <object class="GtkBox" id="vbox17">
+        <property name="visible">True</property>
+        <property name="can_focus">False</property>
+        <property name="orientation">vertical</property>
+        <child>
+          <object class="GtkBox" id="hbox30">
+            <property name="visible">True</property>
+            <property name="can_focus">False</property>
+            <property name="spacing">2</property>
+            <child>
+              <object class="GtkScrolledWindow" id="scrolledwindowAREA">
+                <property name="visible">True</property>
+                <property name="can_focus">True</property>
+                <property name="shadow_type">in</property>
+                <child>
+                  <object class="GtkViewport" id="viewportAREA">
+                    <property name="visible">True</property>
+                    <property name="can_focus">False</property>
+                    <child>
+                      <object class="GtkTable" id="table">
+                        <property name="visible">True</property>
+                        <property name="can_focus">False</property>
+                        <property name="n_rows">3</property>
+                        <property name="n_columns">3</property>
+                      </object>
+                    </child>
+                  </object>
+                </child>
+              </object>
+              <packing>
+                <property name="expand">True</property>
+                <property name="fill">True</property>
+                <property name="position">0</property>
+              </packing>
+            </child>
+            <child>
+              <object class="GtkBox" id="vbox18">
+                <property name="visible">True</property>
+                <property name="can_focus">False</property>
+                <property name="orientation">vertical</property>
+                <child>
+                  <object class="GtkButton" id="buttonUP">
+                    <property name="visible">True</property>
+                    <property name="can_focus">True</property>
+                    <property name="receives_default">False</property>
+                    <child>
+                      <object class="GtkAlignment" id="alignment19">
+                        <property name="visible">True</property>
+                        <property name="can_focus">False</property>
+                        <property name="xscale">0</property>
+                        <property name="yscale">0</property>
+                        <child>
+                          <object class="GtkBox" id="hbox31">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="spacing">2</property>
+                            <child>
+                              <object class="GtkImage" id="image1066">
+                                <property name="visible">True</property>
+                                <property name="can_focus">False</property>
+                                <property name="stock">gtk-go-up</property>
+                              </object>
+                              <packing>
+                                <property name="expand">False</property>
+                                <property name="fill">False</property>
+                                <property name="position">0</property>
+                              </packing>
+                            </child>
+                            <child>
+                              <object class="GtkLabel" id="label30">
+                                <property name="visible">True</property>
+                                <property name="can_focus">False</property>
+                                <property name="use_underline">True</property>
+                              </object>
+                              <packing>
+                                <property name="expand">False</property>
+                                <property name="fill">False</property>
+                                <property name="position">1</property>
+                              </packing>
+                            </child>
+                          </object>
+                        </child>
+                      </object>
+                    </child>
+                  </object>
+                  <packing>
+                    <property name="expand">True</property>
+                    <property name="fill">True</property>
+                    <property name="position">0</property>
+                  </packing>
+                </child>
+                <child>
+                  <object class="GtkButton" id="buttonDOWN">
+                    <property name="visible">True</property>
+                    <property name="can_focus">True</property>
+                    <property name="receives_default">False</property>
+                    <child>
+                      <object class="GtkImage" id="image1065">
+                        <property name="visible">True</property>
+                        <property name="can_focus">False</property>
+                        <property name="stock">gtk-go-down</property>
+                      </object>
+                    </child>
+                  </object>
+                  <packing>
+                    <property name="expand">True</property>
+                    <property name="fill">True</property>
+                    <property name="position">1</property>
+                  </packing>
+                </child>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">1</property>
+              </packing>
+            </child>
+          </object>
+          <packing>
+            <property name="expand">True</property>
+            <property name="fill">True</property>
+            <property name="position">0</property>
+          </packing>
+        </child>
+        <child>
+          <object class="GtkHSeparator" id="hseparator3">
+            <property name="visible">True</property>
+            <property name="can_focus">False</property>
+          </object>
+          <packing>
+            <property name="expand">False</property>
+            <property name="fill">True</property>
+            <property name="padding">3</property>
+            <property name="position">1</property>
+          </packing>
+        </child>
+        <child>
+          <object class="GtkBox" id="hbox32">
+            <property name="visible">True</property>
+            <property name="can_focus">False</property>
+            <child>
+              <object class="GtkLabel" id="labelLAST">
+                <property name="visible">True</property>
+                <property name="can_focus">False</property>
+                <property name="label" translatable="yes">Last:</property>
+                <property name="xalign">0</property>
+              </object>
+              <packing>
+                <property name="expand">True</property>
+                <property name="fill">True</property>
+                <property name="position">0</property>
+              </packing>
+            </child>
+            <child>
+              <object class="GtkHButtonBox" id="hbuttonbox3">
+                <property name="visible">True</property>
+                <property name="can_focus">False</property>
+                <property name="border_width">4</property>
+                <property name="spacing">4</property>
+                <property name="layout_style">end</property>
+                <child>
+                  <object class="GtkButton" id="buttonPAUSE">
+                    <property name="label">gtk-media-pause</property>
+                    <property name="visible">True</property>
+                    <property name="can_focus">True</property>
+                    <property name="can_default">True</property>
+                    <property name="receives_default">False</property>
+                    <property name="use_stock">True</property>
+                  </object>
+                  <packing>
+                    <property name="expand">False</property>
+                    <property name="fill">False</property>
+                    <property name="position">0</property>
+                  </packing>
+                </child>
+                <child>
+                  <object class="GtkButton" id="buttonPLAY">
+                    <property name="label">gtk-media-play</property>
+                    <property name="visible">True</property>
+                    <property name="can_focus">True</property>
+                    <property name="can_default">True</property>
+                    <property name="receives_default">False</property>
+                    <property name="use_stock">True</property>
+                  </object>
+                  <packing>
+                    <property name="expand">False</property>
+                    <property name="fill">False</property>
+                    <property name="position">1</property>
+                  </packing>
+                </child>
+                <child>
+                  <object class="GtkButton" id="buttonNEXT">
+                    <property name="label">gtk-media-next</property>
+                    <property name="visible">True</property>
+                    <property name="can_focus">True</property>
+                    <property name="can_default">True</property>
+                    <property name="receives_default">False</property>
+                    <property name="use_stock">True</property>
+                  </object>
+                  <packing>
+                    <property name="expand">False</property>
+                    <property name="fill">False</property>
+                    <property name="position">2</property>
+                  </packing>
+                </child>
+                <child>
+                  <object class="GtkButton" id="buttonCLOSE">
+                    <property name="label">gtk-close</property>
+                    <property name="visible">True</property>
+                    <property name="can_focus">True</property>
+                    <property name="can_default">True</property>
+                    <property name="receives_default">False</property>
+                    <property name="use_stock">True</property>
+                  </object>
+                  <packing>
+                    <property name="expand">False</property>
+                    <property name="fill">False</property>
+                    <property name="position">3</property>
+                  </packing>
+                </child>
+              </object>
+              <packing>
+                <property name="expand">True</property>
+                <property name="fill">True</property>
+                <property name="position">1</property>
+              </packing>
+            </child>
+          </object>
+          <packing>
+            <property name="expand">False</property>
+            <property name="fill">True</property>
+            <property name="position">2</property>
+          </packing>
+        </child>
+      </object>
+    </child>
+  </object>
+  <object class="GtkWindow" id="BrowserWin">
+    <property name="width_request">500</property>
+    <property name="height_request">480</property>
+    <property name="visible">True</property>
+    <property name="can_focus">False</property>
+    <property name="title" translatable="yes">Cic browser</property>
+    <property name="window_position">center-on-parent</property>
+    <property name="default_width">500</property>
+    <property name="default_height">480</property>
+    <property name="destroy_with_parent">True</property>
+    <child>
+      <object class="GtkEventBox" id="BrowserWinEventBox">
+        <property name="visible">True</property>
+        <property name="can_focus">False</property>
+        <child>
+          <object class="GtkBox" id="BrowserVBox">
+            <property name="visible">True</property>
+            <property name="can_focus">False</property>
+            <property name="orientation">vertical</property>
+            <child>
+              <object class="GtkMenuBar" id="menubar2">
+                <property name="visible">True</property>
+                <property name="can_focus">False</property>
+                <child>
+                  <object class="GtkMenuItem" id="BrowserFileMenu">
+                    <property name="visible">True</property>
+                    <property name="can_focus">False</property>
+                    <property name="label" translatable="yes">_File</property>
+                    <property name="use_underline">True</property>
+                    <child type="submenu">
+                      <object class="GtkMenu" id="BrowserFileMenu_menu">
+                        <property name="can_focus">False</property>
+                        <child>
+                          <object class="GtkMenuItem" id="BrowserNewMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">_New</property>
+                            <property name="use_underline">True</property>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="BrowserUrlMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label" translatable="yes">Open _Location ...</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="L" signal="activate" modifiers="GDK_CONTROL_MASK"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkSeparatorMenuItem" id="separatormenuitem1">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="BrowserCloseMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">_Quit</property>
+                            <property name="use_underline">True</property>
+                          </object>
+                        </child>
+                      </object>
+                    </child>
+                  </object>
+                </child>
+                <child>
+                  <object class="GtkMenuItem" id="BrowserEditMenu">
+                    <property name="visible">True</property>
+                    <property name="can_focus">False</property>
+                    <property name="label" translatable="yes">_Edit</property>
+                    <property name="use_underline">True</property>
+                    <child type="submenu">
+                      <object class="GtkMenu" id="BrowserEditMenu_menu">
+                        <property name="can_focus">False</property>
+                        <child>
+                          <object class="GtkMenuItem" id="BrowserCopyMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">_Copy</property>
+                            <property name="use_underline">True</property>
+                          </object>
+                        </child>
+                      </object>
+                    </child>
+                  </object>
+                </child>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">0</property>
+              </packing>
+            </child>
+            <child>
+              <object class="GtkFrame" id="frame2">
+                <property name="visible">True</property>
+                <property name="can_focus">False</property>
+                <property name="label_xalign">0</property>
+                <property name="label_yalign">0</property>
+                <property name="shadow_type">none</property>
+                <child>
+                  <object class="GtkBox" id="BrowserHBox">
+                    <property name="visible">True</property>
+                    <property name="can_focus">False</property>
+                    <child>
+                      <object class="GtkButton" id="BrowserNewButton">
+                        <property name="visible">True</property>
+                        <property name="can_focus">True</property>
+                        <property name="receives_default">False</property>
+                        <property name="relief">none</property>
+                        <child>
+                          <object class="GtkImage" id="image303">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="stock">gtk-new</property>
+                          </object>
+                        </child>
+                      </object>
+                      <packing>
+                        <property name="expand">False</property>
+                        <property name="fill">False</property>
+                        <property name="position">0</property>
+                      </packing>
+                    </child>
+                    <child>
+                      <object class="GtkButton" id="BrowserBackButton">
+                        <property name="visible">True</property>
+                        <property name="can_focus">True</property>
+                        <property name="receives_default">False</property>
+                        <property name="relief">none</property>
+                        <child>
+                          <object class="GtkImage" id="image304">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="stock">gtk-go-back</property>
+                          </object>
+                        </child>
+                      </object>
+                      <packing>
+                        <property name="expand">False</property>
+                        <property name="fill">False</property>
+                        <property name="position">1</property>
+                      </packing>
+                    </child>
+                    <child>
+                      <object class="GtkButton" id="BrowserForwardButton">
+                        <property name="visible">True</property>
+                        <property name="can_focus">True</property>
+                        <property name="receives_default">False</property>
+                        <property name="relief">none</property>
+                        <child>
+                          <object class="GtkImage" id="image305">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="stock">gtk-go-forward</property>
+                          </object>
+                        </child>
+                      </object>
+                      <packing>
+                        <property name="expand">False</property>
+                        <property name="fill">False</property>
+                        <property name="position">2</property>
+                      </packing>
+                    </child>
+                    <child>
+                      <object class="GtkButton" id="BrowserRefreshButton">
+                        <property name="visible">True</property>
+                        <property name="can_focus">True</property>
+                        <property name="can_default">True</property>
+                        <property name="receives_default">False</property>
+                        <property name="tooltip_text" translatable="yes">refresh</property>
+                        <property name="relief">none</property>
+                        <child>
+                          <object class="GtkImage" id="image229">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="stock">gtk-refresh</property>
+                          </object>
+                        </child>
+                      </object>
+                      <packing>
+                        <property name="expand">False</property>
+                        <property name="fill">False</property>
+                        <property name="position">3</property>
+                      </packing>
+                    </child>
+                    <child>
+                      <object class="GtkButton" id="BrowserHomeButton">
+                        <property name="visible">True</property>
+                        <property name="can_focus">True</property>
+                        <property name="can_default">True</property>
+                        <property name="receives_default">False</property>
+                        <property name="tooltip_text" translatable="yes">home</property>
+                        <property name="relief">none</property>
+                        <child>
+                          <object class="GtkImage" id="image190">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="stock">gtk-home</property>
+                          </object>
+                        </child>
+                      </object>
+                      <packing>
+                        <property name="expand">False</property>
+                        <property name="fill">False</property>
+                        <property name="position">4</property>
+                      </packing>
+                    </child>
+                    <child>
+                      <object class="GtkImage" id="image301">
+                        <property name="visible">True</property>
+                        <property name="can_focus">False</property>
+                        <property name="stock">gtk-jump-to</property>
+                        <property name="icon_size">2</property>
+                      </object>
+                      <packing>
+                        <property name="expand">False</property>
+                        <property name="fill">False</property>
+                        <property name="padding">3</property>
+                        <property name="position">5</property>
+                      </packing>
+                    </child>
+                    <child>
+                      <object class="GtkBox" id="UriHBox">
+                        <property name="visible">True</property>
+                        <property name="can_focus">False</property>
+                        <child>
+                          <object class="GtkEntry" id="browserUri">
+                            <property name="visible">True</property>
+                            <property name="can_focus">True</property>
+                            <property name="has_focus">True</property>
+                            <property name="invisible_char">●</property>
+                          </object>
+                          <packing>
+                            <property name="expand">True</property>
+                            <property name="fill">True</property>
+                            <property name="position">0</property>
+                          </packing>
+                        </child>
+                      </object>
+                      <packing>
+                        <property name="expand">True</property>
+                        <property name="fill">True</property>
+                        <property name="position">6</property>
+                      </packing>
+                    </child>
+                  </object>
+                </child>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">True</property>
+                <property name="position">1</property>
+              </packing>
+            </child>
+            <child>
+              <object class="GtkNotebook" id="mathOrListNotebook">
+                <property name="visible">True</property>
+                <property name="can_focus">True</property>
+                <child>
+                  <object class="GtkScrolledWindow" id="ScrolledBrowser">
+                    <property name="visible">True</property>
+                    <property name="can_focus">True</property>
+                  </object>
+                </child>
+                <child type="tab">
+                  <object class="GtkLabel" id="mathLabel">
+                    <property name="visible">True</property>
+                    <property name="can_focus">False</property>
+                    <property name="label" translatable="yes">MathView</property>
+                  </object>
+                  <packing>
+                    <property name="tab_fill">False</property>
+                  </packing>
+                </child>
+                <child>
+                  <object class="GtkScrolledWindow" id="scrolledwindow9">
+                    <property name="visible">True</property>
+                    <property name="can_focus">True</property>
+                    <property name="shadow_type">in</property>
+                    <child>
+                      <object class="GtkTreeView" id="whelpResultTreeview">
+                        <property name="visible">True</property>
+                        <property name="can_focus">True</property>
+                        <property name="headers_visible">False</property>
+                        <child internal-child="selection">
+                          <object class="GtkTreeSelection"/>
+                        </child>
+                      </object>
+                    </child>
+                  </object>
+                  <packing>
+                    <property name="position">1</property>
+                  </packing>
+                </child>
+                <child type="tab">
+                  <object class="GtkLabel" id="WhelpResult">
+                    <property name="visible">True</property>
+                    <property name="can_focus">False</property>
+                    <property name="label" translatable="yes">WhelpResult</property>
+                  </object>
+                  <packing>
+                    <property name="position">1</property>
+                    <property name="tab_fill">False</property>
+                  </packing>
+                </child>
+                <child>
+                  <object class="GtkScrolledWindow" id="scrolledwindow11">
+                    <property name="visible">True</property>
+                    <property name="can_focus">True</property>
+                    <child>
+                      <object class="GtkViewport" id="viewport2">
+                        <property name="visible">True</property>
+                        <property name="can_focus">False</property>
+                        <property name="shadow_type">none</property>
+                        <child>
+                          <object class="GtkImage" id="BrowserImage">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="stock">gtk-missing-image</property>
+                          </object>
+                        </child>
+                      </object>
+                    </child>
+                  </object>
+                  <packing>
+                    <property name="position">2</property>
+                  </packing>
+                </child>
+                <child type="tab">
+                  <object class="GtkLabel" id="EasterEggLabel">
+                    <property name="visible">True</property>
+                    <property name="can_focus">False</property>
+                    <property name="label" translatable="yes">WhelpEasterEgg</property>
+                  </object>
+                  <packing>
+                    <property name="position">2</property>
+                    <property name="tab_fill">False</property>
+                  </packing>
+                </child>
+                <child>
+                  <object class="GtkScrolledWindow" id="GraphScrolledWin">
+                    <property name="visible">True</property>
+                    <property name="can_focus">True</property>
+                  </object>
+                  <packing>
+                    <property name="position">3</property>
+                  </packing>
+                </child>
+                <child type="tab">
+                  <object class="GtkLabel" id="label26">
+                    <property name="visible">True</property>
+                    <property name="can_focus">False</property>
+                    <property name="label" translatable="yes">Graph</property>
+                  </object>
+                  <packing>
+                    <property name="position">3</property>
+                    <property name="tab_fill">False</property>
+                  </packing>
+                </child>
+                <child>
+                  <object class="GtkBox" id="vbox20">
+                    <property name="visible">True</property>
+                    <property name="can_focus">False</property>
+                    <property name="orientation">vertical</property>
+                    <child>
+                      <object class="GtkScrolledWindow" id="scrolledwinContent">
+                        <property name="visible">True</property>
+                        <property name="can_focus">True</property>
+                        <property name="border_width">3</property>
+                        <property name="shadow_type">in</property>
+                      </object>
+                      <packing>
+                        <property name="expand">True</property>
+                        <property name="fill">True</property>
+                        <property name="position">0</property>
+                      </packing>
+                    </child>
+                    <child>
+                      <object class="GtkBox" id="hbox35">
+                        <property name="visible">True</property>
+                        <property name="can_focus">False</property>
+                        <property name="border_width">4</property>
+                        <property name="spacing">4</property>
+                        <child>
+                          <object class="GtkBox" id="vbox22">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="orientation">vertical</property>
+                          </object>
+                          <packing>
+                            <property name="expand">True</property>
+                            <property name="fill">True</property>
+                            <property name="position">0</property>
+                          </packing>
+                        </child>
+                        <child>
+                          <object class="GtkEntry" id="entrySearch">
+                            <property name="visible">True</property>
+                            <property name="can_focus">True</property>
+                            <property name="has_focus">True</property>
+                          </object>
+                          <packing>
+                            <property name="expand">True</property>
+                            <property name="fill">True</property>
+                            <property name="position">1</property>
+                          </packing>
+                        </child>
+                        <child>
+                          <object class="GtkButton" id="buttonSearch">
+                            <property name="visible">True</property>
+                            <property name="can_focus">True</property>
+                            <property name="receives_default">False</property>
+                            <child>
+                              <object class="GtkAlignment" id="alignment21">
+                                <property name="visible">True</property>
+                                <property name="can_focus">False</property>
+                                <property name="xscale">0</property>
+                                <property name="yscale">0</property>
+                                <child>
+                                  <object class="GtkBox" id="hbox36">
+                                    <property name="visible">True</property>
+                                    <property name="can_focus">False</property>
+                                    <property name="spacing">2</property>
+                                    <child>
+                                      <object class="GtkImage" id="image1068">
+                                        <property name="visible">True</property>
+                                        <property name="can_focus">False</property>
+                                        <property name="stock">gtk-find</property>
+                                      </object>
+                                      <packing>
+                                        <property name="expand">False</property>
+                                        <property name="fill">False</property>
+                                        <property name="position">0</property>
+                                      </packing>
+                                    </child>
+                                    <child>
+                                      <object class="GtkLabel" id="label32">
+                                        <property name="visible">True</property>
+                                        <property name="can_focus">False</property>
+                                        <property name="label" translatable="yes">Search</property>
+                                        <property name="use_underline">True</property>
+                                      </object>
+                                      <packing>
+                                        <property name="expand">False</property>
+                                        <property name="fill">False</property>
+                                        <property name="position">1</property>
+                                      </packing>
+                                    </child>
+                                  </object>
+                                </child>
+                              </object>
+                            </child>
+                          </object>
+                          <packing>
+                            <property name="expand">False</property>
+                            <property name="fill">False</property>
+                            <property name="position">2</property>
+                          </packing>
+                        </child>
+                      </object>
+                      <packing>
+                        <property name="expand">False</property>
+                        <property name="fill">True</property>
+                        <property name="position">1</property>
+                      </packing>
+                    </child>
+                  </object>
+                  <packing>
+                    <property name="position">4</property>
+                  </packing>
+                </child>
+                <child type="tab">
+                  <object class="GtkLabel" id="SearchText">
+                    <property name="visible">True</property>
+                    <property name="can_focus">False</property>
+                    <property name="label" translatable="yes">SearchText</property>
+                  </object>
+                  <packing>
+                    <property name="position">4</property>
+                    <property name="tab_fill">False</property>
+                  </packing>
+                </child>
+              </object>
+              <packing>
+                <property name="expand">True</property>
+                <property name="fill">True</property>
+                <property name="position">3</property>
+              </packing>
+            </child>
+          </object>
+        </child>
+      </object>
+    </child>
+  </object>
+  <object class="GtkDialog" id="ConfirmationDialog">
+    <property name="can_focus">False</property>
+    <property name="title" translatable="yes">DUMMY</property>
+    <property name="resizable">False</property>
+    <property name="modal">True</property>
+    <property name="window_position">center</property>
+    <property name="type_hint">dialog</property>
+    <child internal-child="vbox">
+      <object class="GtkBox" id="dialog-vbox1">
+        <property name="visible">True</property>
+        <property name="can_focus">False</property>
+        <property name="orientation">vertical</property>
+        <child internal-child="action_area">
+          <object class="GtkButtonBox" id="dialog-action_area1">
+            <property name="visible">True</property>
+            <property name="can_focus">False</property>
+            <property name="layout_style">end</property>
+            <child>
+              <object class="GtkButton" id="ConfirmationDialogCancelButton">
+                <property name="label">gtk-cancel</property>
+                <property name="visible">True</property>
+                <property name="can_focus">True</property>
+                <property name="can_default">True</property>
+                <property name="receives_default">False</property>
+                <property name="use_stock">True</property>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">0</property>
+              </packing>
+            </child>
+            <child>
+              <object class="GtkButton" id="ConfirmationDialogOkButton">
+                <property name="label">gtk-ok</property>
+                <property name="visible">True</property>
+                <property name="can_focus">True</property>
+                <property name="can_default">True</property>
+                <property name="receives_default">False</property>
+                <property name="use_stock">True</property>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">1</property>
+              </packing>
+            </child>
+          </object>
+          <packing>
+            <property name="expand">False</property>
+            <property name="fill">False</property>
+            <property name="pack_type">end</property>
+            <property name="position">0</property>
+          </packing>
+        </child>
+        <child>
+          <object class="GtkLabel" id="ConfirmationDialogLabel">
+            <property name="visible">True</property>
+            <property name="can_focus">False</property>
+            <property name="label" translatable="yes">DUMMY</property>
+            <property name="justify">center</property>
+          </object>
+          <packing>
+            <property name="expand">False</property>
+            <property name="fill">False</property>
+            <property name="position">2</property>
+          </packing>
+        </child>
+      </object>
+    </child>
+    <action-widgets>
+      <action-widget response="-6">ConfirmationDialogCancelButton</action-widget>
+      <action-widget response="-5">ConfirmationDialogOkButton</action-widget>
+    </action-widgets>
+  </object>
+  <object class="GtkDialog" id="DisambiguationErrors">
+    <property name="width_request">450</property>
+    <property name="height_request">400</property>
+    <property name="can_focus">False</property>
+    <property name="title" translatable="yes">title</property>
+    <property name="modal">True</property>
+    <property name="type_hint">dialog</property>
+    <child internal-child="vbox">
+      <object class="GtkBox" id="vbox14">
+        <property name="visible">True</property>
+        <property name="can_focus">False</property>
+        <property name="orientation">vertical</property>
+        <child internal-child="action_area">
+          <object class="GtkButtonBox" id="hbuttonbox2">
+            <property name="visible">True</property>
+            <property name="can_focus">False</property>
+            <property name="layout_style">end</property>
+            <child>
+              <object class="GtkButton" id="button6">
+                <property name="label">gtk-help</property>
+                <property name="visible">True</property>
+                <property name="can_focus">True</property>
+                <property name="can_default">True</property>
+                <property name="receives_default">False</property>
+                <property name="use_stock">True</property>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">0</property>
+              </packing>
+            </child>
+            <child>
+              <object class="GtkButton" id="disambiguationErrorsMoreErrors">
+                <property name="visible">True</property>
+                <property name="can_focus">True</property>
+                <property name="can_default">True</property>
+                <property name="receives_default">False</property>
+                <child>
+                  <object class="GtkAlignment" id="alignment18">
+                    <property name="visible">True</property>
+                    <property name="can_focus">False</property>
+                    <property name="xscale">0</property>
+                    <property name="yscale">0</property>
+                    <child>
+                      <object class="GtkBox" id="hbox29">
+                        <property name="visible">True</property>
+                        <property name="can_focus">False</property>
+                        <property name="spacing">2</property>
+                        <child>
+                          <object class="GtkImage" id="image926">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="stock">gtk-zoom-in</property>
+                          </object>
+                          <packing>
+                            <property name="expand">False</property>
+                            <property name="fill">False</property>
+                            <property name="position">0</property>
+                          </packing>
+                        </child>
+                        <child>
+                          <object class="GtkLabel" id="label28">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">More</property>
+                            <property name="use_underline">True</property>
+                          </object>
+                          <packing>
+                            <property name="expand">False</property>
+                            <property name="fill">False</property>
+                            <property name="position">1</property>
+                          </packing>
+                        </child>
+                      </object>
+                    </child>
+                  </object>
+                </child>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">1</property>
+              </packing>
+            </child>
+            <child>
+              <object class="GtkButton" id="disambiguationErrorsCancelButton">
+                <property name="label">gtk-cancel</property>
+                <property name="visible">True</property>
+                <property name="can_focus">True</property>
+                <property name="can_default">True</property>
+                <property name="has_default">True</property>
+                <property name="receives_default">False</property>
+                <property name="use_stock">True</property>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">2</property>
+              </packing>
+            </child>
+            <child>
+              <object class="GtkButton" id="disambiguationErrorsOkButton">
+                <property name="label">gtk-ok</property>
+                <property name="visible">True</property>
+                <property name="can_focus">True</property>
+                <property name="can_default">True</property>
+                <property name="receives_default">False</property>
+                <property name="use_stock">True</property>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">3</property>
+              </packing>
+            </child>
+          </object>
+          <packing>
+            <property name="expand">False</property>
+            <property name="fill">False</property>
+            <property name="pack_type">end</property>
+            <property name="position">0</property>
+          </packing>
+        </child>
+        <child>
+          <object class="GtkBox" id="vbox15">
+            <property name="visible">True</property>
+            <property name="can_focus">False</property>
+            <property name="orientation">vertical</property>
+            <child>
+              <object class="GtkLabel" id="disambiguationErrorsLabel">
+                <property name="visible">True</property>
+                <property name="can_focus">False</property>
+                <property name="label" translatable="yes">some informative message here ...</property>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">0</property>
+              </packing>
+            </child>
+            <child>
+              <object class="GtkScrolledWindow" id="scrolledwindow12">
+                <property name="visible">True</property>
+                <property name="can_focus">True</property>
+                <property name="shadow_type">in</property>
+                <child>
+                  <object class="GtkTreeView" id="treeview">
+                    <property name="visible">True</property>
+                    <property name="can_focus">True</property>
+                    <property name="headers_visible">False</property>
+                    <child internal-child="selection">
+                      <object class="GtkTreeSelection"/>
+                    </child>
+                  </object>
+                </child>
+              </object>
+              <packing>
+                <property name="expand">True</property>
+                <property name="fill">True</property>
+                <property name="position">1</property>
+              </packing>
+            </child>
+          </object>
+          <packing>
+            <property name="expand">False</property>
+            <property name="fill">True</property>
+            <property name="position">2</property>
+          </packing>
+        </child>
+      </object>
+    </child>
+    <action-widgets>
+      <action-widget response="-11">button6</action-widget>
+      <action-widget response="-6">disambiguationErrorsMoreErrors</action-widget>
+      <action-widget response="-6">disambiguationErrorsCancelButton</action-widget>
+      <action-widget response="-5">disambiguationErrorsOkButton</action-widget>
+    </action-widgets>
+  </object>
+  <object class="GtkDialog" id="EmptyDialog">
+    <property name="visible">True</property>
+    <property name="can_focus">False</property>
+    <property name="title" translatable="yes">DUMMY</property>
+    <property name="type_hint">dialog</property>
+    <child internal-child="vbox">
+      <object class="GtkBox" id="EmptyDialogVBox">
+        <property name="visible">True</property>
+        <property name="can_focus">False</property>
+        <property name="orientation">vertical</property>
+        <child internal-child="action_area">
+          <object class="GtkButtonBox" id="dialog-action_area5">
+            <property name="visible">True</property>
+            <property name="can_focus">False</property>
+            <property name="layout_style">end</property>
+            <child>
+              <object class="GtkButton" id="EmptyDialogCancelButton">
+                <property name="label">gtk-cancel</property>
+                <property name="visible">True</property>
+                <property name="can_focus">True</property>
+                <property name="can_default">True</property>
+                <property name="receives_default">False</property>
+                <property name="use_stock">True</property>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">0</property>
+              </packing>
+            </child>
+            <child>
+              <object class="GtkButton" id="EmptyDialogOkButton">
+                <property name="label">gtk-ok</property>
+                <property name="visible">True</property>
+                <property name="can_focus">True</property>
+                <property name="can_default">True</property>
+                <property name="receives_default">False</property>
+                <property name="use_stock">True</property>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">1</property>
+              </packing>
+            </child>
+          </object>
+          <packing>
+            <property name="expand">False</property>
+            <property name="fill">False</property>
+            <property name="pack_type">end</property>
+            <property name="position">0</property>
+          </packing>
+        </child>
+        <child>
+          <object class="GtkLabel" id="EmptyDialogLabel">
+            <property name="visible">True</property>
+            <property name="can_focus">False</property>
+            <property name="label" translatable="yes">DUMMY</property>
+          </object>
+          <packing>
+            <property name="expand">False</property>
+            <property name="fill">False</property>
+            <property name="position">2</property>
+          </packing>
+        </child>
+      </object>
+    </child>
+    <action-widgets>
+      <action-widget response="-6">EmptyDialogCancelButton</action-widget>
+      <action-widget response="-5">EmptyDialogOkButton</action-widget>
+    </action-widgets>
+  </object>
+  <object class="GtkWindow" id="FindReplWin">
+    <property name="can_focus">False</property>
+    <property name="border_width">5</property>
+    <property name="title" translatable="yes">Find &amp; Replace</property>
+    <property name="resizable">False</property>
+    <property name="window_position">mouse</property>
+    <property name="type_hint">dialog</property>
+    <child>
+      <object class="GtkTable" id="table1">
+        <property name="visible">True</property>
+        <property name="can_focus">False</property>
+        <property name="n_rows">3</property>
+        <property name="n_columns">2</property>
+        <property name="row_spacing">5</property>
+        <child>
+          <object class="GtkLabel" id="label17">
+            <property name="visible">True</property>
+            <property name="can_focus">False</property>
+            <property name="label" translatable="yes">Find:</property>
+            <property name="xalign">0</property>
+          </object>
+          <packing>
+            <property name="x_options"/>
+            <property name="y_options"/>
+          </packing>
+        </child>
+        <child>
+          <object class="GtkLabel" id="label18">
+            <property name="visible">True</property>
+            <property name="can_focus">False</property>
+            <property name="label" translatable="yes">Replace with: </property>
+            <property name="xalign">0</property>
+          </object>
+          <packing>
+            <property name="top_attach">1</property>
+            <property name="bottom_attach">2</property>
+            <property name="x_options"/>
+            <property name="y_options"/>
+          </packing>
+        </child>
+        <child>
+          <object class="GtkEntry" id="findEntry">
+            <property name="visible">True</property>
+            <property name="can_focus">True</property>
+            <property name="has_focus">True</property>
+            <property name="can_default">True</property>
+            <property name="has_default">True</property>
+          </object>
+          <packing>
+            <property name="left_attach">1</property>
+            <property name="right_attach">2</property>
+            <property name="y_options"/>
+          </packing>
+        </child>
+        <child>
+          <object class="GtkEntry" id="replaceEntry">
+            <property name="visible">True</property>
+            <property name="can_focus">True</property>
+          </object>
+          <packing>
+            <property name="left_attach">1</property>
+            <property name="right_attach">2</property>
+            <property name="top_attach">1</property>
+            <property name="bottom_attach">2</property>
+            <property name="y_options"/>
+          </packing>
+        </child>
+        <child>
+          <object class="GtkBox" id="hbox19">
+            <property name="visible">True</property>
+            <property name="can_focus">False</property>
+            <property name="spacing">5</property>
+            <child>
+              <object class="GtkBox" id="vbox9">
+                <property name="visible">True</property>
+                <property name="can_focus">False</property>
+                <property name="orientation">vertical</property>
+              </object>
+              <packing>
+                <property name="expand">True</property>
+                <property name="fill">True</property>
+                <property name="position">0</property>
+              </packing>
+            </child>
+            <child>
+              <object class="GtkButton" id="findButton">
+                <property name="label">gtk-find</property>
+                <property name="visible">True</property>
+                <property name="can_focus">True</property>
+                <property name="receives_default">False</property>
+                <property name="use_stock">True</property>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">1</property>
+              </packing>
+            </child>
+            <child>
+              <object class="GtkButton" id="findReplButton">
+                <property name="visible">True</property>
+                <property name="can_focus">True</property>
+                <property name="receives_default">False</property>
+                <child>
+                  <object class="GtkAlignment" id="alignment13">
+                    <property name="visible">True</property>
+                    <property name="can_focus">False</property>
+                    <property name="xscale">0</property>
+                    <property name="yscale">0</property>
+                    <child>
+                      <object class="GtkBox" id="hbox20">
+                        <property name="visible">True</property>
+                        <property name="can_focus">False</property>
+                        <property name="spacing">2</property>
+                        <child>
+                          <object class="GtkImage" id="image357">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="stock">gtk-find-and-replace</property>
+                          </object>
+                          <packing>
+                            <property name="expand">False</property>
+                            <property name="fill">False</property>
+                            <property name="position">0</property>
+                          </packing>
+                        </child>
+                        <child>
+                          <object class="GtkLabel" id="label19">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">_Replace</property>
+                            <property name="use_underline">True</property>
+                          </object>
+                          <packing>
+                            <property name="expand">False</property>
+                            <property name="fill">False</property>
+                            <property name="position">1</property>
+                          </packing>
+                        </child>
+                      </object>
+                    </child>
+                  </object>
+                </child>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">2</property>
+              </packing>
+            </child>
+            <child>
+              <object class="GtkButton" id="cancelButton">
+                <property name="label">gtk-cancel</property>
+                <property name="visible">True</property>
+                <property name="can_focus">True</property>
+                <property name="receives_default">False</property>
+                <property name="use_stock">True</property>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">3</property>
+              </packing>
+            </child>
+          </object>
+          <packing>
+            <property name="right_attach">2</property>
+            <property name="top_attach">2</property>
+            <property name="bottom_attach">3</property>
+            <property name="y_padding">5</property>
+          </packing>
+        </child>
+      </object>
+    </child>
+  </object>
+  <object class="GtkWindow" id="MainWin">
+    <property name="can_focus">False</property>
+    <property name="title" translatable="yes">Matita</property>
+    <child>
+      <object class="GtkEventBox" id="MainWinEventBox">
+        <property name="visible">True</property>
+        <property name="can_focus">False</property>
+        <child>
+          <object class="GtkBox" id="vbox8">
+            <property name="visible">True</property>
+            <property name="can_focus">False</property>
+            <property name="orientation">vertical</property>
+            <child>
+              <object class="GtkMenuBar" id="menubar1">
+                <property name="visible">True</property>
+                <property name="can_focus">False</property>
+                <child>
+                  <object class="GtkMenuItem" id="fileMenu">
+                    <property name="visible">True</property>
+                    <property name="can_focus">False</property>
+                    <property name="label" translatable="yes">_File</property>
+                    <property name="use_underline">True</property>
+                    <child type="submenu">
+                      <object class="GtkMenu" id="fileMenu_menu">
+                        <property name="can_focus">False</property>
+                        <child>
+                          <object class="GtkMenuItem" id="newMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">_New</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="n" signal="activate" modifiers="GDK_CONTROL_MASK"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="openMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">_Open...</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="o" signal="activate" modifiers="GDK_CONTROL_MASK"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="saveMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">_Save</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="s" signal="activate" modifiers="GDK_CONTROL_MASK"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="saveAsMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">_Save as...</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="s" signal="activate" modifiers="GDK_SHIFT_MASK | GDK_CONTROL_MASK"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkSeparatorMenuItem" id="separator2">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="closeMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">_Close</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="w" signal="activate" modifiers="GDK_CONTROL_MASK"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="quitMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">_Quit</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="q" signal="activate" modifiers="GDK_CONTROL_MASK"/>
+                          </object>
+                        </child>
+                      </object>
+                    </child>
+                  </object>
+                </child>
+                <child>
+                  <object class="GtkMenuItem" id="editMenu">
+                    <property name="visible">True</property>
+                    <property name="can_focus">False</property>
+                    <property name="label" translatable="yes">_Edit</property>
+                    <property name="use_underline">True</property>
+                    <child type="submenu">
+                      <object class="GtkMenu" id="editMenu_menu">
+                        <property name="can_focus">False</property>
+                        <child>
+                          <object class="GtkMenuItem" id="undoMenuItem">
+                            <property name="visible">True</property>
+                            <property name="sensitive">False</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">_Undo</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="z" signal="activate" modifiers="GDK_CONTROL_MASK"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="redoMenuItem">
+                            <property name="visible">True</property>
+                            <property name="sensitive">False</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">_Redo</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="z" signal="activate" modifiers="GDK_SHIFT_MASK | GDK_CONTROL_MASK"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkSeparatorMenuItem" id="separator3">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="cutMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">Cut</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="x" signal="activate" modifiers="GDK_CONTROL_MASK"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="copyMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">Copy</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="c" signal="activate" modifiers="GDK_CONTROL_MASK"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="pasteMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">Paste</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="v" signal="activate" modifiers="GDK_CONTROL_MASK"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="pastePatternMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label" translatable="yes">Paste as pattern</property>
+                            <property name="use_underline">True</property>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkCheckMenuItem" id="unicodeAsTexMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label" translatable="yes">Paste Unicode as TeX</property>
+                            <property name="use_underline">True</property>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkCheckMenuItem" id="menuitemAutoAltL">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label" translatable="yes">Auto-expand TeX Macros</property>
+                            <property name="use_underline">True</property>
+                            <property name="active">True</property>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="deleteMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">Delete</property>
+                            <property name="use_underline">True</property>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkSeparatorMenuItem" id="separator4">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="selectAllMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label" translatable="yes">Select _All</property>
+                            <property name="use_underline">True</property>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkSeparatorMenuItem" id="separator7">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="findReplMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">Find and replace...</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="f" signal="activate" modifiers="GDK_CONTROL_MASK"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkSeparatorMenuItem" id="separator8">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="LigatureButton">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label" translatable="yes">Next ligature</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="l" signal="activate" modifiers="GDK_MOD1_MASK"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="externalEditorMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label" translatable="yes">Edit with e_xternal editor</property>
+                            <property name="use_underline">True</property>
+                          </object>
+                        </child>
+                      </object>
+                    </child>
+                  </object>
+                </child>
+                <child>
+                  <object class="GtkMenuItem" id="scriptMenu">
+                    <property name="visible">True</property>
+                    <property name="can_focus">False</property>
+                    <property name="label" translatable="yes">_Script</property>
+                    <property name="use_underline">True</property>
+                    <child type="submenu">
+                      <object class="GtkMenu" id="scriptMenu_menu">
+                        <property name="can_focus">False</property>
+                        <child>
+                          <object class="GtkMenuItem" id="scriptAdvanceMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">Execute 1 phrase</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="Page_Down" signal="activate" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="scriptRetractMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">Retract 1 phrase</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="Page_Up" signal="activate" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkSeparatorMenuItem" id="separator9">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="scriptBottomMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">Execute all</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="End" signal="activate" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="scriptTopMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">Retract all</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="Home" signal="activate" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkSeparatorMenuItem" id="separator10">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="scriptJumpMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">Execute until cursor</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="period" signal="activate" modifiers="GDK_CONTROL_MASK | GDK_MOD1_MASK"/>
+                          </object>
+                        </child>
+                      </object>
+                    </child>
+                  </object>
+                </child>
+                <child>
+                  <object class="GtkMenuItem" id="viewMenu">
+                    <property name="visible">True</property>
+                    <property name="can_focus">False</property>
+                    <property name="label" translatable="yes">_View</property>
+                    <property name="use_underline">True</property>
+                    <child type="submenu">
+                      <object class="GtkMenu" id="viewMenu_menu">
+                        <property name="can_focus">False</property>
+                        <child>
+                          <object class="GtkMenuItem" id="newCicBrowserMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label" translatable="yes">New CIC _browser</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="F3" signal="activate"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkSeparatorMenuItem" id="separator5">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkCheckMenuItem" id="fullscreenMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label" translatable="yes">_Fullscreen</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="F11" signal="activate"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkCheckMenuItem" id="menuitemPalette">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label" translatable="yes">Natural deduction palette</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="F2" signal="activate"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkSeparatorMenuItem" id="separator1">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="increaseFontSizeMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">Zoom in</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="plus" signal="activate" modifiers="GDK_CONTROL_MASK"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="decreaseFontSizeMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">Zoom out</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="minus" signal="activate" modifiers="GDK_CONTROL_MASK"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="normalFontSizeMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">Normal size</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="equal" signal="activate" modifiers="GDK_CONTROL_MASK"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkSeparatorMenuItem" id="separator12">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkCheckMenuItem" id="ppNotationMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label" translatable="yes">Pretty print notation</property>
+                            <property name="use_underline">True</property>
+                            <property name="active">True</property>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkCheckMenuItem" id="hideCoercionsMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label" translatable="yes">Hide coercions</property>
+                            <property name="use_underline">True</property>
+                            <property name="active">True</property>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkSeparatorMenuItem" id="separator13">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="showCoercionsGraphMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label" translatable="yes">Coercions Graph</property>
+                            <property name="use_underline">True</property>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="showHintsDbMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label" translatable="yes">Hints database</property>
+                            <property name="use_underline">True</property>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="showTermGrammarMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label" translatable="yes">Terms grammar</property>
+                            <property name="use_underline">True</property>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="showUnicodeTable">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label" translatable="yes">TeX/UTF-8 table</property>
+                            <property name="use_underline">True</property>
+                          </object>
+                        </child>
+                      </object>
+                    </child>
+                  </object>
+                </child>
+                <child>
+                  <object class="GtkMenuItem" id="debugMenu">
+                    <property name="visible">True</property>
+                    <property name="can_focus">False</property>
+                    <property name="label" translatable="yes">_Debug</property>
+                    <property name="use_underline">True</property>
+                    <child type="submenu">
+                      <object class="GtkMenu" id="debugMenu_menu">
+                        <property name="can_focus">False</property>
+                        <child>
+                          <object class="GtkSeparatorMenuItem" id="separator6">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                          </object>
+                        </child>
+                      </object>
+                    </child>
+                  </object>
+                </child>
+                <child>
+                  <object class="GtkMenuItem" id="helpMenu">
+                    <property name="visible">True</property>
+                    <property name="can_focus">False</property>
+                    <property name="label" translatable="yes">_Help</property>
+                    <property name="use_underline">True</property>
+                    <child type="submenu">
+                      <object class="GtkMenu" id="helpMenu_menu">
+                        <property name="can_focus">False</property>
+                        <child>
+                          <object class="GtkMenuItem" id="contentsMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">Contents</property>
+                            <property name="use_underline">True</property>
+                            <accelerator key="F1" signal="activate"/>
+                          </object>
+                        </child>
+                        <child>
+                          <object class="GtkMenuItem" id="aboutMenuItem">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label">About</property>
+                            <property name="use_underline">True</property>
+                          </object>
+                        </child>
+                      </object>
+                    </child>
+                  </object>
+                </child>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">0</property>
+              </packing>
+            </child>
+            <child>
+              <object class="GtkBox" id="hbox99">
+                <property name="visible">True</property>
+                <property name="can_focus">False</property>
+                <child>
+                  <object class="GtkHPaned" id="hpaneScriptSequent">
+                    <property name="visible">True</property>
+                    <property name="can_focus">True</property>
+                    <child>
+                      <object class="GtkBox" id="hbox18">
+                        <property name="visible">True</property>
+                        <property name="can_focus">False</property>
+                        <property name="spacing">2</property>
+                        <child>
+                          <object class="GtkHandleBox" id="TacticsButtonsHandlebox">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="handle_position">top</property>
+                            <child>
+                              <object class="GtkBox" id="vboxTacticsPalette">
+                                <property name="visible">True</property>
+                                <property name="can_focus">False</property>
+                                <property name="orientation">vertical</property>
+                                <child>
+                                  <object class="GtkExpander" id="expander1">
+                                    <property name="visible">True</property>
+                                    <property name="can_focus">True</property>
+                                    <child>
+                                      <object class="GtkBox" id="vbox1">
+                                        <property name="visible">True</property>
+                                        <property name="can_focus">False</property>
+                                        <property name="orientation">vertical</property>
+                                        <child>
+                                          <object class="GtkButton" id="butImpl_intro">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <child>
+                                              <object class="GtkLabel" id="label8">
+                                                <property name="visible">True</property>
+                                                <property name="can_focus">False</property>
+                                                <property name="label" translatable="yes">Implication (⇒&lt;sub&gt;i&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </object>
+                                            </child>
+                                          </object>
+                                          <packing>
+                                            <property name="expand">True</property>
+                                            <property name="fill">True</property>
+                                            <property name="position">0</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <object class="GtkButton" id="butAnd_intro">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <child>
+                                              <object class="GtkLabel" id="label7">
+                                                <property name="visible">True</property>
+                                                <property name="can_focus">False</property>
+                                                <property name="label" translatable="yes">Conjunction (∧&lt;sub&gt;i&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </object>
+                                            </child>
+                                          </object>
+                                          <packing>
+                                            <property name="expand">True</property>
+                                            <property name="fill">True</property>
+                                            <property name="position">1</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <object class="GtkButton" id="butOr_intro_left">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <child>
+                                              <object class="GtkLabel" id="label9">
+                                                <property name="visible">True</property>
+                                                <property name="can_focus">False</property>
+                                                <property name="label" translatable="yes">Disjunction left (∨&lt;sub&gt;i-l&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </object>
+                                            </child>
+                                          </object>
+                                          <packing>
+                                            <property name="expand">True</property>
+                                            <property name="fill">True</property>
+                                            <property name="position">2</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <object class="GtkButton" id="butOr_intro_right">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <child>
+                                              <object class="GtkLabel" id="label10">
+                                                <property name="visible">True</property>
+                                                <property name="can_focus">False</property>
+                                                <property name="label" translatable="yes">Disjunction right (∨&lt;sub&gt;i-r&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </object>
+                                            </child>
+                                          </object>
+                                          <packing>
+                                            <property name="expand">True</property>
+                                            <property name="fill">True</property>
+                                            <property name="position">3</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <object class="GtkButton" id="butNot_intro">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <child>
+                                              <object class="GtkLabel" id="label11">
+                                                <property name="visible">True</property>
+                                                <property name="can_focus">False</property>
+                                                <property name="label" translatable="yes">Negation (¬&lt;sub&gt;i&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </object>
+                                            </child>
+                                          </object>
+                                          <packing>
+                                            <property name="expand">True</property>
+                                            <property name="fill">True</property>
+                                            <property name="position">4</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <object class="GtkButton" id="butTop_intro">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <child>
+                                              <object class="GtkLabel" id="label12">
+                                                <property name="visible">True</property>
+                                                <property name="can_focus">False</property>
+                                                <property name="label" translatable="yes">Top (⊤&lt;sub&gt;i&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </object>
+                                            </child>
+                                          </object>
+                                          <packing>
+                                            <property name="expand">True</property>
+                                            <property name="fill">True</property>
+                                            <property name="position">5</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <object class="GtkButton" id="butForall_intro">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <child>
+                                              <object class="GtkLabel" id="label20">
+                                                <property name="visible">True</property>
+                                                <property name="can_focus">False</property>
+                                                <property name="label" translatable="yes">Universal (∀&lt;sub&gt;i&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </object>
+                                            </child>
+                                          </object>
+                                          <packing>
+                                            <property name="expand">True</property>
+                                            <property name="fill">True</property>
+                                            <property name="position">6</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <object class="GtkButton" id="butExists_intro">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <child>
+                                              <object class="GtkLabel" id="label21">
+                                                <property name="visible">True</property>
+                                                <property name="can_focus">False</property>
+                                                <property name="label" translatable="yes">Existential (∃&lt;sub&gt;i&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </object>
+                                            </child>
+                                          </object>
+                                          <packing>
+                                            <property name="expand">True</property>
+                                            <property name="fill">True</property>
+                                            <property name="position">7</property>
+                                          </packing>
+                                        </child>
+                                      </object>
+                                    </child>
+                                    <child type="label">
+                                      <object class="GtkLabel" id="label4">
+                                        <property name="visible">True</property>
+                                        <property name="can_focus">False</property>
+                                        <property name="label" translatable="yes">Introduction rules</property>
+                                      </object>
+                                    </child>
+                                  </object>
+                                  <packing>
+                                    <property name="expand">False</property>
+                                    <property name="fill">True</property>
+                                    <property name="position">0</property>
+                                  </packing>
+                                </child>
+                                <child>
+                                  <object class="GtkExpander" id="expander2">
+                                    <property name="visible">True</property>
+                                    <property name="can_focus">True</property>
+                                    <child>
+                                      <object class="GtkBox" id="vbox3">
+                                        <property name="visible">True</property>
+                                        <property name="can_focus">False</property>
+                                        <property name="orientation">vertical</property>
+                                        <child>
+                                          <object class="GtkButton" id="butImpl_elim">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <child>
+                                              <object class="GtkLabel" id="label22">
+                                                <property name="visible">True</property>
+                                                <property name="can_focus">False</property>
+                                                <property name="label" translatable="yes">Implication (⇒&lt;sub&gt;e&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </object>
+                                            </child>
+                                          </object>
+                                          <packing>
+                                            <property name="expand">True</property>
+                                            <property name="fill">True</property>
+                                            <property name="position">0</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <object class="GtkButton" id="butAnd_elim_left">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <child>
+                                              <object class="GtkLabel" id="label23">
+                                                <property name="visible">True</property>
+                                                <property name="can_focus">False</property>
+                                                <property name="label" translatable="yes">Conjunction left (∧&lt;sub&gt;e-l&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </object>
+                                            </child>
+                                          </object>
+                                          <packing>
+                                            <property name="expand">True</property>
+                                            <property name="fill">True</property>
+                                            <property name="position">1</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <object class="GtkButton" id="butAnd_elim_right">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <child>
+                                              <object class="GtkLabel" id="label24">
+                                                <property name="visible">True</property>
+                                                <property name="can_focus">False</property>
+                                                <property name="label" translatable="yes">Conjunction right (∧&lt;sub&gt;e-r&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </object>
+                                            </child>
+                                          </object>
+                                          <packing>
+                                            <property name="expand">True</property>
+                                            <property name="fill">True</property>
+                                            <property name="position">2</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <object class="GtkButton" id="butOr_elim">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <child>
+                                              <object class="GtkLabel" id="label27">
+                                                <property name="visible">True</property>
+                                                <property name="can_focus">False</property>
+                                                <property name="label" translatable="yes">Disjunction (∨&lt;sub&gt;e&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </object>
+                                            </child>
+                                          </object>
+                                          <packing>
+                                            <property name="expand">True</property>
+                                            <property name="fill">True</property>
+                                            <property name="position">3</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <object class="GtkButton" id="butNot_elim">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <child>
+                                              <object class="GtkLabel" id="label31">
+                                                <property name="visible">True</property>
+                                                <property name="can_focus">False</property>
+                                                <property name="label" translatable="yes">Negation (¬&lt;sub&gt;e&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </object>
+                                            </child>
+                                          </object>
+                                          <packing>
+                                            <property name="expand">True</property>
+                                            <property name="fill">True</property>
+                                            <property name="position">4</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <object class="GtkButton" id="butBot_elim">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <child>
+                                              <object class="GtkLabel" id="label33">
+                                                <property name="visible">True</property>
+                                                <property name="can_focus">False</property>
+                                                <property name="label" translatable="yes">Bottom (⊥&lt;sub&gt;e&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </object>
+                                            </child>
+                                          </object>
+                                          <packing>
+                                            <property name="expand">True</property>
+                                            <property name="fill">True</property>
+                                            <property name="position">5</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <object class="GtkButton" id="butForall_elim">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <child>
+                                              <object class="GtkLabel" id="label34">
+                                                <property name="visible">True</property>
+                                                <property name="can_focus">False</property>
+                                                <property name="label" translatable="yes">Universal (∀&lt;sub&gt;e&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </object>
+                                            </child>
+                                          </object>
+                                          <packing>
+                                            <property name="expand">True</property>
+                                            <property name="fill">True</property>
+                                            <property name="position">6</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <object class="GtkButton" id="butExists_elim">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <child>
+                                              <object class="GtkLabel" id="label35">
+                                                <property name="visible">True</property>
+                                                <property name="can_focus">False</property>
+                                                <property name="label" translatable="yes">Existential (∃&lt;sub&gt;e&lt;/sub&gt;)</property>
+                                                <property name="use_markup">True</property>
+                                              </object>
+                                            </child>
+                                          </object>
+                                          <packing>
+                                            <property name="expand">True</property>
+                                            <property name="fill">True</property>
+                                            <property name="position">7</property>
+                                          </packing>
+                                        </child>
+                                      </object>
+                                    </child>
+                                    <child type="label">
+                                      <object class="GtkLabel" id="label5">
+                                        <property name="visible">True</property>
+                                        <property name="can_focus">False</property>
+                                        <property name="label" translatable="yes">Elimination rules</property>
+                                      </object>
+                                    </child>
+                                  </object>
+                                  <packing>
+                                    <property name="expand">False</property>
+                                    <property name="fill">True</property>
+                                    <property name="position">1</property>
+                                  </packing>
+                                </child>
+                                <child>
+                                  <object class="GtkExpander" id="expander3">
+                                    <property name="visible">True</property>
+                                    <property name="can_focus">True</property>
+                                    <child>
+                                      <object class="GtkBox" id="vbox4">
+                                        <property name="visible">True</property>
+                                        <property name="can_focus">False</property>
+                                        <property name="orientation">vertical</property>
+                                        <child>
+                                          <object class="GtkButton" id="butRAA">
+                                            <property name="label" translatable="yes">Reduction to Absurdity (RAA)</property>
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                          </object>
+                                          <packing>
+                                            <property name="expand">True</property>
+                                            <property name="fill">True</property>
+                                            <property name="position">0</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <object class="GtkButton" id="butUseLemma">
+                                            <property name="label" translatable="yes">Use lemma (lem)</property>
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                          </object>
+                                          <packing>
+                                            <property name="expand">True</property>
+                                            <property name="fill">True</property>
+                                            <property name="position">1</property>
+                                          </packing>
+                                        </child>
+                                        <child>
+                                          <object class="GtkButton" id="butDischarge">
+                                            <property name="label" translatable="yes">Discharge (discharge)</property>
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                          </object>
+                                          <packing>
+                                            <property name="expand">True</property>
+                                            <property name="fill">True</property>
+                                            <property name="position">2</property>
+                                          </packing>
+                                        </child>
+                                      </object>
+                                    </child>
+                                    <child type="label">
+                                      <object class="GtkLabel" id="label6">
+                                        <property name="visible">True</property>
+                                        <property name="can_focus">False</property>
+                                        <property name="label" translatable="yes">Misc rules</property>
+                                      </object>
+                                    </child>
+                                  </object>
+                                  <packing>
+                                    <property name="expand">False</property>
+                                    <property name="fill">True</property>
+                                    <property name="position">2</property>
+                                  </packing>
+                                </child>
+                              </object>
+                            </child>
+                          </object>
+                          <packing>
+                            <property name="expand">False</property>
+                            <property name="fill">True</property>
+                            <property name="position">0</property>
+                          </packing>
+                        </child>
+                        <child>
+                          <object class="GtkBox" id="vboxScript">
+                            <property name="width_request">400</property>
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="orientation">vertical</property>
+                            <child>
+                              <object class="GtkBox" id="hbox28">
+                                <property name="visible">True</property>
+                                <property name="can_focus">False</property>
+                                <child>
+                                  <object class="GtkToolbar" id="buttonsToolbar">
+                                    <property name="visible">True</property>
+                                    <property name="can_focus">False</property>
+                                    <property name="toolbar_style">both</property>
+                                    <child>
+                                      <object class="GtkToolItem" id="toolitem41">
+                                        <property name="visible">True</property>
+                                        <property name="can_focus">False</property>
+                                        <child>
+                                          <object class="GtkButton" id="scriptTopButton">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">False</property>
+                                            <property name="tooltip_text" translatable="yes">Retract all</property>
+                                            <property name="relief">none</property>
+                                            <child>
+                                              <object class="GtkImage" id="image920">
+                                                <property name="visible">True</property>
+                                                <property name="can_focus">False</property>
+                                                <property name="stock">gtk-goto-top</property>
+                                              </object>
+                                            </child>
+                                          </object>
+                                        </child>
+                                      </object>
+                                      <packing>
+                                        <property name="expand">False</property>
+                                        <property name="homogeneous">False</property>
+                                      </packing>
+                                    </child>
+                                    <child>
+                                      <object class="GtkToolItem" id="toolitem42">
+                                        <property name="visible">True</property>
+                                        <property name="can_focus">False</property>
+                                        <child>
+                                          <object class="GtkButton" id="scriptRetractButton">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">False</property>
+                                            <property name="tooltip_text" translatable="yes">Retract 1 phrase</property>
+                                            <property name="relief">none</property>
+                                            <child>
+                                              <object class="GtkImage" id="image921">
+                                                <property name="visible">True</property>
+                                                <property name="can_focus">False</property>
+                                                <property name="stock">gtk-go-up</property>
+                                              </object>
+                                            </child>
+                                          </object>
+                                        </child>
+                                      </object>
+                                      <packing>
+                                        <property name="expand">False</property>
+                                        <property name="homogeneous">False</property>
+                                      </packing>
+                                    </child>
+                                    <child>
+                                      <object class="GtkToolItem" id="toolitem43">
+                                        <property name="visible">True</property>
+                                        <property name="can_focus">False</property>
+                                        <child>
+                                          <object class="GtkButton" id="scriptJumpButton">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">False</property>
+                                            <property name="tooltip_text" translatable="yes">Execute until cursor</property>
+                                            <property name="relief">none</property>
+                                            <child>
+                                              <object class="GtkImage" id="image922">
+                                                <property name="visible">True</property>
+                                                <property name="can_focus">False</property>
+                                                <property name="stock">gtk-jump-to</property>
+                                              </object>
+                                            </child>
+                                          </object>
+                                        </child>
+                                      </object>
+                                      <packing>
+                                        <property name="expand">False</property>
+                                        <property name="homogeneous">False</property>
+                                      </packing>
+                                    </child>
+                                    <child>
+                                      <object class="GtkToolItem" id="toolitem44">
+                                        <property name="visible">True</property>
+                                        <property name="can_focus">False</property>
+                                        <child>
+                                          <object class="GtkButton" id="scriptAdvanceButton">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">False</property>
+                                            <property name="tooltip_text" translatable="yes">Execute 1 phrase</property>
+                                            <property name="relief">none</property>
+                                            <child>
+                                              <object class="GtkImage" id="image923">
+                                                <property name="visible">True</property>
+                                                <property name="can_focus">False</property>
+                                                <property name="stock">gtk-go-down</property>
+                                              </object>
+                                            </child>
+                                          </object>
+                                        </child>
+                                      </object>
+                                      <packing>
+                                        <property name="expand">False</property>
+                                        <property name="homogeneous">False</property>
+                                      </packing>
+                                    </child>
+                                    <child>
+                                      <object class="GtkToolItem" id="toolitem45">
+                                        <property name="visible">True</property>
+                                        <property name="can_focus">False</property>
+                                        <child>
+                                          <object class="GtkButton" id="scriptBottomButton">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">False</property>
+                                            <property name="tooltip_text" translatable="yes">Execute all</property>
+                                            <property name="relief">none</property>
+                                            <child>
+                                              <object class="GtkImage" id="image924">
+                                                <property name="visible">True</property>
+                                                <property name="can_focus">False</property>
+                                                <property name="stock">gtk-goto-bottom</property>
+                                              </object>
+                                            </child>
+                                          </object>
+                                        </child>
+                                      </object>
+                                      <packing>
+                                        <property name="expand">False</property>
+                                        <property name="homogeneous">False</property>
+                                      </packing>
+                                    </child>
+                                  </object>
+                                  <packing>
+                                    <property name="expand">True</property>
+                                    <property name="fill">True</property>
+                                    <property name="position">0</property>
+                                  </packing>
+                                </child>
+                                <child>
+                                  <object class="GtkToolbar" id="toolbar2">
+                                    <property name="visible">True</property>
+                                    <property name="can_focus">False</property>
+                                    <property name="orientation">vertical</property>
+                                    <property name="toolbar_style">both</property>
+                                    <child>
+                                      <object class="GtkToolItem" id="toolitem46">
+                                        <property name="visible">True</property>
+                                        <property name="can_focus">False</property>
+                                        <child>
+                                          <object class="GtkButton" id="scriptAbortButton">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">False</property>
+                                            <property name="relief">none</property>
+                                            <child>
+                                              <object class="GtkImage" id="image927">
+                                                <property name="visible">True</property>
+                                                <property name="can_focus">False</property>
+                                                <property name="stock">gtk-stop</property>
+                                              </object>
+                                            </child>
+                                          </object>
+                                        </child>
+                                      </object>
+                                      <packing>
+                                        <property name="expand">False</property>
+                                        <property name="homogeneous">False</property>
+                                      </packing>
+                                    </child>
+                                  </object>
+                                  <packing>
+                                    <property name="expand">False</property>
+                                    <property name="fill">True</property>
+                                    <property name="position">1</property>
+                                  </packing>
+                                </child>
+                              </object>
+                              <packing>
+                                <property name="expand">False</property>
+                                <property name="fill">False</property>
+                                <property name="position">0</property>
+                              </packing>
+                            </child>
+                            <child>
+                              <object class="GtkNotebook" id="scriptNotebook">
+                                <property name="visible">True</property>
+                                <property name="can_focus">True</property>
+                                <property name="scrollable">True</property>
+                              </object>
+                              <packing>
+                                <property name="expand">True</property>
+                                <property name="fill">True</property>
+                                <property name="position">1</property>
+                              </packing>
+                            </child>
+                          </object>
+                          <packing>
+                            <property name="expand">True</property>
+                            <property name="fill">True</property>
+                            <property name="position">1</property>
+                          </packing>
+                        </child>
+                      </object>
+                      <packing>
+                        <property name="resize">False</property>
+                        <property name="shrink">True</property>
+                      </packing>
+                    </child>
+                    <child>
+                      <object class="GtkVPaned" id="vpaned1">
+                        <property name="width_request">250</property>
+                        <property name="height_request">500</property>
+                        <property name="visible">True</property>
+                        <property name="can_focus">True</property>
+                        <property name="position">380</property>
+                        <child>
+                          <object class="GtkNotebook" id="sequentsNotebook">
+                            <property name="visible">True</property>
+                            <property name="can_focus">True</property>
+                            <property name="scrollable">True</property>
+                          </object>
+                          <packing>
+                            <property name="resize">False</property>
+                            <property name="shrink">True</property>
+                          </packing>
+                        </child>
+                        <child>
+                          <object class="GtkBox" id="hbox9">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <child>
+                              <object class="GtkScrolledWindow" id="logScrolledWin">
+                                <property name="visible">True</property>
+                                <property name="can_focus">True</property>
+                                <property name="hscrollbar_policy">never</property>
+                                <property name="shadow_type">in</property>
+                                <child>
+                                  <object class="GtkTextView" id="logTextView">
+                                    <property name="visible">True</property>
+                                    <property name="can_focus">True</property>
+                                    <property name="editable">False</property>
+                                    <property name="wrap_mode">char</property>
+                                    <property name="cursor_visible">False</property>
+                                  </object>
+                                </child>
+                              </object>
+                              <packing>
+                                <property name="expand">True</property>
+                                <property name="fill">True</property>
+                                <property name="position">0</property>
+                              </packing>
+                            </child>
+                          </object>
+                          <packing>
+                            <property name="resize">True</property>
+                            <property name="shrink">True</property>
+                          </packing>
+                        </child>
+                      </object>
+                      <packing>
+                        <property name="resize">True</property>
+                        <property name="shrink">True</property>
+                      </packing>
+                    </child>
+                  </object>
+                  <packing>
+                    <property name="expand">True</property>
+                    <property name="fill">True</property>
+                    <property name="position">0</property>
+                  </packing>
+                </child>
+              </object>
+              <packing>
+                <property name="expand">True</property>
+                <property name="fill">True</property>
+                <property name="position">1</property>
+              </packing>
+            </child>
+            <child>
+              <object class="GtkBox" id="hbox10">
+                <property name="visible">True</property>
+                <property name="can_focus">False</property>
+                <child>
+                  <object class="GtkStatusbar" id="StatusBar">
+                    <property name="visible">True</property>
+                    <property name="can_focus">False</property>
+                  </object>
+                  <packing>
+                    <property name="expand">True</property>
+                    <property name="fill">True</property>
+                    <property name="position">0</property>
+                  </packing>
+                </child>
+                <child>
+                  <object class="GtkNotebook" id="HintNotebook">
+                    <property name="visible">True</property>
+                    <property name="can_focus">False</property>
+                    <property name="show_tabs">False</property>
+                    <child>
+                      <object class="GtkImage" id="HintLowImage">
+                        <property name="visible">True</property>
+                        <property name="can_focus">False</property>
+                        <property name="stock">gtk-missing-image</property>
+                      </object>
+                    </child>
+                    <child type="tab">
+                      <object class="GtkLabel" id="label14">
+                        <property name="visible">True</property>
+                        <property name="can_focus">False</property>
+                        <property name="label" translatable="yes">label14</property>
+                      </object>
+                      <packing>
+                        <property name="tab_fill">False</property>
+                      </packing>
+                    </child>
+                    <child>
+                      <object class="GtkImage" id="HintMediumImage">
+                        <property name="visible">True</property>
+                        <property name="can_focus">False</property>
+                        <property name="stock">gtk-missing-image</property>
+                      </object>
+                      <packing>
+                        <property name="position">1</property>
+                      </packing>
+                    </child>
+                    <child type="tab">
+                      <object class="GtkLabel" id="label15">
+                        <property name="visible">True</property>
+                        <property name="can_focus">False</property>
+                        <property name="label" translatable="yes">label15</property>
+                      </object>
+                      <packing>
+                        <property name="position">1</property>
+                        <property name="tab_fill">False</property>
+                      </packing>
+                    </child>
+                    <child>
+                      <object class="GtkImage" id="HintHighImage">
+                        <property name="visible">True</property>
+                        <property name="can_focus">False</property>
+                        <property name="stock">gtk-missing-image</property>
+                      </object>
+                      <packing>
+                        <property name="position">2</property>
+                      </packing>
+                    </child>
+                    <child type="tab">
+                      <object class="GtkLabel" id="label16">
+                        <property name="visible">True</property>
+                        <property name="can_focus">False</property>
+                        <property name="label" translatable="yes">label16</property>
+                      </object>
+                      <packing>
+                        <property name="position">2</property>
+                        <property name="tab_fill">False</property>
+                      </packing>
+                    </child>
+                  </object>
+                  <packing>
+                    <property name="expand">False</property>
+                    <property name="fill">True</property>
+                    <property name="position">1</property>
+                  </packing>
+                </child>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">2</property>
+              </packing>
+            </child>
+          </object>
+        </child>
+      </object>
+    </child>
+  </object>
+  <object class="GtkDialog" id="TextDialog">
+    <property name="can_focus">False</property>
+    <property name="title" translatable="yes">DUMMY</property>
+    <property name="type_hint">dialog</property>
+    <child internal-child="vbox">
+      <object class="GtkBox" id="vbox5">
+        <property name="visible">True</property>
+        <property name="can_focus">False</property>
+        <property name="orientation">vertical</property>
+        <child internal-child="action_area">
+          <object class="GtkButtonBox" id="hbuttonbox1">
+            <property name="visible">True</property>
+            <property name="can_focus">False</property>
+            <property name="layout_style">end</property>
+            <child>
+              <object class="GtkButton" id="TextDialogCancelButton">
+                <property name="label">gtk-cancel</property>
+                <property name="visible">True</property>
+                <property name="can_focus">True</property>
+                <property name="can_default">True</property>
+                <property name="receives_default">False</property>
+                <property name="use_stock">True</property>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">0</property>
+              </packing>
+            </child>
+            <child>
+              <object class="GtkButton" id="TextDialogOkButton">
+                <property name="label">gtk-ok</property>
+                <property name="visible">True</property>
+                <property name="can_focus">True</property>
+                <property name="can_default">True</property>
+                <property name="receives_default">False</property>
+                <property name="use_stock">True</property>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">1</property>
+              </packing>
+            </child>
+          </object>
+          <packing>
+            <property name="expand">False</property>
+            <property name="fill">False</property>
+            <property name="pack_type">end</property>
+            <property name="position">0</property>
+          </packing>
+        </child>
+        <child>
+          <object class="GtkLabel" id="TextDialogLabel">
+            <property name="visible">True</property>
+            <property name="can_focus">False</property>
+            <property name="label" translatable="yes">DUMMY</property>
+          </object>
+          <packing>
+            <property name="expand">False</property>
+            <property name="fill">False</property>
+            <property name="position">2</property>
+          </packing>
+        </child>
+        <child>
+          <object class="GtkScrolledWindow" id="scrolledwindow2">
+            <property name="visible">True</property>
+            <property name="can_focus">True</property>
+            <property name="shadow_type">in</property>
+            <child>
+              <object class="GtkTextView" id="TextDialogTextView">
+                <property name="visible">True</property>
+                <property name="can_focus">True</property>
+              </object>
+            </child>
+          </object>
+          <packing>
+            <property name="expand">False</property>
+            <property name="fill">True</property>
+            <property name="position">3</property>
+          </packing>
+        </child>
+      </object>
+    </child>
+    <action-widgets>
+      <action-widget response="-6">TextDialogCancelButton</action-widget>
+      <action-widget response="-5">TextDialogOkButton</action-widget>
+    </action-widgets>
+  </object>
+  <object class="GtkDialog" id="UriChoiceDialog">
+    <property name="height_request">280</property>
+    <property name="can_focus">False</property>
+    <property name="title" translatable="yes">Uri choice</property>
+    <property name="modal">True</property>
+    <property name="window_position">center</property>
+    <property name="type_hint">dialog</property>
+    <child internal-child="vbox">
+      <object class="GtkBox" id="dialog-vbox3">
+        <property name="visible">True</property>
+        <property name="can_focus">False</property>
+        <property name="orientation">vertical</property>
+        <property name="spacing">4</property>
+        <child internal-child="action_area">
+          <object class="GtkButtonBox" id="dialog-action_area3">
+            <property name="visible">True</property>
+            <property name="can_focus">False</property>
+            <property name="layout_style">end</property>
+            <child>
+              <object class="GtkButton" id="UriChoiceAbortButton">
+                <property name="label">gtk-cancel</property>
+                <property name="visible">True</property>
+                <property name="can_focus">True</property>
+                <property name="can_default">True</property>
+                <property name="receives_default">False</property>
+                <property name="use_stock">True</property>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">0</property>
+              </packing>
+            </child>
+            <child>
+              <object class="GtkButton" id="UriChoiceSelectedButton">
+                <property name="visible">True</property>
+                <property name="can_focus">True</property>
+                <property name="can_default">True</property>
+                <property name="receives_default">False</property>
+                <child>
+                  <object class="GtkAlignment" id="alignment2">
+                    <property name="visible">True</property>
+                    <property name="can_focus">False</property>
+                    <property name="xscale">0</property>
+                    <property name="yscale">0</property>
+                    <child>
+                      <object class="GtkBox" id="hbox3">
+                        <property name="visible">True</property>
+                        <property name="can_focus">False</property>
+                        <property name="spacing">2</property>
+                        <child>
+                          <object class="GtkImage" id="image19">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="stock">gtk-index</property>
+                          </object>
+                          <packing>
+                            <property name="expand">False</property>
+                            <property name="fill">False</property>
+                            <property name="position">0</property>
+                          </packing>
+                        </child>
+                        <child>
+                          <object class="GtkLabel" id="label3">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label" translatable="yes">Try _Selected</property>
+                            <property name="use_underline">True</property>
+                          </object>
+                          <packing>
+                            <property name="expand">False</property>
+                            <property name="fill">False</property>
+                            <property name="position">1</property>
+                          </packing>
+                        </child>
+                      </object>
+                    </child>
+                  </object>
+                </child>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">1</property>
+              </packing>
+            </child>
+            <child>
+              <object class="GtkButton" id="UriChoiceConstantsButton">
+                <property name="label" translatable="yes">Try Constants</property>
+                <property name="visible">True</property>
+                <property name="sensitive">False</property>
+                <property name="can_focus">True</property>
+                <property name="can_default">True</property>
+                <property name="receives_default">False</property>
+                <property name="use_underline">True</property>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">2</property>
+              </packing>
+            </child>
+            <child>
+              <object class="GtkButton" id="copyButton">
+                <property name="label">gtk-copy</property>
+                <property name="can_focus">True</property>
+                <property name="can_default">True</property>
+                <property name="receives_default">False</property>
+                <property name="use_stock">True</property>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">3</property>
+              </packing>
+            </child>
+            <child>
+              <object class="GtkButton" id="uriChoiceAutoButton">
+                <property name="visible">True</property>
+                <property name="can_focus">True</property>
+                <property name="can_default">True</property>
+                <property name="receives_default">False</property>
+                <child>
+                  <object class="GtkAlignment" id="alignment5">
+                    <property name="visible">True</property>
+                    <property name="can_focus">False</property>
+                    <property name="xscale">0</property>
+                    <property name="yscale">0</property>
+                    <child>
+                      <object class="GtkBox" id="hbox16">
+                        <property name="visible">True</property>
+                        <property name="can_focus">False</property>
+                        <property name="spacing">2</property>
+                        <child>
+                          <object class="GtkImage" id="image302">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="stock">gtk-ok</property>
+                          </object>
+                          <packing>
+                            <property name="expand">False</property>
+                            <property name="fill">False</property>
+                            <property name="position">0</property>
+                          </packing>
+                        </child>
+                        <child>
+                          <object class="GtkLabel" id="okLabel">
+                            <property name="visible">True</property>
+                            <property name="can_focus">False</property>
+                            <property name="label" translatable="yes">bla bla bla</property>
+                            <property name="use_underline">True</property>
+                          </object>
+                          <packing>
+                            <property name="expand">False</property>
+                            <property name="fill">False</property>
+                            <property name="position">1</property>
+                          </packing>
+                        </child>
+                      </object>
+                    </child>
+                  </object>
+                </child>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">4</property>
+              </packing>
+            </child>
+            <child>
+              <object class="GtkButton" id="uriChoiceForwardButton">
+                <property name="label">gtk-go-forward</property>
+                <property name="visible">True</property>
+                <property name="can_focus">True</property>
+                <property name="can_default">True</property>
+                <property name="receives_default">False</property>
+                <property name="use_stock">True</property>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">5</property>
+              </packing>
+            </child>
+          </object>
+          <packing>
+            <property name="expand">False</property>
+            <property name="fill">False</property>
+            <property name="pack_type">end</property>
+            <property name="position">0</property>
+          </packing>
+        </child>
+        <child>
+          <object class="GtkBox" id="vbox2">
+            <property name="visible">True</property>
+            <property name="can_focus">False</property>
+            <property name="orientation">vertical</property>
+            <property name="spacing">3</property>
+            <child>
+              <object class="GtkLabel" id="UriChoiceLabel">
+                <property name="visible">True</property>
+                <property name="can_focus">False</property>
+                <property name="label" translatable="yes">some informative message here ...</property>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">False</property>
+                <property name="position">0</property>
+              </packing>
+            </child>
+            <child>
+              <object class="GtkScrolledWindow" id="scrolledwindow1">
+                <property name="width_request">400</property>
+                <property name="visible">True</property>
+                <property name="can_focus">True</property>
+                <child>
+                  <object class="GtkTreeView" id="UriChoiceTreeView">
+                    <property name="visible">True</property>
+                    <property name="can_focus">True</property>
+                    <property name="headers_visible">False</property>
+                    <child internal-child="selection">
+                      <object class="GtkTreeSelection"/>
+                    </child>
+                  </object>
+                </child>
+              </object>
+              <packing>
+                <property name="expand">True</property>
+                <property name="fill">True</property>
+                <property name="position">1</property>
+              </packing>
+            </child>
+            <child>
+              <object class="GtkBox" id="uriEntryHBox">
+                <property name="visible">True</property>
+                <property name="can_focus">False</property>
+                <child>
+                  <object class="GtkLabel" id="label2">
+                    <property name="visible">True</property>
+                    <property name="can_focus">False</property>
+                    <property name="label" translatable="yes">URI: </property>
+                  </object>
+                  <packing>
+                    <property name="expand">False</property>
+                    <property name="fill">False</property>
+                    <property name="position">0</property>
+                  </packing>
+                </child>
+                <child>
+                  <object class="GtkEntry" id="entry1">
+                    <property name="visible">True</property>
+                    <property name="can_focus">True</property>
+                  </object>
+                  <packing>
+                    <property name="expand">True</property>
+                    <property name="fill">True</property>
+                    <property name="position">1</property>
+                  </packing>
+                </child>
+              </object>
+              <packing>
+                <property name="expand">False</property>
+                <property name="fill">True</property>
+                <property name="position">2</property>
+              </packing>
+            </child>
+          </object>
+          <packing>
+            <property name="expand">False</property>
+            <property name="fill">True</property>
+            <property name="position">2</property>
+          </packing>
+        </child>
+      </object>
+    </child>
+    <action-widgets>
+      <action-widget response="-6">UriChoiceAbortButton</action-widget>
+    </action-widgets>
+  </object>
+</interface>

diff --git a/matita/matita/matitaGtkMisc.ml b/matita/matita/matitaGtkMisc.ml
index aaf297da2bfd7fa4f9e282a02dc2cb77c04c04b3..2022704309e77c21f732386a67606c5b0b0b3247 100644 (file)
--- 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 05a724136617abd9bb94986a5475682bb5eab688..cf4ce93a9d17e836119410bb93dc99466c0369b0 100644 (file)
--- 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 94e3e751db0f046b2f27cf01f36ca761b8fb202e..d8de328ef17d5dad8ea13e94ec6aa2349075c21c 100644 (file)
--- 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 (file)
index 0000000..be9d65a
--- /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 ea9683e188bd6232c3e2996806541fed68a2d56a..390257422968e77420d0374890e335342b898d22 100644 (file)
--- 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 fe6fd35579cfa838a5f098fbd4b1fbc7a605a797..e612b88031396548b92cbc5f1ae69579d7da14b9 100644 (file)
--- 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 de78194f0254f0592642d8b90ad40c3ccd183fde..33296d2320ec2be4487110090af548ba9586d86b 100644 (file)
--- 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 9958170d9c400eb663309947ac2df5f95a8b6fd9..ca4b2f86dcdb4dafdb27f3175ffde5217153e980 100644 (file)
--- 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 *)