let status,cmd = disambiguate_command status (text,prefix_len,cmd) in
let status,uris =
match cmd with
+ | GrafiteAst.Print (_,"proofterm") ->
+ let _,_,p,_ = GrafiteTypes.get_current_proof status in
+ print_endline (AutoTactic.pp_proofterm p);
+ status,[]
+ | GrafiteAst.Print (_,_) -> status,[]
| GrafiteAst.Default (loc, what, uris) as cmd ->
LibraryObjects.set_default what uris;
GrafiteTypes.add_moo_content [cmd] status,[]
LibraryClean.clean_baseuris [value];
assert (Http_getter_storage.is_empty value);
end;
- HExtlib.mkdir
- (Filename.dirname (Http_getter.filename ~writable:true (value ^
- "/foo.con")));
+ if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk"
+ ~default:false)
+ then
+ HExtlib.mkdir
+ (Filename.dirname (Http_getter.filename ~writable:true (value ^
+ "/foo.con")));
end;
GrafiteTypes.set_option status name value,[]
| GrafiteAst.Drop loc -> raise Drop