# HG changeset patch
# User wenzelm
# Date 1230933244 -3600
# Node ID a205acc943562aefe2145542aea560608a38d2f5
# Parent  e07fc65e296b70ad4c609bbf06e126094a5c1bf6
Markup.no_output;

diff -r e07fc65e296b -r a205acc94356 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Fri Jan 02 22:52:42 2009 +0100
+++ b/src/Pure/General/markup.ML	Fri Jan 02 22:54:04 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/markup.ML
-    ID:         $Id$
     Author:     Makarius
 
 Common markup elements.
@@ -104,6 +103,7 @@
   val debugN: string
   val initN: string
   val statusN: string
+  val no_output: output * output
   val default_output: T -> output * output
   val add_mode: string -> (T -> output * output) -> unit
   val output: T -> output * output
@@ -288,7 +288,8 @@
 
 (* print mode operations *)
 
-fun default_output (_: T) = ("", "");
+val no_output = ("", "");
+fun default_output (_: T) = no_output;
 
 local
   val default = {output = default_output};
@@ -300,7 +301,7 @@
     the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
 end;
 
-fun output m = if is_none m then ("", "") else #output (get_mode ()) m;
+fun output m = if is_none m then no_output else #output (get_mode ()) m;
 
 val enclose = output #-> Library.enclose;
 
diff -r e07fc65e296b -r a205acc94356 src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Fri Jan 02 22:52:42 2009 +0100
+++ b/src/Pure/General/xml.ML	Fri Jan 02 22:54:04 2009 +0100
@@ -79,7 +79,7 @@
   end;
 
 fun output_markup (markup as (name, atts)) =
-  if Markup.is_none markup then ("", "")
+  if Markup.is_none markup then Markup.no_output
   else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
 
 
diff -r e07fc65e296b -r a205acc94356 src/Pure/General/yxml.ML
--- a/src/Pure/General/yxml.ML	Fri Jan 02 22:52:42 2009 +0100
+++ b/src/Pure/General/yxml.ML	Fri Jan 02 22:54:04 2009 +0100
@@ -42,7 +42,7 @@
 (* output *)
 
 fun output_markup (markup as (name, atts)) =
-  if Markup.is_none markup then ("", "")
+  if Markup.is_none markup then Markup.no_output
   else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
 
 fun element name atts body =
diff -r e07fc65e296b -r a205acc94356 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Fri Jan 02 22:52:42 2009 +0100
+++ b/src/Pure/Thy/latex.ML	Fri Jan 02 22:54:04 2009 +0100
@@ -174,7 +174,7 @@
 fun latex_markup (s, _) =
   if s = Markup.keywordN then ("\\isakeyword{", "}")
   else if s = Markup.commandN then ("\\isacommand{", "}")
-  else ("", "");
+  else Markup.no_output;
 
 fun latex_indent "" _ = ""
   | latex_indent s _ = enclose "\\isaindent{" "}" s;