discontinued obsolete markup;
authorwenzelm
Wed, 27 Apr 2011 20:28:27 +0200
changeset 42492 83c57d850049
parent 42491 4bb5de0aae66
child 42493 01430341fc79
discontinued obsolete markup;
src/Pure/General/markup.ML
src/Pure/General/markup.scala
src/Tools/jEdit/src/jedit/isabelle_markup.scala
--- a/src/Pure/General/markup.ML	Wed Apr 27 20:19:05 2011 +0200
+++ b/src/Pure/General/markup.ML	Wed Apr 27 20:28:27 2011 +0200
@@ -36,7 +36,6 @@
   val hiddenN: string val hidden: T
   val tclassN: string val tclass: string -> T
   val tyconN: string val tycon: string -> T
-  val fixed_declN: string val fixed_decl: string -> T
   val fixedN: string val fixed: string -> T
   val constN: string val const: string -> T
   val dynamic_factN: string val dynamic_fact: string -> T
@@ -209,7 +208,6 @@
 
 val (tclassN, tclass) = markup_string "tclass" nameN;
 val (tyconN, tycon) = markup_string "tycon" nameN;
-val (fixed_declN, fixed_decl) = markup_string "fixed_decl" nameN;
 val (fixedN, fixed) = markup_string "fixed" nameN;
 val (constN, const) = markup_string "constant" nameN;
 val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
--- a/src/Pure/General/markup.scala	Wed Apr 27 20:19:05 2011 +0200
+++ b/src/Pure/General/markup.scala	Wed Apr 27 20:28:27 2011 +0200
@@ -149,7 +149,6 @@
 
   val TCLASS = "tclass"
   val TYCON = "tycon"
-  val FIXED_DECL = "fixed_decl"
   val FIXED = "fixed"
   val CONST = "constant"
   val DYNAMIC_FACT = "dynamic_fact"
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Wed Apr 27 20:19:05 2011 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Wed Apr 27 20:28:27 2011 +0200
@@ -152,7 +152,6 @@
       // logical entities
       Markup.TCLASS -> NULL,
       Markup.TYCON -> NULL,
-      Markup.FIXED_DECL -> FUNCTION,
       Markup.FIXED -> NULL,
       Markup.CONST -> LITERAL2,
       Markup.DYNAMIC_FACT -> LABEL,