# HG changeset patch
# User wenzelm
# Date 1218808249 -7200
# Node ID e506f0c6d3f068466225b1a8063e8009adc34895
# Parent  eaa9fef9f4c1e335bf14b8b17db864c6c7ae906e
added is_none;
added inner_comment;

diff -r eaa9fef9f4c1 -r e506f0c6d3f0 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Fri Aug 15 15:50:44 2008 +0200
+++ b/src/Pure/General/markup.ML	Fri Aug 15 15:50:49 2008 +0200
@@ -12,6 +12,7 @@
   val get_string: T -> string -> string option
   val get_int: T -> string -> int option
   val none: T
+  val is_none: T -> bool
   val properties: (string * string) list -> T -> T
   val nameN: string
   val name: string -> T -> T
@@ -54,6 +55,7 @@
   val xnumN: string val xnum: T
   val xstrN: string val xstr: T
   val literalN: string val literal: T
+  val inner_commentN: string val inner_comment: T
   val sortN: string val sort: T
   val typN: string val typ: T
   val termN: string val term: T
@@ -105,6 +107,9 @@
 
 val none = ("", []);
 
+fun is_none ("", _) = true
+  | is_none _ = false;
+
 
 fun properties more_props ((elem, props): T) =
   (elem, fold_rev (AList.update (op =)) more_props props);
@@ -187,6 +192,7 @@
 val (xnumN, xnum) = markup_elem "xnum";
 val (xstrN, xstr) = markup_elem "xstr";
 val (literalN, literal) = markup_elem "literal";
+val (inner_commentN, inner_comment) = markup_elem "inner_comment";
 
 val (sortN, sort) = markup_elem "sort";
 val (typN, typ) = markup_elem "typ";
@@ -261,8 +267,7 @@
     the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
 end;
 
-fun output ("", _) = ("", "")
-  | output m = #output (get_mode ()) m;
+fun output m = if is_none m then ("", "") else #output (get_mode ()) m;
 
 val enclose = output #-> Library.enclose;