src/Pure/Isar/outer_lex.ML
changeset 25582 655453e635c4
parent 25579 22869d9d545b
child 25642 ebdff0dca2a5
equal deleted inserted replaced
25581:f2b137c3e725 25582:655453e635c4
   160 fun text_of tok =
   160 fun text_of tok =
   161   if is_semicolon tok then ("terminator", "")
   161   if is_semicolon tok then ("terminator", "")
   162   else
   162   else
   163     let
   163     let
   164       val k = str_of_kind (kind_of tok);
   164       val k = str_of_kind (kind_of tok);
   165       val s = unparse tok;
   165       val txt = unparse tok;
       
   166       val s =
       
   167         if can Symbol.explode txt
       
   168         then txt else Output.escape_malformed txt;
   166     in
   169     in
   167       if s = "" then (k, "")
   170       if s = "" then (k, "")
   168       else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ s, "")
   171       else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ s, "")
   169       else (k, s)
   172       else (k, s)
   170     end;
   173     end;