diamond
authorLuc Moreau <l.moreau@ecs.soton.ac.uk>
Thu, 14 Jun 2012 07:34:52 +0100
changeset 3331 ac2c3cbdc8a4
parent 3330 bfd8e9ff9b48
child 3332 61767801c2f2
diamond
model/extra-dm.css
model/prov-dm.html
--- a/model/extra-dm.css	Wed Jun 13 23:22:09 2012 +0100
+++ b/model/extra-dm.css	Thu Jun 14 07:34:52 2012 +0100
@@ -326,11 +326,17 @@
     font-weight: bold;
 }
 
+.anexampleTitle {
+    font-family: sans-serif;
+    font-size: 1.6ex;
+    font-weight: bold;
+}
 
-.pnExpression {
+
+.diamond {
     font-weight: normal;
-    font-size:120%;
-    font-family: monospace;
+    font-size:100%;
+    font-family: sans-serif;
 }
 
 
--- a/model/prov-dm.html	Wed Jun 13 23:22:09 2012 +0100
+++ b/model/prov-dm.html	Thu Jun 14 07:34:52 2012 +0100
@@ -14,6 +14,13 @@
     <style type="text/css">
       .note { font-size:small; margin-left:50px }
 
+.diamond {
+    font-weight: normal;
+    font-style: normal;
+    font-size:100%;
+    font-family: sans-serif;
+}
+
 table.thinborder {
 	border-width: 1px;
 	border-spacing: 0px;
@@ -85,8 +92,8 @@
           
           $(this).attr('data-count', mycount).prepend($('<div>').addClass('anexampleTitle')
                                                           //.append($('<a>').addClass('internalDFN').attr('href','#'+myid).append("Example " + mycount))
-              .append("Example " + mycount + " ")
-              .append($('<sup>').append($('<a>').addClass('internalDFN').attr('href','#'+myid).append($('<span>').attr('style','font-size: 100%; font-weight:normal; font-family: sans-serif; ').append("&#9674;"))))
+              .append("Example " + mycount)
+              .append($('<sup>').append($('<a>').addClass('internalDFN').attr('href','#'+myid).append($('<span>').addClass('diamond').append("&#9674;"))))
               );
 
 
@@ -103,7 +110,7 @@
 
           var myid=$(this).addClass('internalDFN').attr('id');
 
-          $(this).after($('<sup>').append($('<a>').attr('href','#'+myid).append("&#9674;")));  //&#9674;//&#9830;
+          $(this).after($('<sup>').append($('<a>').addClass('internalDFN').attr('href','#'+myid).append($('<span>').addClass('diamond').append("&#9674;"))));  //&#9674;//&#9830;
           
               console.log( "dfn for " + myid + " ");