16 months ago wenzelm [Mon, 20 Mar 2017 21:53:37 +0100] rev 65337
merged

16 months ago wenzelm [Mon, 20 Mar 2017 21:44:41 +0100] rev 65336
misc tuning and modernization;
src/HOL/Word/Tools/smt_word.ML src/HOL/Word/Word.thy

16 months ago wenzelm [Mon, 20 Mar 2017 20:43:26 +0100] rev 65335
support to encode/decode command state;
support to merge full contents of command state;
src/Pure/General/symbol.scala src/Pure/Isar/token.scala src/Pure/PIDE/command.scala src/Pure/PIDE/command_span.scala src/Pure/PIDE/markup.scala

16 months ago wenzelm [Mon, 20 Mar 2017 17:24:40 +0100] rev 65334
tuned;
src/Pure/PIDE/xml.scala

16 months ago wenzelm [Mon, 20 Mar 2017 15:37:14 +0100] rev 65333
more operations;
src/Pure/PIDE/xml.ML src/Pure/PIDE/xml.scala

16 months ago wenzelm [Mon, 20 Mar 2017 14:36:15 +0100] rev 65332
tuned signature;
src/Pure/PIDE/document.scala src/Tools/jEdit/src/jedit_rendering.scala src/Tools/jEdit/src/rich_text_area.scala

16 months ago wenzelm [Mon, 20 Mar 2017 14:25:06 +0100] rev 65331
eliminated redundant check (see also 27328dcaf64c vs. 9c53198dbb1c);
src/Tools/jEdit/src/document_view.scala

16 months ago ballarin [Mon, 20 Mar 2017 21:01:47 +0100] rev 65330
Corrected affiliation.
CONTRIBUTORS

16 months ago wenzelm [Sun, 19 Mar 2017 20:28:21 +0100] rev 65329
updated to jedit-5.4.0;
Admin/components/components.sha1 Admin/components/main NEWS src/Tools/jEdit/lib/Tools/jedit src/Tools/jEdit/patches/brackets_extended_styles src/Tools/jEdit/patches/docking src/Tools/jEdit/patches/extended_styles src/Tools/jEdit/patches/file_completion src/Tools/jEdit/patches/folding src/Tools/jEdit/patches/gutter src/Tools/jEdit/patches/props src/Tools/jEdit/src/Isabelle.props src/Tools/jEdit/src/plugin.scala

16 months ago wenzelm [Sun, 19 Mar 2017 18:28:32 +0100] rev 65328
misc tuning and modernization;
src/HOL/Word/Word.thy