From b4fb1d2a880acc6123c31e8ab70c9089b9f8a270 Mon Sep 17 00:00:00 2001
From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Wed, 8 Jun 2011 11:14:02 +0000
Subject: [PATCH] Removed dependency of Matitaweb from GTK libraries.

---
 matitaB/configure.ac           |  2 --
 matitaB/matita/Makefile        |  8 ++++----
 matitaB/matita/matitadaemon.ml | 13 ++++++++++---
 3 files changed, 14 insertions(+), 9 deletions(-)

diff --git a/matitaB/configure.ac b/matitaB/configure.ac
index 17ceabba1..e11e011a0 100644
--- 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 8c3e8c29e..05e632427 100644
--- 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 3d9b9d09c..ea63e1a08 100644
--- 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) =
-- 
2.39.2