# HG changeset patch # User wenzelm # Date 1513258107 -3600 # Node ID 4cffa4791ef7a30b43edc3eb0d181b622a541239 # Parent d49727160f0ad0a73fbcf28d4be5636ed35e844f proper \isakeeptag (amending 13b5c3ff1954); diff -r d49727160f0a -r 4cffa4791ef7 src/Pure/Thy/present.scala --- a/src/Pure/Thy/present.scala Thu Dec 14 14:27:37 2017 +0100 +++ b/src/Pure/Thy/present.scala Thu Dec 14 14:28:27 2017 +0100 @@ -149,7 +149,7 @@ case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}" case '-' :: cs => "\\isadroptag{" + cs.mkString + "}" case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}" - case cs => "\\isafoldtag{" + cs.mkString + "}" + case cs => "\\isakeeptag{" + cs.mkString + "}" })) + "\n" }