let xmlpres = mpres_document pres_sequent in
Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres
+let ntxt_of_cic_sequent ~map_unicode_to_tex size status metasenv subst sequent =
+ let content_sequent,ids_to_refs =
+ NTermCicContent.nmap_sequent status ~metasenv ~subst sequent in
+ let pres_sequent =
+ Sequent2pres.nsequent2pres ids_to_refs subst content_sequent in
+ let pres_sequent = CicNotationPres.mpres_of_box pres_sequent in
+ BoxPp.render_to_string ~map_unicode_to_tex
+ (function x::_ -> x | _ -> assert false) size pres_sequent
+
let mml_of_cic_object obj =
let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses)
Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres
;;
-let txt_of_cic_sequent ~map_unicode_to_tex size metasenv sequent =
+let ntxt_of_cic_object ~map_unicode_to_tex size status obj =
+ let cobj,ids_to_nrefs = NTermCicContent.nmap_obj status obj in
+ let pres_sequent = Content2pres.ncontent2pres ~ids_to_nrefs cobj in
+ let pres_sequent = CicNotationPres.mpres_of_box pres_sequent in
+ BoxPp.render_to_string ~map_unicode_to_tex
+ (function x::_ -> x | _ -> assert false) size pres_sequent
+;;
+
+let txt_of_cic_sequent_all ~map_unicode_to_tex size metasenv sequent =
let unsh_sequent,(asequent,ids_to_terms,
ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses)
=
let content_sequent = Acic2content.map_sequent asequent in
let pres_sequent =
CicNotationPres.mpres_of_box
- (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent)
- in
+ (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent) in
+ let txt =
BoxPp.render_to_string ~map_unicode_to_tex
(function x::_ -> x | _ -> assert false) size pres_sequent
+ in
+ (txt,
+ unsh_sequent,
+ (asequent,
+ (ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)))
+
+let txt_of_cic_sequent ~map_unicode_to_tex size metasenv sequent =
+ let txt,_,_ = txt_of_cic_sequent_all ~map_unicode_to_tex size metasenv sequent
+ in txt
+;;
let txt_of_cic_sequent_conclusion ~map_unicode_to_tex ~output_type size
metasenv sequent =
| false ->
CicNotation.set_active_notations []
-let txt_of_cic_object
+let txt_of_cic_object_all
~map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas n params obj
=
let get_aobj obj =
try
- let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ =
+ let
+ aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses =
Cic2acic.acic_object_of_cic_object obj
in
- aobj, ids_to_inner_sorts, ids_to_inner_types
+ aobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
+ ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses
with
| E.Object_not_found uri ->
let msg = "txt_of_cic_object: object not found: " ^ UM.string_of_uri uri in
let msg = "txt_of_cic_object: " ^ Printexc.to_string e in
failwith msg
in
+ (*MATITA1.0
if List.mem G.IPProcedural params then begin
Procedural2.debug := A2P.is_debug 1 params;
(*
let _ = ProceduralTeX.tex_of_obj Format.std_formatter obj in
*)
- let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in
+ let aobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
+ ids_to_inner_types,ids_to_conjectures,ids_to_hypothesis = get_aobj obj in
let term_pp = term2pres ~map_unicode_to_tex (n - 8) ids_to_inner_sorts in
let lazy_term_pp = term_pp in
let obj_pp = CicNotationPp.pp_obj term_pp in
~ids_to_inner_sorts ~ids_to_inner_types ~info params aobj
in
String.concat "" (List.map aux script) ^ "\n\n"
- end else
- let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in
+ end else *)
+ let aobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
+ ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses = get_aobj obj in
let cobj =
Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj
in
Content2pres.content2pres
?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts cobj
in
- remove_closed_substs (
+ let txt =
+ remove_closed_substs (
BoxPp.render_to_string ~map_unicode_to_tex
(function _::x::_ -> x | _ -> assert false) n
(CicNotationPres.mpres_of_box bobj)
^ "\n\n"
- )
+ )
+ in
+ (txt,(aobj,
+ (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses,
+ ids_to_inner_sorts,ids_to_inner_types)))
+
+let txt_of_cic_object
+ ~map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas n params obj
+=
+ let txt,_ = txt_of_cic_object_all
+ ~map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas n params obj
+ in txt
let cic_prefix = Str.regexp_string "cic:/"
let matita_prefix = Str.regexp_string "cic:/matita/"
int * NCic.conjecture -> (* sequent *)
Gdome.document (* Math ML *)
+val ntxt_of_cic_sequent:
+ map_unicode_to_tex:bool -> int ->
+ #NCicCoercion.status ->
+ NCic.metasenv -> NCic.substitution -> (* metasenv, substitution *)
+ int * NCic.conjecture -> (* sequent *)
+ string (* text *)
+
val mml_of_cic_object:
Cic.obj -> (* object *)
Gdome.document * (* Math ML *)
val nmml_of_cic_object: #NCicCoercion.status -> NCic.obj -> Gdome.document
+val ntxt_of_cic_object:
+ map_unicode_to_tex:bool -> int -> #NCicCoercion.status -> NCic.obj -> string
+
+val txt_of_cic_sequent_all:
+ map_unicode_to_tex:bool -> int ->
+ Cic.metasenv -> (* metasenv *)
+ Cic.conjecture -> (* sequent *)
+ string * (* text *)
+ Cic.conjecture * (* unshared sequent *)
+ (Cic.annconjecture * (* annsequent *)
+ ((Cic.id, Cic.term) Hashtbl.t * (* id -> term *)
+ (Cic.id, Cic.id option) Hashtbl.t * (* id -> father id *)
+ (Cic.id, Cic.hypothesis) Hashtbl.t * (* id -> hypothesis *)
+ (Cic.id, Cic2acic.sort_kind) Hashtbl.t)) (* ids_to_inner_sorts *)
+
val txt_of_cic_term:
map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.context -> Cic.term ->
string
int -> GrafiteAst.inline_param list -> Cic.obj ->
string
+val txt_of_cic_object_all:
+ map_unicode_to_tex:bool ->
+ ?skip_thm_and_qed:bool -> ?skip_initial_lambdas:int ->
+ int -> GrafiteAst.inline_param list -> Cic.obj ->
+ string * (* text *)
+ (Cic.annobj * (* annobj *)
+ ((Cic.id, Cic.term) Hashtbl.t * (* id -> term *)
+ (Cic.id, Cic.id option) Hashtbl.t * (* id -> father id *)
+ (Cic.id, Cic.conjecture) Hashtbl.t * (* id -> conjecture *)
+ (Cic.id, Cic.hypothesis) Hashtbl.t * (* id -> hypothesis *)
+ (Cic.id, Cic2acic.sort_kind) Hashtbl.t * (* ids_to_inner_sorts *)
+ (Cic.id, Cic2acic.anntypes) Hashtbl.t)) (* ids_to_inner_types *)
+
(* params, uri or baseuri *)
val txt_of_inline_macro:
map_unicode_to_tex:bool -> GrafiteAst.inline_param list -> string ->
~qualifiedName:(Gdome.domString "box") ~doctype:None)
(** shown for goals closed by side effects *)
-let closed_goal_mathml = lazy (
- domImpl#createDocumentFromURI ~uri:BuildTimeConf.closed_xml ())
+let closed_goal_mathml = lazy "chiuso per side effect..."
(* ids_to_terms should not be passed here, is just for debugging *)
let find_root_id annobj id ids_to_father_ids ids_to_terms ids_to_inner_types =
class clickableMathView obj =
let text_width = 80 in
object (self)
+ inherit GSourceView2.source_view obj
+
+ method has_selection = (assert false : bool)
+ method strings_of_selection = (assert false : (paste_kind * string) list)
+ method update_font_size = (assert false : unit)
+ method set_href_callback = (function _ -> () : (string -> unit) option -> unit)
+ method private set_cic_info = (function _ -> () : (Cic.conjecture option * (Cic.id, Cic.term) Hashtbl.t *
+ (Cic.id, Cic.hypothesis) Hashtbl.t *
+ (Cic.id, Cic.id option) Hashtbl.t * ('a, 'b) Hashtbl.t * 'c option) option -> unit)
+ (* dal widget di Luca *)
+ method load_root ~root =
+ self#buffer#delete ~start:(self#buffer#get_iter `START)
+ ~stop:(self#buffer#get_iter `END);
+ self#buffer#insert root
+ method remove_selections = (() : unit)
+ method set_selection = (fun _ -> () : Gdome.element option -> unit)
+ method get_selections = (assert false : Gdome.element list)
+ method set_font_size font_size =
+ self#misc#modify_font_by_name
+ (sprintf "%s %d" BuildTimeConf.script_font font_size)
+
+(* MATITA1.0
inherit GMathViewAux.multi_selection_math_view obj
val mutable href_callback: (string -> unit) option = None
paste_kind, HExtlib.unopt (self#string_of_selection ~paste_kind))
[ `Term; `Pattern ]
with Failure _ -> failwith "no selection"
-
+*)
end
+open GtkSourceView2
+
let clickableMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity =
+ SourceView.make_params [] ~cont:(
+ GtkText.View.make_params ~cont:(
+ GContainer.pack_container ~create:(fun pl ->
+ let obj = SourceView.new_ () in
+ Gobject.set_params (Gobject.try_cast obj "GtkSourceView") pl;
+ new clickableMathView obj)))
+ (* MATITA1.0
GtkBase.Widget.size_params
- ~cont:(OgtkMathViewProps.pack_return (fun p ->
- OgtkMathViewProps.set_params
- (new clickableMathView (GtkMathViewProps.MathView_GMetaDOM.create p))
+ ~cont:(OgtkSourceView2Props.pack_return (fun p ->
+ OgtkSourceView2Props.set_params
+ (new clickableMathView (GtkSourceView2Props.MathView_GMetaDOM.create p))
~font_size:None ~log_verbosity:None))
[]
+ *)
class cicMathView obj =
object (self)
method load_sequent metasenv metano =
let sequent = CicUtil.lookup_meta metano metasenv in
- let (mathml, unsh_sequent,
+ let (txt, unsh_sequent,
(_, (ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_ )))
=
- ApplyTransformation.mml_of_cic_sequent metasenv sequent
+ ApplyTransformation.txt_of_cic_sequent_all
+ ~map_unicode_to_tex:false 80 (*MATITA 1.0??*) metasenv sequent
in
self#set_cic_info
(Some (Some unsh_sequent,
ids_to_terms, ids_to_hypotheses, ids_to_father_ids,
Hashtbl.create 1, None));
+ (*MATITA 1.0
if BuildTimeConf.debug then begin
let name =
"/tmp/sequent_viewer_" ^ string_of_int (Unix.getuid ()) ^ ".xml" in
HLog.debug ("load_sequent: dumping MathML to ./" ^ name);
- ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ())
- end;
- self#load_root ~root:mathml#get_documentElement
+ ignore (domImpl#saveDocumentToFile ~name ~doc:txt ())
+ end; *)
+ self#load_root ~root:txt
method nload_sequent:
'status. #NCicCoercion.status as 'status -> NCic.metasenv ->
NCic.substitution -> int -> unit
= fun status metasenv subst metano ->
let sequent = List.assoc metano metasenv in
- let mathml =
- ApplyTransformation.nmml_of_cic_sequent status metasenv subst
- (metano,sequent)
+ let txt =
+ ApplyTransformation.ntxt_of_cic_sequent
+ ~map_unicode_to_tex:false 80 status metasenv subst (metano,sequent)
in
- if BuildTimeConf.debug then begin
+ (* MATITA 1.0 if BuildTimeConf.debug then begin
let name =
"/tmp/sequent_viewer_" ^ string_of_int (Unix.getuid ()) ^ ".xml" in
HLog.debug ("load_sequent: dumping MathML to ./" ^ name);
ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ())
- end;
- self#load_root ~root:mathml#get_documentElement
+ end;*)
+ self#load_root ~root:txt
method load_object obj =
let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *)
- let (mathml,
+ let (txt,
(annobj, (ids_to_terms, ids_to_father_ids, _, ids_to_hypotheses, _, ids_to_inner_types)))
=
- ApplyTransformation.mml_of_cic_object obj
+ ApplyTransformation.txt_of_cic_object_all ~map_unicode_to_tex:false
+ 80 [] obj
in
self#set_cic_info
(Some (None, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj));
(match current_mathml with
| Some current_mathml when use_diff ->
+assert false (*MATITA1.0
self#freeze;
XmlDiff.update_dom ~from:current_mathml mathml;
- self#thaw
+ self#thaw*)
| _ ->
- if BuildTimeConf.debug then begin
+ (* MATITA1.0 if BuildTimeConf.debug then begin
let name =
"/tmp/cic_browser_" ^ string_of_int (Unix.getuid ()) ^ ".xml" in
HLog.debug ("cic_browser: dumping MathML to ./" ^ name);
ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ())
- end;
- self#load_root ~root:mathml#get_documentElement;
- current_mathml <- Some mathml);
+ end;*)
+ self#load_root ~root:txt;
+ current_mathml <- Some txt);
method load_nobject :
'status. #NCicCoercion.status as 'status -> NCic.obj -> unit
= fun status obj ->
- let mathml = ApplyTransformation.nmml_of_cic_object status obj in
+ let txt = ApplyTransformation.ntxt_of_cic_object ~map_unicode_to_tex:false
+ 80 status obj in
(*
self#set_cic_info
(Some (None, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj));
self#thaw
| _ ->
*)
- if BuildTimeConf.debug then begin
+ (* MATITA1.0 if BuildTimeConf.debug then begin
let name =
"/tmp/cic_browser_" ^ string_of_int (Unix.getuid ()) ^ ".xml" in
HLog.debug ("cic_browser: dumping MathML to ./" ^ name);
ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ())
- end;
- self#load_root ~root:mathml#get_documentElement;
+ end;*)
+ self#load_root ~root:txt;
(*current_mathml <- Some mathml*)(*)*);
end
cicMathView#nload_sequent status menv subst goal)
| Stack.Closed goal ->
let doc = Lazy.force closed_goal_mathml in
- cicMathView#load_root ~root:doc#get_documentElement);
+ cicMathView#load_root ~root:doc);
(try
cicMathView#set_selection None;
List.assoc goal_switch goal2win ()
end
(** constructors *)
-
type 'widget constructor =
- ?hadjustment:GData.adjustment ->
- ?vadjustment:GData.adjustment ->
- ?font_size:int ->
- ?log_verbosity:int ->
- ?width:int ->
- ?height:int ->
- ?packing:(GObj.widget -> unit) ->
- ?show:bool ->
- unit ->
- 'widget
+ ?hadjustment:GData.adjustment ->
+ ?vadjustment:GData.adjustment ->
+ ?font_size:int ->
+ ?log_verbosity:int ->
+ ?auto_indent:bool ->
+ ?highlight_current_line:bool ->
+ ?indent_on_tab:bool ->
+ ?indent_width:int ->
+ ?insert_spaces_instead_of_tabs:bool ->
+ ?right_margin_position:int ->
+ ?show_line_marks:bool ->
+ ?show_line_numbers:bool ->
+ ?show_right_margin:bool ->
+ ?smart_home_end:SourceView2Enums.source_smart_home_end_type ->
+ ?tab_width:int ->
+ ?editable:bool ->
+ ?cursor_visible:bool ->
+ ?justification:GtkEnums.justification ->
+ ?wrap_mode:GtkEnums.wrap_mode ->
+ ?accepts_tab:bool ->
+ ?border_width:int ->
+ ?width:int ->
+ ?height:int ->
+ ?packing:(GObj.widget -> unit) ->
+ ?show:bool -> unit ->
+ 'widget
let cicMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity =
+ SourceView.make_params [] ~cont:(
+ GtkText.View.make_params ~cont:(
+ GContainer.pack_container ~create:(fun pl ->
+ let obj = SourceView.new_ () in
+ Gobject.set_params (Gobject.try_cast obj "GtkSourceView") pl;
+ new cicMathView obj)))
+(* MATITA 1.0
GtkBase.Widget.size_params
~cont:(OgtkMathViewProps.pack_return (fun p ->
OgtkMathViewProps.set_params
(new cicMathView (GtkMathViewProps.MathView_GMetaDOM.create p))
~font_size ~log_verbosity))
[]
+*)
let blank_uri = BuildTimeConf.blank_uri
let current_proof_uri = BuildTimeConf.current_proof_uri
method private blank () =
self#_showMath;
- mathView#load_root (Lazy.force empty_mathml)#get_documentElement
+ mathView#load_root ""
method private _loadCheck term =
failwith "not implemented _loadCheck";
(self#get_browser reuse)#load entry
method screenshot status sequents metasenv subst (filename as ofn) =
+ () (*MATITA 1.0
let w = GWindow.window ~title:"screenshot" () in
let width = 500 in
let height = 2000 in
List.iter (fun x,_ -> Sys.remove x) filenames;
List.iter Sys.remove (List.flatten items);
w#destroy ();
+ *)
end
let refresh_all_browsers () =
projects / helm.git / commitdiff