discontinued mostly unused markup for command spans;
authorwenzelm
Fri Aug 10 10:23:54 2012 +0200 (2012-08-10 ago)
changeset 487528a81ef0bc790
parent 48751 dc3bbdda4bc8
child 48753 5e57a6f24cdb
discontinued mostly unused markup for command spans;
etc/isabelle.css
src/Pure/PIDE/isabelle_markup.ML
src/Pure/PIDE/isabelle_markup.scala
src/Pure/Thy/thy_syntax.ML
     1.1 --- a/etc/isabelle.css	Fri Aug 10 10:18:07 2012 +0200
     1.2 +++ b/etc/isabelle.css	Fri Aug 10 10:23:54 2012 +0200
     1.3 @@ -44,5 +44,3 @@
     1.4  .control        { background-color: #FF6A6A; }
     1.5  .bad            { background-color: #FF6A6A; }
     1.6  
     1.7 -.malformed_span { background-color: #FF6A6A; }
     1.8 -
     2.1 --- a/src/Pure/PIDE/isabelle_markup.ML	Fri Aug 10 10:18:07 2012 +0200
     2.2 +++ b/src/Pure/PIDE/isabelle_markup.ML	Fri Aug 10 10:23:54 2012 +0200
     2.3 @@ -74,9 +74,6 @@
     2.4    val commentN: string val comment: Markup.T
     2.5    val controlN: string val control: Markup.T
     2.6    val tokenN: string val token: Properties.T -> Markup.T
     2.7 -  val command_spanN: string val command_span: string -> Markup.T
     2.8 -  val ignored_spanN: string val ignored_span: Markup.T
     2.9 -  val malformed_spanN: string val malformed_span: Markup.T
    2.10    val elapsedN: string
    2.11    val cpuN: string
    2.12    val gcN: string
    2.13 @@ -241,10 +238,6 @@
    2.14  val tokenN = "token";
    2.15  fun token props = (tokenN, props);
    2.16  
    2.17 -val (command_spanN, command_span) = markup_string "command_span" Markup.nameN;
    2.18 -val (ignored_spanN, ignored_span) = markup_elem "ignored_span";
    2.19 -val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
    2.20 -
    2.21  
    2.22  (* timing *)
    2.23  
     3.1 --- a/src/Pure/PIDE/isabelle_markup.scala	Fri Aug 10 10:18:07 2012 +0200
     3.2 +++ b/src/Pure/PIDE/isabelle_markup.scala	Fri Aug 10 10:23:54 2012 +0200
     3.3 @@ -150,10 +150,6 @@
     3.4    val COMMENT = "comment"
     3.5    val CONTROL = "control"
     3.6  
     3.7 -  val COMMAND_SPAN = "command_span"
     3.8 -  val IGNORED_SPAN = "ignored_span"
     3.9 -  val MALFORMED_SPAN = "malformed_span"
    3.10 -
    3.11  
    3.12    /* timing */
    3.13  
     4.1 --- a/src/Pure/Thy/thy_syntax.ML	Fri Aug 10 10:18:07 2012 +0200
     4.2 +++ b/src/Pure/Thy/thy_syntax.ML	Fri Aug 10 10:23:54 2012 +0200
     4.3 @@ -127,18 +127,7 @@
     4.4  
     4.5  (* present *)
     4.6  
     4.7 -local
     4.8 -
     4.9 -fun kind_markup (Command name) = Isabelle_Markup.command_span name
    4.10 -  | kind_markup Ignored = Isabelle_Markup.ignored_span
    4.11 -  | kind_markup Malformed = Isabelle_Markup.malformed_span;
    4.12 -
    4.13 -in
    4.14 -
    4.15 -fun present_span span =
    4.16 -  Markup.enclose (kind_markup (span_kind span)) (implode (map present_token (span_content span)));
    4.17 -
    4.18 -end;
    4.19 +val present_span = implode o map present_token o span_content;
    4.20  
    4.21  
    4.22