src/Pure/General/markup.ML
changeset 43673 29eb1cd29961
parent 43665 573d1272f36d
child 43684 85388f5570c4
equal deleted inserted replaced
43672:e9f26e66692d 43673:29eb1cd29961
    90   val malformedN: string val malformed: T
    90   val malformedN: string val malformed: T
    91   val tokenN: string val token: Properties.T -> T
    91   val tokenN: string val token: Properties.T -> T
    92   val command_spanN: string val command_span: string -> T
    92   val command_spanN: string val command_span: string -> T
    93   val ignored_spanN: string val ignored_span: T
    93   val ignored_spanN: string val ignored_span: T
    94   val malformed_spanN: string val malformed_span: T
    94   val malformed_spanN: string val malformed_span: T
       
    95   val loaded_theoryN: string val loaded_theory: string -> T
    95   val elapsedN: string
    96   val elapsedN: string
    96   val cpuN: string
    97   val cpuN: string
    97   val gcN: string
    98   val gcN: string
    98   val timingN: string val timing: Timing.timing -> T
    99   val timingN: string val timing: Timing.timing -> T
    99   val subgoalsN: string
   100   val subgoalsN: string
   303 val (command_spanN, command_span) = markup_string "command_span" nameN;
   304 val (command_spanN, command_span) = markup_string "command_span" nameN;
   304 val (ignored_spanN, ignored_span) = markup_elem "ignored_span";
   305 val (ignored_spanN, ignored_span) = markup_elem "ignored_span";
   305 val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
   306 val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
   306 
   307 
   307 
   308 
       
   309 (* theory loader *)
       
   310 
       
   311 val (loaded_theoryN, loaded_theory) = markup_string "loaded_theory" nameN;
       
   312 
       
   313 
   308 (* timing *)
   314 (* timing *)
   309 
   315 
   310 val timingN = "timing";
   316 val timingN = "timing";
   311 val elapsedN = "elapsed";
   317 val elapsedN = "elapsed";
   312 val cpuN = "cpu";
   318 val cpuN = "cpu";