src/Pure/PIDE/markup.ML
changeset 66873 9953ae603a23
parent 66379 6392766f3c25
child 67000 1698e9ccef2d
equal deleted inserted replaced
66872:69afe45a6062 66873:9953ae603a23
   192   val invoke_scala: string -> string -> Properties.T
   192   val invoke_scala: string -> string -> Properties.T
   193   val cancel_scala: string -> Properties.T
   193   val cancel_scala: string -> Properties.T
   194   val ML_statistics: Properties.entry
   194   val ML_statistics: Properties.entry
   195   val task_statistics: Properties.entry
   195   val task_statistics: Properties.entry
   196   val command_timing: Properties.entry
   196   val command_timing: Properties.entry
       
   197   val theory_timing: Properties.entry
   197   val loading_theory: string -> Properties.T
   198   val loading_theory: string -> Properties.T
   198   val dest_loading_theory: Properties.T -> string option
   199   val dest_loading_theory: Properties.T -> string option
   199   val build_session_finished: Properties.T
   200   val build_session_finished: Properties.T
   200   val print_operationsN: string
   201   val print_operationsN: string
   201   val print_operations: Properties.T
   202   val print_operations: Properties.T
   617 
   618 
   618 val task_statistics = (functionN, "task_statistics");
   619 val task_statistics = (functionN, "task_statistics");
   619 
   620 
   620 val command_timing = (functionN, "command_timing");
   621 val command_timing = (functionN, "command_timing");
   621 
   622 
       
   623 val theory_timing = (functionN, "theory_timing");
       
   624 
   622 fun loading_theory name = [("function", "loading_theory"), ("name", name)];
   625 fun loading_theory name = [("function", "loading_theory"), ("name", name)];
   623 
   626 
   624 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
   627 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
   625   | dest_loading_theory _ = NONE;
   628   | dest_loading_theory _ = NONE;
   626 
   629