# HG changeset patch
# User wenzelm
# Date 1344587034 -7200
# Node ID 8a81ef0bc79002bf8d077fa6e91f85596f1f5e7f
# Parent  dc3bbdda4bc880b76c1c80edadd8c4e2dd3c51be
discontinued mostly unused markup for command spans;

diff -r dc3bbdda4bc8 -r 8a81ef0bc790 etc/isabelle.css
--- a/etc/isabelle.css	Fri Aug 10 10:18:07 2012 +0200
+++ b/etc/isabelle.css	Fri Aug 10 10:23:54 2012 +0200
@@ -44,5 +44,3 @@
 .control        { background-color: #FF6A6A; }
 .bad            { background-color: #FF6A6A; }
 
-.malformed_span { background-color: #FF6A6A; }
-
diff -r dc3bbdda4bc8 -r 8a81ef0bc790 src/Pure/PIDE/isabelle_markup.ML
--- a/src/Pure/PIDE/isabelle_markup.ML	Fri Aug 10 10:18:07 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML	Fri Aug 10 10:23:54 2012 +0200
@@ -74,9 +74,6 @@
   val commentN: string val comment: Markup.T
   val controlN: string val control: Markup.T
   val tokenN: string val token: Properties.T -> Markup.T
-  val command_spanN: string val command_span: string -> Markup.T
-  val ignored_spanN: string val ignored_span: Markup.T
-  val malformed_spanN: string val malformed_span: Markup.T
   val elapsedN: string
   val cpuN: string
   val gcN: string
@@ -241,10 +238,6 @@
 val tokenN = "token";
 fun token props = (tokenN, props);
 
-val (command_spanN, command_span) = markup_string "command_span" Markup.nameN;
-val (ignored_spanN, ignored_span) = markup_elem "ignored_span";
-val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
-
 
 (* timing *)
 
diff -r dc3bbdda4bc8 -r 8a81ef0bc790 src/Pure/PIDE/isabelle_markup.scala
--- a/src/Pure/PIDE/isabelle_markup.scala	Fri Aug 10 10:18:07 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala	Fri Aug 10 10:23:54 2012 +0200
@@ -150,10 +150,6 @@
   val COMMENT = "comment"
   val CONTROL = "control"
 
-  val COMMAND_SPAN = "command_span"
-  val IGNORED_SPAN = "ignored_span"
-  val MALFORMED_SPAN = "malformed_span"
-
 
   /* timing */
 
diff -r dc3bbdda4bc8 -r 8a81ef0bc790 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Fri Aug 10 10:18:07 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Fri Aug 10 10:23:54 2012 +0200
@@ -127,18 +127,7 @@
 
 (* present *)
 
-local
-
-fun kind_markup (Command name) = Isabelle_Markup.command_span name
-  | kind_markup Ignored = Isabelle_Markup.ignored_span
-  | kind_markup Malformed = Isabelle_Markup.malformed_span;
-
-in
-
-fun present_span span =
-  Markup.enclose (kind_markup (span_kind span)) (implode (map present_token (span_content span)));
-
-end;
+val present_span = implode o map present_token o span_content;