src/Pure/Isar/outer_lex.ML
changeset 25642 ebdff0dca2a5
parent 25582 655453e635c4
child 26004 2abb3005660f
equal deleted inserted replaced
25641:615aecd485ad 25642:ebdff0dca2a5
    26   val is_comment: token -> bool
    26   val is_comment: token -> bool
    27   val is_begin_ignore: token -> bool
    27   val is_begin_ignore: token -> bool
    28   val is_end_ignore: token -> bool
    28   val is_end_ignore: token -> bool
    29   val is_blank: token -> bool
    29   val is_blank: token -> bool
    30   val is_newline: token -> bool
    30   val is_newline: token -> bool
       
    31   val val_of: token -> string
    31   val unparse: token -> string
    32   val unparse: token -> string
    32   val text_of: token -> string * string
    33   val text_of: token -> string * string
    33   val val_of: token -> string
       
    34   val is_sid: string -> bool
    34   val is_sid: string -> bool
    35   val !!! : string -> (Position.T * 'a -> 'b) -> Position.T * 'a -> 'b
    35   val !!! : string -> (Position.T * 'a -> 'b) -> Position.T * 'a -> 'b
    36   val incr_line: ('a -> 'b * 'c) -> Position.T * 'a -> 'b * (Position.T * 'c)
    36   val incr_line: ('a -> 'b * 'c) -> Position.T * 'a -> 'b * (Position.T * 'c)
    37   val keep_line: ('a -> 'b * 'c) -> Position.T * 'a -> 'b * (Position.T * 'c)
    37   val keep_line: ('a -> 'b * 'c) -> Position.T * 'a -> 'b * (Position.T * 'c)
    38   val scan_blank: Position.T * Symbol.symbol list
    38   val scan_blank: Position.T * Symbol.symbol list
   141   | is_newline _ = false;
   141   | is_newline _ = false;
   142 
   142 
   143 
   143 
   144 (* token content *)
   144 (* token content *)
   145 
   145 
       
   146 fun val_of (Token (_, (_, x))) = x;
       
   147 fun token_leq (tok1, tok2) = val_of tok1 <= val_of tok2;
       
   148 
   146 fun escape q =
   149 fun escape q =
   147   implode o map (fn s => if s = q orelse s = "\\" then "\\" ^ s else s) o Symbol.explode;
   150   implode o map (fn s => if s = q orelse s = "\\" then "\\" ^ s else s) o Symbol.explode;
   148 
   151 
   149 fun unparse (Token (_, (kind, x))) =
   152 fun unparse (Token (_, (kind, x))) =
   150   (case kind of
   153   (case kind of
   151     String => x |> quote o escape "\""
   154     String => x |> quote o escape "\""
   152   | AltString => x |> enclose "`" "`" o escape "`"
   155   | AltString => x |> enclose "`" "`" o escape "`"
   153   | Verbatim => x |> enclose "{*" "*}"
   156   | Verbatim => x |> enclose "{*" "*}"
   154   | Comment => x |> enclose "(*" "*)"
   157   | Comment => x |> enclose "(*" "*)"
   155   | Malformed => Output.escape_malformed x
   158   | Malformed => Output.escape (translate_string Output.output x)
   156   | Sync => ""
   159   | Sync => ""
   157   | EOF => ""
   160   | EOF => ""
   158   | _ => x);
   161   | _ => x);
   159 
   162 
   160 fun text_of tok =
   163 fun text_of tok =
   161   if is_semicolon tok then ("terminator", "")
   164   if is_semicolon tok then ("terminator", "")
   162   else
   165   else
   163     let
   166     let
   164       val k = str_of_kind (kind_of tok);
   167       val k = str_of_kind (kind_of tok);
   165       val txt = unparse tok;
   168       val s = unparse tok
   166       val s =
   169         handle ERROR _ => Symbol.separate_chars (val_of tok);
   167         if can Symbol.explode txt
       
   168         then txt else Output.escape_malformed txt;
       
   169     in
   170     in
   170       if s = "" then (k, "")
   171       if s = "" then (k, "")
   171       else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ s, "")
   172       else if size s < 40 andalso not (exists_string (fn c => c = "\n") s) then (k ^ " " ^ s, "")
   172       else (k, s)
   173       else (k, s)
   173     end;
   174     end;
   174 
       
   175 fun val_of (Token (_, (_, x))) = x;
       
   176 
       
   177 fun token_leq (Token (_, (_, x)), Token (_, (_, x'))) = x <= x';
       
   178 
   175 
   179 
   176 
   180 
   177 
   181 (** scanners **)
   178 (** scanners **)
   182 
   179