uniform Markup.empty/Markup.Empty in ML and Scala;
authorwenzelm
Wed Aug 18 11:02:47 2010 +0200 (2010-08-18 ago)
changeset 38474e498dc2eb576
parent 38473 bd96f2a5beb0
child 38475 1dd4f545ac24
uniform Markup.empty/Markup.Empty in ML and Scala;
src/Pure/General/markup.ML
src/Pure/General/markup.scala
src/Pure/General/pretty.ML
src/Pure/General/xml.ML
src/Pure/General/yxml.ML
src/Pure/ML/ml_lex.ML
src/Pure/Syntax/lexicon.ML
src/Pure/Thy/thy_syntax.ML
     1.1 --- a/src/Pure/General/markup.ML	Tue Aug 17 23:23:29 2010 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Wed Aug 18 11:02:47 2010 +0200
     1.3 @@ -9,8 +9,8 @@
     1.4    val parse_int: string -> int
     1.5    val print_int: int -> string
     1.6    type T = string * Properties.T
     1.7 -  val none: T
     1.8 -  val is_none: T -> bool
     1.9 +  val empty: T
    1.10 +  val is_empty: T -> bool
    1.11    val properties: Properties.T -> T -> T
    1.12    val nameN: string
    1.13    val name: string -> T -> T
    1.14 @@ -142,10 +142,10 @@
    1.15  
    1.16  type T = string * Properties.T;
    1.17  
    1.18 -val none = ("", []);
    1.19 +val empty = ("", []);
    1.20  
    1.21 -fun is_none ("", _) = true
    1.22 -  | is_none _ = false;
    1.23 +fun is_empty ("", _) = true
    1.24 +  | is_empty _ = false;
    1.25  
    1.26  
    1.27  fun properties more_props ((elem, props): T) =
    1.28 @@ -356,7 +356,7 @@
    1.29      the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
    1.30  end;
    1.31  
    1.32 -fun output m = if is_none m then no_output else #output (get_mode ()) m;
    1.33 +fun output m = if is_empty m then no_output else #output (get_mode ()) m;
    1.34  
    1.35  val enclose = output #-> Library.enclose;
    1.36  
     2.1 --- a/src/Pure/General/markup.scala	Tue Aug 17 23:23:29 2010 +0200
     2.2 +++ b/src/Pure/General/markup.scala	Wed Aug 18 11:02:47 2010 +0200
     2.3 @@ -48,6 +48,11 @@
     2.4    }
     2.5  
     2.6  
     2.7 +  /* empty */
     2.8 +
     2.9 +  val Empty = Markup("", Nil)
    2.10 +
    2.11 +
    2.12    /* name */
    2.13  
    2.14    val NAME = "name"
     3.1 --- a/src/Pure/General/pretty.ML	Tue Aug 17 23:23:29 2010 +0200
     3.2 +++ b/src/Pure/General/pretty.ML	Wed Aug 18 11:02:47 2010 +0200
     3.3 @@ -132,7 +132,7 @@
     3.4  
     3.5  fun markup_block m arg = block_markup (Markup.output m) arg;
     3.6  
     3.7 -val blk = markup_block Markup.none;
     3.8 +val blk = markup_block Markup.empty;
     3.9  fun block prts = blk (2, prts);
    3.10  val strs = block o breaks o map str;
    3.11  
    3.12 @@ -142,7 +142,7 @@
    3.13  fun command name = mark Markup.command (str name);
    3.14  
    3.15  fun markup_chunks m prts = markup m (fbreaks prts);
    3.16 -val chunks = markup_chunks Markup.none;
    3.17 +val chunks = markup_chunks Markup.empty;
    3.18  fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts)));
    3.19  
    3.20  fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];
     4.1 --- a/src/Pure/General/xml.ML	Tue Aug 17 23:23:29 2010 +0200
     4.2 +++ b/src/Pure/General/xml.ML	Wed Aug 18 11:02:47 2010 +0200
     4.3 @@ -79,7 +79,7 @@
     4.4    end;
     4.5  
     4.6  fun output_markup (markup as (name, atts)) =
     4.7 -  if Markup.is_none markup then Markup.no_output
     4.8 +  if Markup.is_empty markup then Markup.no_output
     4.9    else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
    4.10  
    4.11  
     5.1 --- a/src/Pure/General/yxml.ML	Tue Aug 17 23:23:29 2010 +0200
     5.2 +++ b/src/Pure/General/yxml.ML	Wed Aug 18 11:02:47 2010 +0200
     5.3 @@ -52,7 +52,7 @@
     5.4  (* output *)
     5.5  
     5.6  fun output_markup (markup as (name, atts)) =
     5.7 -  if Markup.is_none markup then Markup.no_output
     5.8 +  if Markup.is_empty markup then Markup.no_output
     5.9    else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
    5.10  
    5.11  fun element name atts body =
     6.1 --- a/src/Pure/ML/ml_lex.ML	Tue Aug 17 23:23:29 2010 +0200
     6.2 +++ b/src/Pure/ML/ml_lex.ML	Wed Aug 18 11:02:47 2010 +0200
     6.3 @@ -100,10 +100,10 @@
     6.4    | Real      => Markup.ML_numeral
     6.5    | Char      => Markup.ML_char
     6.6    | String    => Markup.ML_string
     6.7 -  | Space     => Markup.none
     6.8 +  | Space     => Markup.empty
     6.9    | Comment   => Markup.ML_comment
    6.10    | Error _   => Markup.ML_malformed
    6.11 -  | EOF       => Markup.none;
    6.12 +  | EOF       => Markup.empty;
    6.13  
    6.14  fun token_markup kind x =
    6.15    if kind = Keyword andalso exists_string (not o Symbol.is_ascii_letter) x
     7.1 --- a/src/Pure/Syntax/lexicon.ML	Tue Aug 17 23:23:29 2010 +0200
     7.2 +++ b/src/Pure/Syntax/lexicon.ML	Wed Aug 18 11:02:47 2010 +0200
     7.3 @@ -181,9 +181,9 @@
     7.4    | FloatSy     => Markup.numeral
     7.5    | XNumSy      => Markup.numeral
     7.6    | StrSy       => Markup.inner_string
     7.7 -  | Space       => Markup.none
     7.8 +  | Space       => Markup.empty
     7.9    | Comment     => Markup.inner_comment
    7.10 -  | EOF         => Markup.none;
    7.11 +  | EOF         => Markup.empty;
    7.12  
    7.13  fun report_token ctxt (Token (kind, _, (pos, _))) =
    7.14    Context_Position.report ctxt (token_kind_markup kind) pos;
     8.1 --- a/src/Pure/Thy/thy_syntax.ML	Tue Aug 17 23:23:29 2010 +0200
     8.2 +++ b/src/Pure/Thy/thy_syntax.ML	Wed Aug 18 11:02:47 2010 +0200
     8.3 @@ -59,9 +59,9 @@
     8.4    | Token.String        => Markup.string
     8.5    | Token.AltString     => Markup.altstring
     8.6    | Token.Verbatim      => Markup.verbatim
     8.7 -  | Token.Space         => Markup.none
     8.8 +  | Token.Space         => Markup.empty
     8.9    | Token.Comment       => Markup.comment
    8.10 -  | Token.InternalValue => Markup.none
    8.11 +  | Token.InternalValue => Markup.empty
    8.12    | Token.Malformed     => Markup.malformed
    8.13    | Token.Error _       => Markup.malformed
    8.14    | Token.Sync          => Markup.control