src/Pure/General/markup.ML
changeset 38474 e498dc2eb576
parent 38429 9951852fae91
child 38721 ca8b14fa0d0d
--- 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;