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,[]