Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: symbol_explode.ML Sprache: SML

Original von: Isabelle^©

(*  Title:      Pure/General/symbol_explode.ML
    Author:     Makarius

String explode operation for Isabelle symbols (see also symbol.ML).
*)

structure Symbol: sig val explode: string -> string list end =
struct

fun is_ascii_letter c = #"A" <= c andalso c <= #"Z" orelse #"a" <= c andalso c <= #"z";
fun is_ascii_letdig c =
  is_ascii_letter c orelse #"0" <= c andalso c <= #"9" orelse c = #"_" orelse c = #"'";

fun is_utf8 c = c >= #"\128";
fun is_utf8_trailer c = #"\128" <= c andalso c < #"\192";
fun is_utf8_control c = #"\128" <= c andalso c < #"\160";

fun explode string =
  let
    fun char i = String.sub (string, i);
    fun string_range i j = String.substring (string, i, j - i);

    val n = size string;
    fun test pred i = i < n andalso pred (char i);
    fun many pred i = if test pred i then many pred (i + 1) else i;
    fun maybe pred i = if test pred i then i + 1 else i;
    fun maybe_char c = maybe (fn c' => c = c');
    fun maybe_ascii_id i = if test is_ascii_letter i then many is_ascii_letdig (i + 1) else i;

    fun scan i =
      if i < n then
        let val ch = char i in
          (*encoded newline*)
          if ch = #"\^M" then "\n" :: scan (maybe_char #"\n" (i + 1))
          (*pseudo utf8: encoded ascii control*)
          else if ch = #"\192" andalso
            test is_utf8_control (i + 1) andalso not (test is_utf8 (i + 2))
          then chr (Char.ord (char (i + 1)) - 128) :: scan (i + 2)
          (*utf8*)
          else if is_utf8 ch then
            let val j = many is_utf8_trailer (i + 1)
            in string_range i j :: scan j end
          (*named symbol*)
          else if ch = #"\\" andalso test (fn c => c = #"<") (i + 1) then
            let val j = (i + 2) |> maybe_char #"^" |> maybe_ascii_id |> maybe_char #">"
            in string_range i j :: scan j end
          (*single character*)
          else String.str ch :: scan (i + 1)
        end
      else [];
  in scan 0 end;

end;

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.