# HG changeset patch
# User wenzelm
# Date 1444825260 -7200
# Node ID 8bb17fd2fa81d8b4d0bc79821645e326d014f841
# Parent  b8708432ce03ca478dab800a2f90de78a1710e95
clarified control symbols;

diff -r b8708432ce03 -r 8bb17fd2fa81 NEWS
--- a/NEWS	Wed Oct 14 14:15:13 2015 +0200
+++ b/NEWS	Wed Oct 14 14:21:00 2015 +0200
@@ -59,12 +59,14 @@
 
 * Isabelle control symbols for markup and formatting:
 
+  \<^noindent>   \noindent
   \<^smallskip>   \smallskip
   \<^medskip>   \medskip
   \<^bigskip>   \bigskip
 
   \<^item>  \item  (itemize)
-  \<^enum>  \item  (enumeration)
+  \<^enum>  \item  (enumerate)
+  \<^descr>  \item  (description)
 
 
 *** Isar ***
diff -r b8708432ce03 -r 8bb17fd2fa81 etc/symbols
--- a/etc/symbols	Wed Oct 14 14:15:13 2015 +0200
+++ b/etc/symbols	Wed Oct 14 14:21:00 2015 +0200
@@ -352,15 +352,18 @@
 \<open>                 code: 0x002039  group: punctuation  font: IsabelleText  abbrev: <<
 \<close>                code: 0x00203a  group: punctuation  font: IsabelleText  abbrev: >>
 \<here>                 code: 0x002302  font: IsabelleText
+\<^noindent>            code: 0x0021e4  group: control  font: IsabelleText
+\<^smallskip>           code: 0x002508  group: control  font: IsabelleText
+\<^medskip>             code: 0x002509  group: control  font: IsabelleText
+\<^bigskip>             code: 0x002501  group: control  font: IsabelleText
+\<^item>                code: 0x0025aa  group: control  font: IsabelleText
+\<^enum>                code: 0x0025b8  group: control  font: IsabelleText
+\<^descr>               code: 0x0027a7  group: control  font: IsabelleText
+\<^emph>                code: 0x002217  group: control  font: IsabelleText
+\<^bold>                code: 0x002759  group: control  font: IsabelleText
 \<^sub>                 code: 0x0021e9  group: control  font: IsabelleText
 \<^sup>                 code: 0x0021e7  group: control  font: IsabelleText
-\<^bold>                code: 0x002759  group: control  font: IsabelleText
 \<^bsub>                code: 0x0021d8  group: control_block  font: IsabelleText  abbrev: =_(
 \<^esub>                code: 0x0021d9  group: control_block  font: IsabelleText  abbrev: =_)
 \<^bsup>                code: 0x0021d7  group: control_block  font: IsabelleText  abbrev: =^(
 \<^esup>                code: 0x0021d6  group: control_block  font: IsabelleText  abbrev: =^)
-\<^smallskip>           code: 0x002508  group: control
-\<^medskip>             code: 0x002509  group: control
-\<^bigskip>             code: 0x002501  group: control
-\<^item>                code: 0x0025aa  group: control
-\<^enum>                code: 0x0025b8  group: control
diff -r b8708432ce03 -r 8bb17fd2fa81 lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Wed Oct 14 14:15:13 2015 +0200
+++ b/lib/texinputs/isabelle.sty	Wed Oct 14 14:21:00 2015 +0200
@@ -39,11 +39,13 @@
 \DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 
+\def\isactrlnoindent{\noindent}
 \def\isactrlsmallskip{\smallskip}
 \def\isactrlmedskip{\medskip}
 \def\isactrlbigskip{\bigskip}
 \def\isactrlitem{\item}
 \def\isactrlenum{\item}
+\def\isactrldescr{\item}
 
 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}