src/Pure/PIDE/markup.ML
changeset 65313 347ed6219dab
parent 64677 8dc24130e8fe
child 66044 bd7516709051
equal deleted inserted replaced
65312:34d56ca5b548 65313:347ed6219dab
   192   val ML_statistics: Properties.entry
   192   val ML_statistics: Properties.entry
   193   val task_statistics: Properties.entry
   193   val task_statistics: Properties.entry
   194   val command_timing: Properties.entry
   194   val command_timing: Properties.entry
   195   val loading_theory: string -> Properties.T
   195   val loading_theory: string -> Properties.T
   196   val dest_loading_theory: Properties.T -> string option
   196   val dest_loading_theory: Properties.T -> string option
   197   val build_theories_result: string -> Properties.T
   197   val build_session_finished: Properties.T
   198   val print_operationsN: string
   198   val print_operationsN: string
   199   val print_operations: Properties.T
   199   val print_operations: Properties.T
   200   val debugger_state: string -> Properties.T
   200   val debugger_state: string -> Properties.T
   201   val debugger_output: string -> Properties.T
   201   val debugger_output: string -> Properties.T
   202   val simp_trace_panelN: string
   202   val simp_trace_panelN: string
   616 fun loading_theory name = [("function", "loading_theory"), ("name", name)];
   616 fun loading_theory name = [("function", "loading_theory"), ("name", name)];
   617 
   617 
   618 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
   618 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
   619   | dest_loading_theory _ = NONE;
   619   | dest_loading_theory _ = NONE;
   620 
   620 
   621 fun build_theories_result id = [("function", "build_theories_result"), ("id", id)];
   621 val build_session_finished = [("function", "build_session_finished")];
   622 
   622 
   623 val print_operationsN = "print_operations";
   623 val print_operationsN = "print_operations";
   624 val print_operations = [(functionN, print_operationsN)];
   624 val print_operations = [(functionN, print_operationsN)];
   625 
   625 
   626 
   626