Removed dependency of Matitaweb from GTK libraries.

diff --git a/matitaB/configure.ac b/matitaB/configure.ac
index 17ceabba1a24a9ec201c39c2e34cbbb2bf64537d..e11e011a0b8304990792a2876e9c7f761576dc0b 100644 (file)
--- a/matitaB/configure.ac
+++ b/matitaB/configure.ac
@@ -98,8 +98,6 @@ FINDLIB_WREQUIRES="\
 $FINDLIB_CREQUIRES \
 netcgi2 \
 nethttpd \
-lablgtk2.glade \
-lablgtksourceview2.gtksourceview2 \
 "
 for r in $FINDLIB_LIBSREQUIRES $FINDLIB_REQUIRES
 do

diff --git a/matitaB/matita/Makefile b/matitaB/matita/Makefile
index 8c3e8c29ea1d885797210bbc72e71a6767331c43..05e632427c356b8928e3c94c9e408fddc3cfcb62 100644 (file)
--- a/matitaB/matita/Makefile
+++ b/matitaB/matita/Makefile
@@ -141,12 +141,12 @@ matitac.opt: matitac.ml $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS)
        $(H)echo "  OCAMLOPT $<"
        $(H)$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml
 
-matitadaemon: matitadaemon.ml $(WLIB_DEPS) $(CMOS) $(MAINCMOS)
+matitadaemon: matitadaemon.ml $(WLIB_DEPS) $(CCMOS) $(MAINCMOS)
        $(H)echo "  OCAMLC $<"
-       $(H)$(OCAMLC) $(WPKGS) -linkpkg -o $@ $(CMOS) $(MAINCMOS) matitadaemon.ml
-matitadaemon.opt: matitadaemon.ml $(WLIBX_DEPS) $(CMXS) $(MAINCMXS)
+       $(H)$(OCAMLC) $(WPKGS) -linkpkg -o $@ $(CCMOS) $(MAINCMOS) matitadaemon.ml
+matitadaemon.opt: matitadaemon.ml $(WLIBX_DEPS) $(CCMXS) $(MAINCMXS)
        $(H)echo "  OCAMLOPT $<"
-       $(H)$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) $(MAINCMXS) matitadaemon.ml
+       $(H)$(OCAMLOPT) $(WPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitadaemon.ml
 
 rottener: rottener.ml $(CLIB_DEPS) $(CCMOS) $(MAINCMOS)
        $(H)echo "  OCAMLC $<"

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 3d9b9d09cfdcb9faa7836e8ee2fc40053a5e6ac7..ea63e1a084ba6d231695f693559e650a11b06d82 100644 (file)
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -5,6 +5,12 @@ module Stack = Continuationals.Stack
 
 let utf8_length = Netconversion.ustring_length `Enc_utf8
 
+let utf8_parsed_text s floc =
+  let start, stop = HExtlib.loc_of_floc floc in
+  let len = stop - start in
+  let res = Netconversion.ustring_sub `Enc_utf8 start len s in
+  res, String.length res
+
 (*** from matitaScript.ml ***)
 (* let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" *)
 
@@ -27,8 +33,8 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script
   | GrafiteAst.Comment (loc, _) -> loc in
   
   let _,lend = HExtlib.loc_of_floc floc in 
-  let parsed_text, parsed_text_len = 
-    MatitaGtkMisc.utf8_parsed_text unparsed_text (HExtlib.floc_of_loc (0,lend)) in
+  let parsed_text, _parsed_text_len = 
+    utf8_parsed_text unparsed_text (HExtlib.floc_of_loc (0,lend)) in
   let byte_parsed_text_len = String.length parsed_text in
   let unparsed_txt' = 
     String.sub unparsed_text byte_parsed_text_len 
@@ -44,6 +50,7 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script
 
 let status = ref (new MatitaEngine.status "cic:/matita");;
 let history = ref [!status];;
+let sequent_size = ref 40;;
 
 let include_paths = ref [];;
 
@@ -68,7 +75,7 @@ let output_status s =
   | Stack.Open i ->
       let meta = List.assoc i metasenv in
       snd (ApplyTransformation.ntxt_of_cic_sequent 
-        ~metasenv ~subst ~map_unicode_to_tex:false 80 s (i,meta))
+        ~metasenv ~subst ~map_unicode_to_tex:false !sequent_size s (i,meta))
   | Stack.Closed _ -> "This goal has already been closed."
   in
   let render_sequent is_loc acc depth tag (pos,sw) =