From b4fb1d2a880acc6123c31e8ab70c9089b9f8a270 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti 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