# HG changeset patch # User wenzelm # Date 1331419547 -3600 # Node ID b190913c3c4174b795c1d8a302b94b35a84ed29e # Parent 659dcbafe4bf635b831985cf2e78cc3b9653923a simplified span class in conformance to Scala version; diff -r 659dcbafe4bf -r b190913c3c41 src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML Sat Mar 10 23:28:42 2012 +0100 +++ b/src/Pure/Thy/html.ML Sat Mar 10 23:45:47 2012 +0100 @@ -48,12 +48,7 @@ fun span class = ("", ""); -fun span_class (name, props) = - (case Isabelle_Markup.get_entity_kind (name, props) of - SOME kind => Isabelle_Markup.entityN ^ "_" ^ name - | NONE => name); - -val _ = Markup.add_mode htmlN (span o span_class); +val _ = Markup.add_mode htmlN (span o fst); (* symbol output *)