# HG changeset patch
# User wenzelm
# Date 1555155002 -7200
# Node ID 0cc7fe6169245fdc897c2e7c1b44c78882403023
# Parent  7efe226c50e4da6b37d8cc4a659fa7b12a963f3b
more abbrevs;

diff -r 7efe226c50e4 -r 0cc7fe616924 NEWS
--- a/NEWS	Sat Apr 13 12:45:38 2019 +0200
+++ b/NEWS	Sat Apr 13 13:30:02 2019 +0200
@@ -131,6 +131,9 @@
 statement by default (e.g. 'theorem', 'lemma'). This is a subtle change
 of semantics wrt. old-style %name.
 
+* In Isabelle/jEdit, the string "\tag" may be completed to a "\<^marker>\<open>tag \<close>"
+template.
+
 * Document antiquotation option "cartouche" indicates if the output
 should be delimited as cartouche; this takes precedence over the
 analogous option "quotes".
diff -r 7efe226c50e4 -r 0cc7fe616924 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sat Apr 13 12:45:38 2019 +0200
+++ b/src/Pure/Pure.thy	Sat Apr 13 13:30:02 2019 +0200
@@ -95,7 +95,8 @@
   and "extract_type" "extract" :: thy_decl
   and "find_theorems" "find_consts" :: diag
   and "named_theorems" :: thy_decl
-abbrevs "===>" = "===>"  (*prevent replacement of very long arrows*)
+abbrevs "\\tag" = "\<^marker>\<open>tag \<close>"
+  and "===>" = "===>"  (*prevent replacement of very long arrows*)
   and "--->" = "\<midarrow>\<rightarrow>"
   and "hence" "thus" "default_sort" "simproc_setup" "apply_end" "realizers" "realizability" = ""
   and "hence" = "then have"