From: Andrea Asperti Date: Tue, 5 Oct 2010 13:56:33 +0000 (+0000) Subject: - matitaWiki removed X-Git-Tag: make_still_working~2810 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c0700c9d9cf3aa044b2f2945a832a6c2eebd5409;p=helm.git - matitaWiki removed - dump_moo removed - matitaAutoGui removed --- diff --git a/matita/matita/.depend b/matita/matita/.depend index 9ebd03a64..e07465dfd 100644 --- a/matita/matita/.depend +++ b/matita/matita/.depend @@ -1,39 +1,37 @@ applyTransformation.cmo: applyTransformation.cmi applyTransformation.cmx: applyTransformation.cmi -dump_moo.cmo: buildTimeConf.cmo -dump_moo.cmx: buildTimeConf.cmx +buildTimeConf.cmo: +buildTimeConf.cmx: lablGraphviz.cmo: lablGraphviz.cmi lablGraphviz.cmx: lablGraphviz.cmi -matitaAutoGui.cmo: matitaGtkMisc.cmi matitaGeneratedGui.cmo buildTimeConf.cmo \ - applyTransformation.cmi matitaAutoGui.cmi -matitaAutoGui.cmx: matitaGtkMisc.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \ - applyTransformation.cmx matitaAutoGui.cmi matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi matitacLib.cmo: matitaMisc.cmi matitaExcPp.cmi matitaEngine.cmi \ buildTimeConf.cmo applyTransformation.cmi matitacLib.cmi matitacLib.cmx: matitaMisc.cmx matitaExcPp.cmx matitaEngine.cmx \ buildTimeConf.cmx applyTransformation.cmx matitacLib.cmi -matitac.cmo: matitadep.cmi matitaclean.cmi matitacLib.cmi matitaWiki.cmo \ - matitaMisc.cmi matitaInit.cmi -matitac.cmx: matitadep.cmx matitaclean.cmx matitacLib.cmx matitaWiki.cmx \ - matitaMisc.cmx matitaInit.cmx +matitac.cmo: matitadep.cmi matitaclean.cmi matitacLib.cmi matitaMisc.cmi \ + matitaInit.cmi +matitac.cmx: matitadep.cmx matitaclean.cmx matitacLib.cmx matitaMisc.cmx \ + matitaInit.cmx matitadep.cmo: matitaMisc.cmi matitaInit.cmi matitadep.cmi matitadep.cmx: matitaMisc.cmx matitaInit.cmx matitadep.cmi matitaEngine.cmo: applyTransformation.cmi matitaEngine.cmi matitaEngine.cmx: applyTransformation.cmx matitaEngine.cmi matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi matitaExcPp.cmx: matitaEngine.cmx matitaExcPp.cmi +matitaGeneratedGui.cmo: +matitaGeneratedGui.cmx: matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmo buildTimeConf.cmo \ matitaGtkMisc.cmi matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \ matitaGtkMisc.cmi matitaGui.cmo: virtuals.cmi matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ matitaMathView.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmo \ - matitaExcPp.cmi matitaAutoGui.cmi buildTimeConf.cmo matitaGui.cmi + matitaExcPp.cmi buildTimeConf.cmo matitaGui.cmi matitaGui.cmx: virtuals.cmx matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ matitaMathView.cmx matitaGtkMisc.cmx matitaGeneratedGui.cmx \ - matitaExcPp.cmx matitaAutoGui.cmx buildTimeConf.cmx matitaGui.cmi + matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi matitaInit.cmo: matitaExcPp.cmi buildTimeConf.cmo matitaInit.cmi matitaInit.cmx: matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi matitaMathView.cmo: virtuals.cmi matitaTypes.cmi matitaScript.cmi \ @@ -60,16 +58,24 @@ matitaScript.cmx: virtuals.cmx matitacLib.cmx matitaTypes.cmx \ applyTransformation.cmx matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi -matitaWiki.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ - buildTimeConf.cmo applyTransformation.cmi -matitaWiki.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ - buildTimeConf.cmx applyTransformation.cmx predefined_virtuals.cmo: virtuals.cmi predefined_virtuals.cmi predefined_virtuals.cmx: virtuals.cmx predefined_virtuals.cmi virtuals.cmo: virtuals.cmi virtuals.cmx: virtuals.cmi +applyTransformation.cmi: +lablGraphviz.cmi: +matitaclean.cmi: +matitacLib.cmi: +matitadep.cmi: +matitaEngine.cmi: +matitaExcPp.cmi: matitaGtkMisc.cmi: matitaGeneratedGui.cmo matitaGui.cmi: matitaGuiTypes.cmi matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmo +matitaInit.cmi: matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi +matitaMisc.cmi: matitaScript.cmi: matitaTypes.cmi +matitaTypes.cmi: +predefined_virtuals.cmi: +virtuals.cmi: diff --git a/matita/matita/.depend.opt b/matita/matita/.depend.opt index e4454794f..a6f969454 100644 --- a/matita/matita/.depend.opt +++ b/matita/matita/.depend.opt @@ -1,39 +1,37 @@ applyTransformation.cmo: applyTransformation.cmi applyTransformation.cmx: applyTransformation.cmi -dump_moo.cmo: buildTimeConf.cmx -dump_moo.cmx: buildTimeConf.cmx +buildTimeConf.cmo: +buildTimeConf.cmx: lablGraphviz.cmo: lablGraphviz.cmi lablGraphviz.cmx: lablGraphviz.cmi -matitaAutoGui.cmo: matitaGtkMisc.cmi matitaGeneratedGui.cmx buildTimeConf.cmx \ - applyTransformation.cmi matitaAutoGui.cmi -matitaAutoGui.cmx: matitaGtkMisc.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \ - applyTransformation.cmx matitaAutoGui.cmi matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi matitacLib.cmo: matitaMisc.cmi matitaExcPp.cmi matitaEngine.cmi \ buildTimeConf.cmx applyTransformation.cmi matitacLib.cmi matitacLib.cmx: matitaMisc.cmx matitaExcPp.cmx matitaEngine.cmx \ buildTimeConf.cmx applyTransformation.cmx matitacLib.cmi -matitac.cmo: matitadep.cmi matitaclean.cmi matitacLib.cmi matitaWiki.cmx \ - matitaMisc.cmi matitaInit.cmi -matitac.cmx: matitadep.cmx matitaclean.cmx matitacLib.cmx matitaWiki.cmx \ - matitaMisc.cmx matitaInit.cmx +matitac.cmo: matitadep.cmi matitaclean.cmi matitacLib.cmi matitaMisc.cmi \ + matitaInit.cmi +matitac.cmx: matitadep.cmx matitaclean.cmx matitacLib.cmx matitaMisc.cmx \ + matitaInit.cmx matitadep.cmo: matitaMisc.cmi matitaInit.cmi matitadep.cmi matitadep.cmx: matitaMisc.cmx matitaInit.cmx matitadep.cmi -matitaEngine.cmo: matitaEngine.cmi -matitaEngine.cmx: matitaEngine.cmi +matitaEngine.cmo: applyTransformation.cmi matitaEngine.cmi +matitaEngine.cmx: applyTransformation.cmx matitaEngine.cmi matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi matitaExcPp.cmx: matitaEngine.cmx matitaExcPp.cmi +matitaGeneratedGui.cmo: +matitaGeneratedGui.cmx: matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmx buildTimeConf.cmx \ matitaGtkMisc.cmi matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \ matitaGtkMisc.cmi matitaGui.cmo: virtuals.cmi matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ matitaMathView.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmx \ - matitaExcPp.cmi matitaAutoGui.cmi buildTimeConf.cmx matitaGui.cmi + matitaExcPp.cmi buildTimeConf.cmx matitaGui.cmi matitaGui.cmx: virtuals.cmx matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ matitaMathView.cmx matitaGtkMisc.cmx matitaGeneratedGui.cmx \ - matitaExcPp.cmx matitaAutoGui.cmx buildTimeConf.cmx matitaGui.cmi + matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi matitaInit.cmo: matitaExcPp.cmi buildTimeConf.cmx matitaInit.cmi matitaInit.cmx: matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi matitaMathView.cmo: virtuals.cmi matitaTypes.cmi matitaScript.cmi \ @@ -52,24 +50,32 @@ matita.cmo: predefined_virtuals.cmi matitaTypes.cmi matitaScript.cmi \ matita.cmx: predefined_virtuals.cmx matitaTypes.cmx matitaScript.cmx \ matitaMathView.cmx matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx \ buildTimeConf.cmx applyTransformation.cmx -matitaScript.cmo: virtuals.cmi matitacLib.cmi matitaTypes.cmi matitaMisc.cmi \ +matitaScript.cmo: virtuals.cmi matitacLib.cmi matitaTypes.cmi \ matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmx \ applyTransformation.cmi matitaScript.cmi -matitaScript.cmx: virtuals.cmx matitacLib.cmx matitaTypes.cmx matitaMisc.cmx \ +matitaScript.cmx: virtuals.cmx matitacLib.cmx matitaTypes.cmx \ matitaGtkMisc.cmx matitaEngine.cmx buildTimeConf.cmx \ applyTransformation.cmx matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi -matitaWiki.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ - buildTimeConf.cmx applyTransformation.cmi -matitaWiki.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ - buildTimeConf.cmx applyTransformation.cmx predefined_virtuals.cmo: virtuals.cmi predefined_virtuals.cmi predefined_virtuals.cmx: virtuals.cmx predefined_virtuals.cmi virtuals.cmo: virtuals.cmi virtuals.cmx: virtuals.cmi +applyTransformation.cmi: +lablGraphviz.cmi: +matitaclean.cmi: +matitacLib.cmi: +matitadep.cmi: +matitaEngine.cmi: +matitaExcPp.cmi: matitaGtkMisc.cmi: matitaGeneratedGui.cmx matitaGui.cmi: matitaGuiTypes.cmi matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmx +matitaInit.cmi: matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi +matitaMisc.cmi: matitaScript.cmi: matitaTypes.cmi +matitaTypes.cmi: +predefined_virtuals.cmi: +virtuals.cmi: diff --git a/matita/matita/Makefile b/matita/matita/Makefile index fcf51b5d0..c76236dde 100644 --- a/matita/matita/Makefile +++ b/matita/matita/Makefile @@ -25,7 +25,7 @@ OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS) $(OCAMLOPT_DEBUG_FLAGS) OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAMLDEP_FLAGS) INSTALL_PROGRAMS= matita matitac INSTALL_PROGRAMS_LINKS_MATITA= -INSTALL_PROGRAMS_LINKS_MATITAC= matitadep matitaclean matitawiki +INSTALL_PROGRAMS_LINKS_MATITAC= matitadep matitaclean MATITA_FLAGS = -noprofile NODB=false @@ -43,7 +43,6 @@ MLI = \ matitacLib.mli \ matitaInit.mli \ matitaGtkMisc.mli \ - matitaAutoGui.mli \ virtuals.mli \ matitaScript.mli \ predefined_virtuals.mli \ @@ -58,7 +57,6 @@ CMLI = \ matitaExcPp.mli \ matitacLib.mli \ matitaInit.mli \ - matitaWiki.mli \ $(NULL) MAINCMLI = \ matitadep.mli \ @@ -71,11 +69,10 @@ CML = buildTimeConf.ml $(CMLI:%.mli=%.ml) MAINCML = $(MAINCMLI:%.mli=%.ml) PROGRAMS_BYTE = \ - matita matitac matitadep matitaclean \ - matitawiki + matita matitac matitadep matitaclean PROGRAMS = $(PROGRAMS_BYTE) PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE)) -NOINST_PROGRAMS = dump_moo +NOINST_PROGRAMS = NOINST_PROGRAMS_OPT = $(patsubst %,%.opt,$(EXTRA_PROGRAMS)) .PHONY: all @@ -126,13 +123,6 @@ matita.opt: matita.ml $(LIBX_DEPS) $(CMXS) $(H)echo " OCAMLOPT $<" $(H)$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml -dump_moo: dump_moo.ml buildTimeConf.cmo - $(H)echo " OCAMLC $<" - $(H)$(OCAMLC) $(PKGS) -linkpkg -o $@ buildTimeConf.cmo $< -dump_moo.opt: dump_moo.ml buildTimeConf.cmx - $(H)echo "OCAMLOPT $<" - $(H)$(OCAMLOPT) $(PKGS) -linkpkg -o $@ buildTimeConf.cmx $< - matitac: matitac.ml $(CLIB_DEPS) $(CCMOS) $(MAINCMOS) $(H)echo " OCAMLC $<" $(H)$(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) $(MAINCMOS) matitac.ml @@ -154,11 +144,6 @@ matitadep: matitac matitadep.opt: matitac.opt $(H)test -f $@ || ln -s $< $@ -matitawiki: matitac - $(H)test -f $@ || ln -s $< $@ -matitawiki.opt: matitac.opt - $(H)test -f $@ || ln -s $< $@ - matitaclean: matitac $(H)test -f $@ || ln -s $< $@ matitaclean.opt: matitac.opt @@ -338,11 +323,6 @@ matita.opt.static: $(STATIC_LINK) $(LIBX_DEPS) $(CMXS) matita.ml $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml \ $(STATIC_EXTRA_LIBS) strip $@ -dump_moo.opt.static: $(STATIC_LINK) buildTimeConf.cmx dump_moo.ml - $(STATIC_LINK) $(STATIC_CLIBS) -- \ - $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $^ \ - $(STATIC_EXTRA_CLIBS) - strip $@ matitac.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml $(STATIC_LINK) $(STATIC_CLIBS) -- \ $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml \ @@ -352,8 +332,6 @@ matitadep.opt.static: matitac.opt.static $(H)test -f $@ || ln -s $< $@ matitaclean.opt.static: matitac.opt.static $(H)test -f $@ || ln -s $< $@ -matitawiki.opt.static: matitac.opt.static - $(H)test -f $@ || ln -s $< $@ %.upx: % cp $< $@ diff --git a/matita/matita/dump_moo.ml b/matita/matita/dump_moo.ml deleted file mode 100644 index 6b8658abd..000000000 --- a/matita/matita/dump_moo.ml +++ /dev/null @@ -1,60 +0,0 @@ -(* Copyright (C) 2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(* $Id$ *) - -open Printf - -let arg_spec = - let std_arg_spec = [] in - let debug_arg_spec = [] in - std_arg_spec @ debug_arg_spec - -let usage = - sprintf "MatitaC v%s\nUsage: dump_moo [option ...] file.moo\nOptions:" - BuildTimeConf.version - -let _ = - let moos = ref [] in - let add_moo fname = moos := fname :: !moos in - Arg.parse arg_spec add_moo usage; - if !moos = [] then begin print_endline usage; exit 1 end; - List.iter - (fun fname -> - if not (Sys.file_exists fname) then - HLog.error (sprintf "Can't find moo '%s', skipping it." fname) - else begin - printf "%s:\n" fname; flush stdout; - let commands = GrafiteMarshal.load_moo ~fname in - List.iter - (fun cmd -> - printf " %s\n%!" - (GrafiteAstPp.pp_command - ~term_pp:(fun t -> CicPp.ppterm t) - ~obj_pp:(fun _ -> "OBJ") cmd)) - commands; - end) - (List.rev !moos) - diff --git a/matita/matita/matita.glade b/matita/matita/matita.glade index 0d80fe22c..5c343f0af 100644 --- a/matita/matita/matita.glade +++ b/matita/matita/matita.glade @@ -1291,19 +1291,6 @@ True - - - True - Displays a window helpful to drive automation - Auto GUI - True - - - gtk-media-pause - - - - True diff --git a/matita/matita/matitaAutoGui.ml b/matita/matita/matitaAutoGui.ml deleted file mode 100644 index 588dc5fec..000000000 --- a/matita/matita/matitaAutoGui.ml +++ /dev/null @@ -1,244 +0,0 @@ -(* Copyright (C) 2003, HELM Team. - * - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -type status = - Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list * - (int * Cic.term * int) list * - Cic.term Lazy.t list -let fake_goal = Cic.Implicit None;; -let fake_candidates = [];; - -let start = ref 0;; -let len = ref 10;; - - -let font_size = ref - (Helm_registry.get_opt_default Helm_registry.int - ~default:BuildTimeConf.default_font_size "matita.font_size") -;; - -let set_font_size n = font_size := n;; - -let pp ?(size=(!font_size)) c t = - let t = - ProofEngineReduction.replace - ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false) - ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:t - in - (if size > 0 then "" else "") ^ - (MatitaGtkMisc.escape_pango_markup - (ApplyTransformation.txt_of_cic_term ~map_unicode_to_tex:false - max_int [] c t))^ - (if size > 0 then "" else "") -;; -let pp_goal context x = - if x == fake_goal then "" else pp context x -;; -let pp_candidate context x = pp context (Lazy.force x) -let pp_candidate_tip context x = pp ~size:0 context (Lazy.force x) -let pp_candidate_type context x = - try - let ty, _ = - CicTypeChecker.type_of_aux' [] ~subst:[] - context (Lazy.force x) CicUniv.oblivion_ugraph - in - pp ~size:0 context ty - with CicUtil.Meta_not_found _ -> pp ~size:0 context (Lazy.force x) -;; - -let sublist start len l = - let rec aux pos len = function - | [] when pos < start -> aux (pos+1) len [] - | [] when len > 0 -> - (0,fake_goal, false, 0, fake_candidates) :: aux (pos+1) (len-1) [] - | [] (* when len <= 0 *) -> [] - | he::tl when pos < start -> aux (pos+1) len tl - | he::tl when pos >= start && len > 0 -> he::aux (pos+1) (len-1) tl - | he::tl (* when pos >= start && len <= 0 *) -> [] - in - aux 0 len l -;; - -let cell_of_candidate height context ?(active=false) g id c = - let tooltip = GData.tooltips () in (* should be only one isn't it? *) - let button = GButton.button () in - let l = GMisc.label ~markup:(pp_candidate context c) () in - button#add l#coerce; - button#misc#set_size_request ~height (); - if active then - button#misc#set_sensitive false; - let text = - "Follow/Prune computation of\n"^pp_candidate_tip context c^": "^ - pp_candidate_type context c - in - tooltip#set_tip ~text (button :> GObj.widget); - ignore(button#connect#clicked - (fun _ -> - let menu = GMenu.menu () in - let follow = GMenu.menu_item ~label:"Follow" () in - let prune = GMenu.menu_item ~label:"Prune" () in - ignore (follow#connect#activate - (fun _ -> HLog.warn (string_of_int id); Auto.give_hint id)); - ignore (prune#connect#activate - (fun _ -> HLog.warn (string_of_int id); Auto.give_prune_hint id)); - menu#append follow; - menu#append prune; - menu#popup 0 (GtkMain.Main.get_current_event_time ()))); - button -;; -let cell_of_goal height win_width context goal = - GMisc.label - ~markup:(pp_goal context goal) ~xalign:0.0 - ~width:(min (win_width * 30 / 100) 500) - ~line_wrap:false - ~ellipsize:`END - ~height - () -;; -let cell_of_row_header height n k id = - GMisc.label - ~markup:("" ^ string_of_int n ^ "(" ^ - string_of_int id ^ "|" ^ string_of_int k ^ ")") - ~line_wrap:true ~justify:`LEFT ~height ~width:80 () -;; -let cell_of_candidates height grey context goal cads = - let hbox = GPack.hbox () in - match cads with - | [] -> hbox - | (id,c)::tl -> - hbox#pack - (cell_of_candidate height ~active:grey - context goal id c :> GObj.widget); - List.iter - (fun (id,c) -> - hbox#pack (cell_of_candidate height context goal id c :> GObj.widget)) tl; - hbox -;; - -let elems_to_rows height context win_width (table : GPack.table) (or_list) = - let height = height / ((List.length or_list) + 1) in - let _ = - List.fold_left - (fun position (goal_id, goal, grey, depth, candidates) -> - table#attach ~left:0 ~top:position - (cell_of_row_header height (position + !start) - depth goal_id :> GObj.widget); - table#attach ~left:1 ~top:position ~fill:`BOTH - (cell_of_goal height win_width context goal :> GObj.widget); - table#attach ~left:2 ~top:position - (cell_of_candidates height grey context goal candidates :> GObj.widget); - position+1) - 0 or_list - in - () -;; - -let old_displayed_status = ref [];; -let old_size = ref 0;; - -let fill_win (win : MatitaGeneratedGui.autoWin) cb = -(* let init = Unix.gettimeofday () in *) - try - let (status : status) = cb () in - let win_size = win#toplevel#misc#allocation.Gtk.width in - let ctx, or_list, and_list, last_moves = status in - let displayed_status = - sublist !start !len - (or_list @ (List.map (fun (id,x,d) -> id,x,false,d,[]) and_list)) - in - if displayed_status <> !old_displayed_status || !old_size <> win_size then - begin - old_displayed_status := displayed_status; - old_size := win_size; -(* - win#labelLAST#set_text - (String.concat ";" (List.map (pp_candidate ctx) last_moves)); -*) - List.iter win#table#remove win#table#children; - let height = win#viewportAREA#misc#allocation.Gtk.height in - elems_to_rows height ctx win_size win#table displayed_status; -(* - Printf.eprintf - "REDRAW COST: %2.1f\n%!" (Unix.gettimeofday () -. init); -*) - end - with exn -> prerr_endline (Printexc.to_string exn); () -;; - -let auto_dialog elems = - let win = new MatitaGeneratedGui.autoWin () in - let width = Gdk.Screen.width () in - let height = Gdk.Screen.height () in - let main_w = width * 70 / 100 in - let main_h = height * 60 / 100 in - win#toplevel#resize ~width:main_w ~height:main_h; - win#check_widgets (); - win#table#set_columns 3; - win#table#set_col_spacings 6; - win#table#set_row_spacings 4; - ignore(win#buttonUP#connect#clicked - (fun _ -> start := max 0 (!start -1); fill_win win elems)); - ignore(win#buttonDOWN#connect#clicked - (fun _ -> incr start; fill_win win elems)); - ignore(win#buttonCLOSE#connect#clicked - (fun _ -> - Auto.pause false; - Auto.step (); - win#toplevel#destroy (); - GMain.Main.quit ())); - ignore(win#toplevel#event#connect#delete - (fun _ -> - Auto.pause false; - Auto.step (); - win#toplevel#destroy (); - GMain.Main.quit ();true)); - let redraw_callback _ = - fill_win win elems; - true - in - let redraw = GMain.Timeout.add ~ms:400 ~callback:redraw_callback in - ignore(win#buttonPAUSE#connect#clicked - (fun _ -> - Auto.pause true; - win#buttonPLAY#misc#set_sensitive true; - win#buttonPAUSE#misc#set_sensitive false;)); - ignore(win#buttonPLAY#connect#clicked - (fun _ -> - Auto.pause false; - Auto.step (); - win#buttonPLAY#misc#set_sensitive false; - win#buttonPAUSE#misc#set_sensitive true;)); - ignore(win#buttonNEXT#connect#clicked - (fun _ -> Auto.step ())); - Auto.pause true; - win#buttonPLAY#misc#set_sensitive true; - win#buttonPAUSE#misc#set_sensitive false; - fill_win win elems; - win#toplevel#show (); - GtkThread.main (); - GMain.Timeout.remove redraw; -;; - diff --git a/matita/matita/matitaAutoGui.mli b/matita/matita/matitaAutoGui.mli deleted file mode 100644 index eabf24aab..000000000 --- a/matita/matita/matitaAutoGui.mli +++ /dev/null @@ -1,33 +0,0 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(* $Id$ *) - -type status = - Cic.context * - (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list * - (int * Cic.term * int) list * Cic.term Lazy.t list -val auto_dialog : (unit -> status) -> unit -val set_font_size: int -> unit diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index 9271384c1..59f5c687f 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -1008,8 +1008,6 @@ class gui () = (fun _ -> let c = MatitaMathView.cicBrowser () in c#load (`About `Hints)); - connect_menu_item main#showAutoGuiMenuItem - (fun _ -> MatitaAutoGui.auto_dialog Auto.get_auto_status); connect_menu_item main#showTermGrammarMenuItem (fun _ -> let c = MatitaMathView.cicBrowser () in @@ -1379,8 +1377,7 @@ class gui () = method private updateFontSize () = self#sourceView#misc#modify_font_by_name - (sprintf "%s %d" BuildTimeConf.script_font font_size); - MatitaAutoGui.set_font_size font_size + (sprintf "%s %d" BuildTimeConf.script_font font_size) method increaseFontSize () = font_size <- font_size + 1; diff --git a/matita/matita/matitaWiki.ml b/matita/matita/matitaWiki.ml deleted file mode 100644 index 52d18f42a..000000000 --- a/matita/matita/matitaWiki.ml +++ /dev/null @@ -1,260 +0,0 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -(* $Id: matitacLib.ml 7090 2006-12-12 14:04:59Z fguidi $ *) - -open Printf - -open GrafiteTypes - -exception AttemptToInsertAnAlias - - -(** {2 Initialization} *) - -let grafite_status = (ref [] : GrafiteTypes.status list ref) - -let run_script is eval_function = - let grafite_status' = - match !grafite_status with - | s::_ -> s - | _ -> assert false - in - let cb = fun _ _ -> () in - let matita_debug = Helm_registry.get_bool "matita.debug" in - try - match eval_function grafite_status' is cb with - [] -> raise End_of_file - | (grafite_status'',None)::_ -> - grafite_status := grafite_status''::!grafite_status - | (s,Some _)::_ -> raise AttemptToInsertAnAlias - with - | GrafiteEngine.Drop - | End_of_file - | CicNotationParser.Parse_error _ - | HExtlib.Localized _ as exn -> raise exn - | exn -> - if not matita_debug then - HLog.error (snd (MatitaExcPp.to_string exn)) ; - raise exn - -let clean_exit n = - match !grafite_status with - [] -> exit n - | grafite_status::_ -> - let baseuri = grafite_status#baseuri in - LibraryClean.clean_baseuris ~verbose:false [baseuri]; - exit n - -let terminate n = - let terminator = String.make 1 (Char.chr 249) in - let prompt = - (match n with - None -> "-1" - | Some n -> string_of_int n) ^ terminator - in - print_endline prompt; - prerr_endline prompt -;; - -let outer_syntax_parser () = - let text = ref "" in - let tag = ref `Do in - let callbacks = - { XmlPushParser.default_callbacks with - XmlPushParser.start_element = - (Some - (fun name attrs -> - match name with - "pgip" -> () - | "doitem" -> tag := `Do - | "undoitem" -> tag := `Undo - | _ -> assert false)) ; - XmlPushParser.character_data = - (Some (fun s -> text := !text ^ s)) ; - XmlPushParser.end_element = - (Some - (function - "pgip" -> raise (XmlPushParser.Parse_error "EOC") - | "doitem" - | "undoitem" -> () - | _ -> assert false)) - } - in - let parse = XmlPushParser.create_parser callbacks in - try - XmlPushParser.parse parse (`Channel stdin) ; - raise End_of_file - with - XmlPushParser.Parse_error "no element found" -> raise End_of_file - | XmlPushParser.Parse_error "EOC" -> - match !tag with - `Do -> `Do !text - | `Undo -> - try - `Undo (int_of_string !text) - with - Failure _ -> assert false -;; - -let include_paths = - lazy (Helm_registry.get_list Helm_registry.string "matita.includes") -;; - -let rec interactive_loop () = - (* every loop is terminated by a terminator both on stdout and stderr *) - let interactive_loop n = terminate n; interactive_loop () in - try - match outer_syntax_parser () with - `Undo n -> - let rec drop = - function - 0,l -> l - | n,_::l -> drop (n-1,l) - | _,[] -> assert false - in - let to_be_dropped = List.length !grafite_status - n in - let safe_hd = function [] -> assert false | he::_ -> he in - let cur_grafite_status = safe_hd !grafite_status in - grafite_status := drop (to_be_dropped, !grafite_status) ; - let grafite_status = safe_hd !grafite_status in - LexiconSync.time_travel - ~present:cur_grafite_status ~past:grafite_status; - GrafiteSync.time_travel - ~present:cur_grafite_status ~past:grafite_status (); - interactive_loop (Some n) - | `Do command -> - let str = Ulexing.from_utf8_string command in - let watch_statuses grafite_status = - match grafite_status#proof_status with - GrafiteTypes.Incomplete_proof - {GrafiteTypes.proof = uri,metasenv,_subst,bo,ty,attrs ; - GrafiteTypes.stack = stack } -> - let open_goals = Continuationals.Stack.open_goals stack in - print_endline - (String.concat "\n" - (List.map - (fun i -> - ApplyTransformation.txt_of_cic_sequent 80 metasenv - ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex") - (List.find (fun (j,_,_) -> j=i) metasenv) - ) open_goals)) - | _ -> () - in - run_script str - (MatitaEngine.eval_from_stream ~first_statement_only:true - ~include_paths:(Lazy.force include_paths) ~watch_statuses) ; - interactive_loop (Some (List.length !grafite_status)) - with - | GrafiteEngine.Macro (floc,_) -> - let x, y = HExtlib.loc_of_floc floc in - HLog.error - (sprintf "A macro has been found in a script at %d-%d" x y); - interactive_loop None - | Sys.Break -> HLog.error "user break!"; interactive_loop None - | GrafiteTypes.Command_error _ -> interactive_loop None - | HExtlib.Localized (floc,CicNotationParser.Parse_error err) -> - let x, y = HExtlib.loc_of_floc floc in - HLog.error (sprintf "Parse error at %d-%d: %s" x y err); - interactive_loop None - | End_of_file as exn -> raise exn - | exn -> HLog.error (Printexc.to_string exn); interactive_loop None - - -let main () = - MatitaInit.initialize_all (); - HLog.set_log_callback - (fun tag msg -> - let s = - match tag with - `Debug -> "
Debug: " ^ msg ^ "

\n" - | `Message -> "
Info: " ^ msg ^ "

\n" - | `Warning -> "
Warn: " ^ msg ^ "

\n" - | `Error -> "
Error: " ^ msg ^ "

\n" - in - output_string stderr s; - flush stderr - ); - (* must be called after init since args are set by cmdline parsing *) - let system_mode = Helm_registry.get_bool "matita.system" in - let include_paths = - Helm_registry.get_list Helm_registry.string "matita.includes" in - grafite_status := [GrafiteSync.init (CicNotation2.load_notation ~include_paths - (new LexiconEngine.status) BuildTimeConf.core_notation_script) "cic:/matita/tests/"]; - Sys.catch_break true; - let origcb = HLog.get_log_callback () in - let origcb t s = origcb t ((if system_mode then "[S] " else "") ^ s) in - let newcb tag s = - match tag with - | `Debug -> () - | `Message | `Warning | `Error -> origcb tag s - in - HLog.set_log_callback newcb; - let matita_debug = Helm_registry.get_bool "matita.debug" in - try - (try - interactive_loop () - with - | End_of_file -> () - | GrafiteEngine.Drop -> clean_exit 1 - ); - let proof_status,moo_content_rev,lexicon_content_rev,dump = - match !grafite_status with - | s::_ -> - s#proof_status, s#moo_content_rev, - s#lstatus.LexiconEngine.lexicon_content_rev, s#dump - | _ -> assert false - in - if proof_status <> GrafiteTypes.No_proof then - begin - HLog.error - "there are still incomplete proofs at the end of the script"; - clean_exit 2 - end - else - begin - let baseuri = - (match !grafite_status with - [] -> assert false - | s::_ -> s)#baseuri - in - let moo_fname = - LibraryMisc.obj_file_of_baseuri - ~must_exist:false ~baseuri ~writable:true - in - let lexicon_fname= - LibraryMisc.lexicon_file_of_baseuri - ~must_exist:false ~baseuri ~writable:true - in - GrafiteMarshal.save_moo moo_fname moo_content_rev; - LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev; - NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) dump; - exit 0 - end - with - | exn -> - if matita_debug then raise exn; - clean_exit 3 diff --git a/matita/matita/matitac.ml b/matita/matita/matitac.ml index 83ab74439..5c8ea3738 100644 --- a/matita/matita/matitac.ml +++ b/matita/matita/matitac.ml @@ -68,7 +68,6 @@ let main () = let bin = Filename.basename Sys.argv.(0) in if Pcre.pmatch ~pat:"^matitadep" bin then Matitadep.main () else if Pcre.pmatch ~pat:"^matitaclean" bin then Matitaclean.main () - else if Pcre.pmatch ~pat:"^matitawiki" bin then MatitaWiki.main () else exit (main_compiler ()) ;;