author | wenzelm |
Wed, 21 Nov 2012 21:08:20 +0100 | |
changeset 50160 | a29be9d067d2 |
parent 50159 | 1f645910e177 |
child 50161 | 4fc4237488ab |
--- a/src/Tools/jEdit/src/pretty_text_area.scala Wed Nov 21 20:50:34 2012 +0100 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Wed Nov 21 21:08:20 2012 +0100 @@ -1,7 +1,8 @@ /* Title: Tools/jEdit/src/pretty_text_area.scala Author: Makarius -GUI component for pretty-printed with markup, rendered like jEdit text area. +GUI component for pretty-printed text with markup, rendered like jEdit +text area. */ package isabelle.jedit