sequents_viewer#load_logo;
cic_math_view#set_href_callback
(Some (fun uri ->
- let uri =
- try
- `Uri (UriManager.uri_of_string uri)
- with
- UriManager.IllFormedUri _ ->
- `NRef (NReference.reference_of_string uri)
- in
- (MatitaMathView.cicBrowser ())#load uri));
+ let uri = `NRef (NReference.reference_of_string uri) in
+ (MatitaMathView.cicBrowser ())#load uri));
let browser_observer _ = MatitaMathView.refresh_all_browsers () in
let sequents_observer grafite_status =
sequents_viewer#reset;
in
addDebugItem "dump aliases" (fun _ ->
let status = script#grafite_status in
- LexiconEngine.dump_aliases prerr_endline "" status);
+ GrafiteDisambiguate.dump_aliases prerr_endline "" status);
(* FG: DEBUGGING
addDebugItem "dump interpretations" (fun _ ->
let status = script#lexicon_status in
*)
addDebugSeparator ();
addDebugCheckbox "high level pretty printer" ~init:true
- (fun mi () -> CicMetaSubst.use_low_level_ppterm_in_context := mi#active);
+ (fun mi () -> assert false (* MATITA 1.0 *));
addDebugSeparator ();
addDebugItem "always show all disambiguation errors"
(fun _ -> MatitaGui.all_disambiguation_passes := true);
(fun mi () -> NCicRefiner.debug := mi#active; NCicUnification.debug :=
mi#active; MultiPassDisambiguator.debug := mi#active; NCicMetaSubst.debug := mi#active);
addDebugCheckbox "reduction logging"
- (fun mi () -> NCicReduction.debug := mi#active; CicReduction.ndebug := mi#active);
+ (fun mi () -> NCicReduction.debug := mi#active);
addDebugSeparator ();
addDebugItem "Expand virtuals"
(fun _ -> (MatitaScript.current ())#expandAllVirtuals);