src/Pure/PIDE/isabelle_markup.ML
changeset 48768 abc45de5bb22
parent 48756 1c843142758e
child 48927 ef462b5558eb
equal deleted inserted replaced
48767:7f0c469cc796 48768:abc45de5bb22
    93   val serialN: string
    93   val serialN: string
    94   val legacyN: string val legacy: Markup.T
    94   val legacyN: string val legacy: Markup.T
    95   val promptN: string val prompt: Markup.T
    95   val promptN: string val prompt: Markup.T
    96   val reportN: string val report: Markup.T
    96   val reportN: string val report: Markup.T
    97   val no_reportN: string val no_report: Markup.T
    97   val no_reportN: string val no_report: Markup.T
    98   val messageN: string
    98   val badN: string val bad: Markup.T
    99   val badN: string val bad: string -> Markup.T
       
   100   val functionN: string
    99   val functionN: string
   101   val assign_execs: Properties.T
   100   val assign_execs: Properties.T
   102   val removed_versions: Properties.T
   101   val removed_versions: Properties.T
   103   val invoke_scala: string -> string -> Properties.T
   102   val invoke_scala: string -> string -> Properties.T
   104   val cancel_scala: string -> Properties.T
   103   val cancel_scala: string -> Properties.T
   285 val (promptN, prompt) = markup_elem "prompt";
   284 val (promptN, prompt) = markup_elem "prompt";
   286 
   285 
   287 val (reportN, report) = markup_elem "report";
   286 val (reportN, report) = markup_elem "report";
   288 val (no_reportN, no_report) = markup_elem "no_report";
   287 val (no_reportN, no_report) = markup_elem "no_report";
   289 
   288 
   290 val messageN = "message"
   289 val (badN, bad) = markup_elem "bad";
   291 val badN = "bad"
       
   292 
       
   293 fun bad "" = (badN, [])
       
   294   | bad msg = (badN, [(messageN, msg)]);
       
   295 
   290 
   296 
   291 
   297 (* protocol message functions *)
   292 (* protocol message functions *)
   298 
   293 
   299 val functionN = "function"
   294 val functionN = "function"