src/Pure/Isar/toplevel.ML
changeset 11894 39a3ece43772
parent 10324 498999fd7c37
child 12009 cbd35a736954
equal deleted inserted replaced
11893:6b9e8820d4de 11894:39a3ece43772
   124   | print_current_node prt (State (Some (node, _))) = prt (History.current node);
   124   | print_current_node prt (State (Some (node, _))) = prt (History.current node);
   125 
   125 
   126 val print_state_context = print_current_node print_node_ctxt;
   126 val print_state_context = print_current_node print_node_ctxt;
   127 
   127 
   128 fun print_state_default prf_only state =
   128 fun print_state_default prf_only state =
   129   let val ref (begin_state, end_state, _) = Goals.current_goals_markers in
   129   let val ref (begin_state, end_state, _) = Display.current_goals_markers in
   130     if begin_state = "" then () else writeln begin_state;
   130     if begin_state = "" then () else writeln begin_state;
   131     print_current_node (print_node prf_only) state;
   131     print_current_node (print_node prf_only) state;
   132     if end_state = "" then () else writeln end_state
   132     if end_state = "" then () else writeln end_state
   133   end;
   133   end;
   134 
   134