uniform Markup.empty/Markup.Empty in ML and Scala;

--- a/src/Pure/General/markup.ML	Tue Aug 17 23:23:29 2010 +0200
+++ b/src/Pure/General/markup.ML	Wed Aug 18 11:02:47 2010 +0200
@@ -9,8 +9,8 @@
   val parse_int: string -> int
   val print_int: int -> string
   type T = string * Properties.T
-  val none: T
-  val is_none: T -> bool
+  val empty: T
+  val is_empty: T -> bool
   val properties: Properties.T -> T -> T
   val nameN: string
   val name: string -> T -> T
@@ -142,10 +142,10 @@
 
 type T = string * Properties.T;
 
-val none = ("", []);
+val empty = ("", []);
 
-fun is_none ("", _) = true
-  | is_none _ = false;
+fun is_empty ("", _) = true
+  | is_empty _ = false;
 
 
 fun properties more_props ((elem, props): T) =
@@ -356,7 +356,7 @@
     the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
 end;
 
-fun output m = if is_none m then no_output else #output (get_mode ()) m;
+fun output m = if is_empty m then no_output else #output (get_mode ()) m;
 
 val enclose = output #-> Library.enclose;
 

--- a/src/Pure/General/markup.scala	Tue Aug 17 23:23:29 2010 +0200
+++ b/src/Pure/General/markup.scala	Wed Aug 18 11:02:47 2010 +0200
@@ -48,6 +48,11 @@
   }
 
 
+  /* empty */
+
+  val Empty = Markup("", Nil)
+
+
   /* name */
 
   val NAME = "name"

--- a/src/Pure/General/pretty.ML	Tue Aug 17 23:23:29 2010 +0200
+++ b/src/Pure/General/pretty.ML	Wed Aug 18 11:02:47 2010 +0200
@@ -132,7 +132,7 @@
 
 fun markup_block m arg = block_markup (Markup.output m) arg;
 
-val blk = markup_block Markup.none;
+val blk = markup_block Markup.empty;
 fun block prts = blk (2, prts);
 val strs = block o breaks o map str;
 
@@ -142,7 +142,7 @@
 fun command name = mark Markup.command (str name);
 
 fun markup_chunks m prts = markup m (fbreaks prts);
-val chunks = markup_chunks Markup.none;
+val chunks = markup_chunks Markup.empty;
 fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts)));
 
 fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];

--- a/src/Pure/General/xml.ML	Tue Aug 17 23:23:29 2010 +0200
+++ b/src/Pure/General/xml.ML	Wed Aug 18 11:02:47 2010 +0200
@@ -79,7 +79,7 @@
   end;
 
 fun output_markup (markup as (name, atts)) =
-  if Markup.is_none markup then Markup.no_output
+  if Markup.is_empty markup then Markup.no_output
   else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
 
 

--- a/src/Pure/General/yxml.ML	Tue Aug 17 23:23:29 2010 +0200
+++ b/src/Pure/General/yxml.ML	Wed Aug 18 11:02:47 2010 +0200
@@ -52,7 +52,7 @@
 (* output *)
 
 fun output_markup (markup as (name, atts)) =
-  if Markup.is_none markup then Markup.no_output
+  if Markup.is_empty markup then Markup.no_output
   else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
 
 fun element name atts body =

--- a/src/Pure/ML/ml_lex.ML	Tue Aug 17 23:23:29 2010 +0200
+++ b/src/Pure/ML/ml_lex.ML	Wed Aug 18 11:02:47 2010 +0200
@@ -100,10 +100,10 @@
   | Real      => Markup.ML_numeral
   | Char      => Markup.ML_char
   | String    => Markup.ML_string
-  | Space     => Markup.none
+  | Space     => Markup.empty
   | Comment   => Markup.ML_comment
   | Error _   => Markup.ML_malformed
-  | EOF       => Markup.none;
+  | EOF       => Markup.empty;
 
 fun token_markup kind x =
   if kind = Keyword andalso exists_string (not o Symbol.is_ascii_letter) x

--- a/src/Pure/Syntax/lexicon.ML	Tue Aug 17 23:23:29 2010 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Wed Aug 18 11:02:47 2010 +0200
@@ -181,9 +181,9 @@
   | FloatSy     => Markup.numeral
   | XNumSy      => Markup.numeral
   | StrSy       => Markup.inner_string
-  | Space       => Markup.none
+  | Space       => Markup.empty
   | Comment     => Markup.inner_comment
-  | EOF         => Markup.none;
+  | EOF         => Markup.empty;
 
 fun report_token ctxt (Token (kind, _, (pos, _))) =
   Context_Position.report ctxt (token_kind_markup kind) pos;

--- a/src/Pure/Thy/thy_syntax.ML	Tue Aug 17 23:23:29 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Wed Aug 18 11:02:47 2010 +0200
@@ -59,9 +59,9 @@
   | Token.String        => Markup.string
   | Token.AltString     => Markup.altstring
   | Token.Verbatim      => Markup.verbatim
-  | Token.Space         => Markup.none
+  | Token.Space         => Markup.empty
   | Token.Comment       => Markup.comment
-  | Token.InternalValue => Markup.none
+  | Token.InternalValue => Markup.empty
   | Token.Malformed     => Markup.malformed
   | Token.Error _       => Markup.malformed
   | Token.Sync          => Markup.control