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 \
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:
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 \
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:
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
matitacLib.mli \
matitaInit.mli \
matitaGtkMisc.mli \
- matitaAutoGui.mli \
virtuals.mli \
matitaScript.mli \
predefined_virtuals.mli \
matitaExcPp.mli \
matitacLib.mli \
matitaInit.mli \
- matitaWiki.mli \
$(NULL)
MAINCMLI = \
matitadep.mli \
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
$(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
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
$(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 \
$(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 $< $@
+++ /dev/null
-(* 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)
-
<property name="use_underline">True</property>
</widget>
</child>
- <child>
- <widget class="GtkImageMenuItem" id="showAutoGuiMenuItem">
- <property name="visible">True</property>
- <property name="tooltip" translatable="yes">Displays a window helpful to drive automation</property>
- <property name="label" translatable="yes">Auto GUI</property>
- <property name="use_underline">True</property>
- <child internal-child="image">
- <widget class="GtkImage" id="menu-item-image19">
- <property name="stock">gtk-media-pause</property>
- </widget>
- </child>
- </widget>
- </child>
<child>
<widget class="GtkMenuItem" id="showTermGrammarMenuItem">
<property name="visible">True</property>
+++ /dev/null
-(* 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 "<span font_desc=\""^string_of_int size^"\">" else "") ^
- (MatitaGtkMisc.escape_pango_markup
- (ApplyTransformation.txt_of_cic_term ~map_unicode_to_tex:false
- max_int [] c t))^
- (if size > 0 then "</span>" 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:("<span stretch=\"ultracondensed\">" ^ string_of_int n ^ "<sub>(" ^
- string_of_int id ^ "|" ^ string_of_int k ^ ")</sub></span>")
- ~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;
-;;
-
+++ /dev/null
-(* 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
(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
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;
+++ /dev/null
-(* 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 -> "<div style='color:blue'>Debug: " ^ msg ^ "</div><br/>\n"
- | `Message -> "<div style='color:green'>Info: " ^ msg ^ "</div><br/>\n"
- | `Warning -> "<div style='color:yellow'>Warn: " ^ msg ^ "</div><br/>\n"
- | `Error -> "<div style='color:red'>Error: " ^ msg ^ "</div><br/>\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
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 ())
;;
projects / helm.git / commitdiff