# HG changeset patch
# User wenzelm
# Date 1243971992 -7200
# Node ID fc5df4a6561b6afbbdbadcd60a913d83dee615a4
# Parent  4c65620f53188344a307d02c4ffced7050d7d42e
type_at: no quotes;

diff -r 4c65620f5318 -r fc5df4a6561b src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Tue Jun 02 21:44:16 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Tue Jun 02 21:46:32 2009 +0200
@@ -104,7 +104,7 @@
     val types = markup_root.filter(_.info match { case TypeInfo(_) => true case _ => false })
     types.flatten(_.flatten).
       find(t => t.start <= pos && t.stop > pos).
-      map(t => "\"" + t.content + "\" : " + (t.info match { case TypeInfo(i) => i case _ => "" })).
+      map(t => t.content + ": " + (t.info match { case TypeInfo(i) => i case _ => "" })).
       getOrElse(null)
   }