clarified nesting of paragraphs: indentation is taken into account more uniformly;
authorwenzelm
Sat Oct 17 19:26:34 2015 +0200 (2015-10-17)
changeset 614595f2ddeb15c06
parent 61458 987533262fc2
child 61460 732028edfbc7
clarified nesting of paragraphs: indentation is taken into account more uniformly;
tuned;
src/Doc/Implementation/ML.thy
src/Doc/Isar_Ref/Generic.thy
src/Doc/Isar_Ref/HOL_Specific.thy
src/Doc/Isar_Ref/Inner_Syntax.thy
src/Doc/Isar_Ref/Spec.thy
src/Pure/Thy/markdown.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Doc/Implementation/ML.thy	Fri Oct 16 14:53:26 2015 +0200
     1.2 +++ b/src/Doc/Implementation/ML.thy	Sat Oct 17 19:26:34 2015 +0200
     1.3 @@ -206,22 +206,18 @@
     1.4    framework (\secref{sec:context} and \chref{ch:local-theory}) have
     1.5    firm naming conventions as follows:
     1.6  
     1.7 -  \begin{itemize}
     1.8 -
     1.9 -    \item theories are called @{ML_text thy}, rarely @{ML_text theory}
    1.10 +    \<^item> theories are called @{ML_text thy}, rarely @{ML_text theory}
    1.11      (never @{ML_text thry})
    1.12  
    1.13 -    \item proof contexts are called @{ML_text ctxt}, rarely @{ML_text
    1.14 +    \<^item> proof contexts are called @{ML_text ctxt}, rarely @{ML_text
    1.15      context} (never @{ML_text ctx})
    1.16  
    1.17 -    \item generic contexts are called @{ML_text context}
    1.18 -
    1.19 -    \item local theories are called @{ML_text lthy}, except for local
    1.20 +    \<^item> generic contexts are called @{ML_text context}
    1.21 +
    1.22 +    \<^item> local theories are called @{ML_text lthy}, except for local
    1.23      theories that are treated as proof context (which is a semantic
    1.24      super-type)
    1.25  
    1.26 -  \end{itemize}
    1.27 -
    1.28    Variations with primed or decimal numbers are always possible, as
    1.29    well as semantic prefixes like @{ML_text foo_thy} or @{ML_text
    1.30    bar_ctxt}, but the base conventions above need to be preserved.
    1.31 @@ -231,25 +227,21 @@
    1.32    \<^item> The main logical entities (\secref{ch:logic}) have established
    1.33    naming convention as follows:
    1.34  
    1.35 -  \begin{itemize}
    1.36 -
    1.37 -    \item sorts are called @{ML_text S}
    1.38 -
    1.39 -    \item types are called @{ML_text T}, @{ML_text U}, or @{ML_text
    1.40 +    \<^item> sorts are called @{ML_text S}
    1.41 +
    1.42 +    \<^item> types are called @{ML_text T}, @{ML_text U}, or @{ML_text
    1.43      ty} (never @{ML_text t})
    1.44  
    1.45 -    \item terms are called @{ML_text t}, @{ML_text u}, or @{ML_text
    1.46 +    \<^item> terms are called @{ML_text t}, @{ML_text u}, or @{ML_text
    1.47      tm} (never @{ML_text trm})
    1.48  
    1.49 -    \item certified types are called @{ML_text cT}, rarely @{ML_text
    1.50 +    \<^item> certified types are called @{ML_text cT}, rarely @{ML_text
    1.51      T}, with variants as for types
    1.52  
    1.53 -    \item certified terms are called @{ML_text ct}, rarely @{ML_text
    1.54 +    \<^item> certified terms are called @{ML_text ct}, rarely @{ML_text
    1.55      t}, with variants as for terms (never @{ML_text ctrm})
    1.56  
    1.57 -    \item theorems are called @{ML_text th}, or @{ML_text thm}
    1.58 -
    1.59 -  \end{itemize}
    1.60 +    \<^item> theorems are called @{ML_text th}, or @{ML_text thm}
    1.61  
    1.62    Proper semantic names override these conventions completely.  For
    1.63    example, the left-hand side of an equation (as a term) can be called
    1.64 @@ -1376,15 +1368,11 @@
    1.65    Isabelle-specific purposes with the following implicit substructures
    1.66    packed into the string content:
    1.67  
    1.68 -  \begin{enumerate}
    1.69 -
    1.70 -    \item sequence of Isabelle symbols (see also \secref{sec:symbols}),
    1.71 +    \<^enum> sequence of Isabelle symbols (see also \secref{sec:symbols}),
    1.72      with @{ML Symbol.explode} as key operation;
    1.73    
    1.74 -    \item XML tree structure via YXML (see also @{cite "isabelle-system"}),
    1.75 +    \<^enum> XML tree structure via YXML (see also @{cite "isabelle-system"}),
    1.76      with @{ML YXML.parse_body} as key operation.
    1.77 -  
    1.78 -  \end{enumerate}
    1.79  
    1.80    Note that Isabelle/ML string literals may refer Isabelle symbols like
    1.81    ``@{verbatim \<alpha>}'' natively, \emph{without} escaping the backslash. This is a
    1.82 @@ -2140,21 +2128,19 @@
    1.83    fork several futures simultaneously. The @{text params} consist of the
    1.84    following fields:
    1.85  
    1.86 -  \begin{itemize}
    1.87 -
    1.88 -    \item @{text "name : string"} (default @{ML "\"\""}) specifies a common name
    1.89 +    \<^item> @{text "name : string"} (default @{ML "\"\""}) specifies a common name
    1.90      for the tasks of the forked futures, which serves diagnostic purposes.
    1.91  
    1.92 -    \item @{text "group : Future.group option"} (default @{ML NONE}) specifies
    1.93 +    \<^item> @{text "group : Future.group option"} (default @{ML NONE}) specifies
    1.94      an optional task group for the forked futures. @{ML NONE} means that a new
    1.95      sub-group of the current worker-thread task context is created. If this is
    1.96      not a worker thread, the group will be a new root in the group hierarchy.
    1.97  
    1.98 -    \item @{text "deps : Future.task list"} (default @{ML "[]"}) specifies
    1.99 +    \<^item> @{text "deps : Future.task list"} (default @{ML "[]"}) specifies
   1.100      dependencies on other future tasks, i.e.\ the adjacency relation in the
   1.101      global task queue. Dependencies on already finished tasks are ignored.
   1.102  
   1.103 -    \item @{text "pri : int"} (default @{ML 0}) specifies a priority within the
   1.104 +    \<^item> @{text "pri : int"} (default @{ML 0}) specifies a priority within the
   1.105      task queue.
   1.106  
   1.107      Typically there is only little deviation from the default priority @{ML 0}.
   1.108 @@ -2167,7 +2153,7 @@
   1.109      priority tasks that are queued later need to wait until this (or another)
   1.110      worker thread becomes free again.
   1.111  
   1.112 -    \item @{text "interrupts : bool"} (default @{ML true}) tells whether the
   1.113 +    \<^item> @{text "interrupts : bool"} (default @{ML true}) tells whether the
   1.114      worker thread that processes the corresponding task is initially put into
   1.115      interruptible state. This state may change again while running, by modifying
   1.116      the thread attributes.
   1.117 @@ -2176,8 +2162,6 @@
   1.118      the responsibility of the programmer that this special state is retained
   1.119      only briefly.
   1.120  
   1.121 -  \end{itemize}
   1.122 -
   1.123    \<^descr> @{ML Future.join}~@{text x} retrieves the value of an already finished
   1.124    future, which may lead to an exception, according to the result of its
   1.125    previous evaluation.
     2.1 --- a/src/Doc/Isar_Ref/Generic.thy	Fri Oct 16 14:53:26 2015 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Generic.thy	Sat Oct 17 19:26:34 2015 +0200
     2.3 @@ -521,9 +521,7 @@
     2.4    The Simplifier accepts the following formats for the @{text "lhs"}
     2.5    term:
     2.6  
     2.7 -  \begin{enumerate}
     2.8 -
     2.9 -    \item First-order patterns, considering the sublanguage of
    2.10 +    \<^enum> First-order patterns, considering the sublanguage of
    2.11      application of constant operators to variable operands, without
    2.12      @{text "\<lambda>"}-abstractions or functional variables.
    2.13      For example:
    2.14 @@ -531,7 +529,7 @@
    2.15      @{text "(?x + ?y) + ?z \<equiv> ?x + (?y + ?z)"} \\
    2.16      @{text "f (f ?x ?y) ?z \<equiv> f ?x (f ?y ?z)"}
    2.17  
    2.18 -    \item Higher-order patterns in the sense of @{cite "nipkow-patterns"}.
    2.19 +    \<^enum> Higher-order patterns in the sense of @{cite "nipkow-patterns"}.
    2.20      These are terms in @{text "\<beta>"}-normal form (this will always be the
    2.21      case unless you have done something strange) where each occurrence
    2.22      of an unknown is of the form @{text "?F x\<^sub>1 \<dots> x\<^sub>n"}, where the
    2.23 @@ -541,7 +539,7 @@
    2.24      or its symmetric form, since the @{text "rhs"} is also a
    2.25      higher-order pattern.
    2.26  
    2.27 -    \item Physical first-order patterns over raw @{text "\<lambda>"}-term
    2.28 +    \<^enum> Physical first-order patterns over raw @{text "\<lambda>"}-term
    2.29      structure without @{text "\<alpha>\<beta>\<eta>"}-equality; abstractions and bound
    2.30      variables are treated like quasi-constant term material.
    2.31  
    2.32 @@ -554,8 +552,6 @@
    2.33      rewrite rule of the second category since conditions can be
    2.34      arbitrary terms.
    2.35  
    2.36 -  \end{enumerate}
    2.37 -
    2.38    \<^descr> @{attribute split} declares case split rules.
    2.39  
    2.40    \<^descr> @{attribute cong} declares congruence rules to the Simplifier
    2.41 @@ -1519,28 +1515,24 @@
    2.42    inferences.  It is faster and more powerful than the other classical
    2.43    reasoning tools, but has major limitations too.
    2.44  
    2.45 -  \begin{itemize}
    2.46 -
    2.47 -    \item It does not use the classical wrapper tacticals, such as the
    2.48 +    \<^item> It does not use the classical wrapper tacticals, such as the
    2.49      integration with the Simplifier of @{method fastforce}.
    2.50  
    2.51 -    \item It does not perform higher-order unification, as needed by the
    2.52 +    \<^item> It does not perform higher-order unification, as needed by the
    2.53      rule @{thm [source=false] rangeI} in HOL.  There are often
    2.54      alternatives to such rules, for example @{thm [source=false]
    2.55      range_eqI}.
    2.56  
    2.57 -    \item Function variables may only be applied to parameters of the
    2.58 +    \<^item> Function variables may only be applied to parameters of the
    2.59      subgoal.  (This restriction arises because the prover does not use
    2.60      higher-order unification.)  If other function variables are present
    2.61      then the prover will fail with the message
    2.62      @{verbatim [display] \<open>Function unknown's argument not a bound variable\<close>}
    2.63  
    2.64 -    \item Its proof strategy is more general than @{method fast} but can
    2.65 +    \<^item> Its proof strategy is more general than @{method fast} but can
    2.66      be slower.  If @{method blast} fails or seems to be running forever,
    2.67      try @{method fast} and the other proof tools described below.
    2.68  
    2.69 -  \end{itemize}
    2.70 -
    2.71    The optional integer argument specifies a bound for the number of
    2.72    unsafe steps used in a proof.  By default, @{method blast} starts
    2.73    with a bound of 0 and increases it successively to 20.  In contrast,
     3.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Oct 16 14:53:26 2015 +0200
     3.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Sat Oct 17 19:26:34 2015 +0200
     3.3 @@ -595,16 +595,14 @@
     3.4    order on the result type. By default, the following modes are
     3.5    defined:
     3.6  
     3.7 -  \begin{description}
     3.8 -
     3.9 -    \item @{text option} defines functions that map into the @{type
    3.10 +    \<^descr> @{text option} defines functions that map into the @{type
    3.11      option} type. Here, the value @{term None} is used to model a
    3.12      non-terminating computation. Monotonicity requires that if @{term
    3.13      None} is returned by a recursive call, then the overall result must
    3.14      also be @{term None}. This is best achieved through the use of the
    3.15      monadic operator @{const "Option.bind"}.
    3.16  
    3.17 -    \item @{text tailrec} defines functions with an arbitrary result
    3.18 +    \<^descr> @{text tailrec} defines functions with an arbitrary result
    3.19      type and uses the slightly degenerated partial order where @{term
    3.20      "undefined"} is the bottom element.  Now, monotonicity requires that
    3.21      if @{term undefined} is returned by a recursive call, then the
    3.22 @@ -613,8 +611,6 @@
    3.23      is directly returned. Thus, this mode of operation allows the
    3.24      definition of arbitrary tail-recursive functions.
    3.25  
    3.26 -  \end{description}
    3.27 -
    3.28    Experienced users may define new modes by instantiating the locale
    3.29    @{const "partial_function_definitions"} appropriately.
    3.30  
    3.31 @@ -1345,9 +1341,7 @@
    3.32    \<^descr> @{command (HOL) "setup_lifting"} Sets up the Lifting package to work
    3.33    with a user-defined type. The command supports two modes.
    3.34  
    3.35 -  \begin{enumerate}
    3.36 -
    3.37 -    \item The first one is a low-level mode when the user must provide as a
    3.38 +    \<^enum> The first one is a low-level mode when the user must provide as a
    3.39      first argument of @{command (HOL) "setup_lifting"} a quotient theorem
    3.40      @{term "Quotient R Abs Rep T"}. The package configures a transfer rule for
    3.41      equality, a domain transfer rules and sets up the @{command_def (HOL)
    3.42 @@ -1361,15 +1355,13 @@
    3.43      Users generally will not prove the @{text Quotient} theorem manually for
    3.44      new types, as special commands exist to automate the process.
    3.45  
    3.46 -    \item When a new subtype is defined by @{command (HOL) typedef}, @{command
    3.47 +    \<^enum> When a new subtype is defined by @{command (HOL) typedef}, @{command
    3.48      (HOL) "lift_definition"} can be used in its second mode, where only the
    3.49      @{term type_definition} theorem @{term "type_definition Rep Abs A"} is
    3.50      used as an argument of the command. The command internally proves the
    3.51      corresponding @{term Quotient} theorem and registers it with @{command
    3.52      (HOL) setup_lifting} using its first mode.
    3.53  
    3.54 -  \end{enumerate}
    3.55 -
    3.56    For quotients, the command @{command (HOL) quotient_type} can be used. The
    3.57    command defines a new quotient type and similarly to the previous case,
    3.58    the corresponding Quotient theorem is proved and registered by @{command
    3.59 @@ -1423,21 +1415,17 @@
    3.60    code execution through series of internal type and lifting definitions if
    3.61    the return type @{text "\<tau>"} meets the following inductive conditions:
    3.62  
    3.63 -  \begin{description}
    3.64 -
    3.65 -    \item @{text "\<tau>"} is a type variable
    3.66 -
    3.67 -    \item @{text "\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>"},
    3.68 +    \<^descr> @{text "\<tau>"} is a type variable
    3.69 +
    3.70 +    \<^descr> @{text "\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>"},
    3.71      where @{text "\<kappa>"} is an abstract type constructor and @{text "\<tau>\<^sub>1 \<dots> \<tau>\<^sub>n"}
    3.72      do not contain abstract types (i.e.\ @{typ "int dlist"} is allowed whereas
    3.73      @{typ "int dlist dlist"} not)
    3.74  
    3.75 -    \item @{text "\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>"}, @{text "\<kappa>"} is a type constructor that
    3.76 +    \<^descr> @{text "\<tau> = \<tau>\<^sub>1 \<dots> \<tau>\<^sub>n \<kappa>"}, @{text "\<kappa>"} is a type constructor that
    3.77      was defined as a (co)datatype whose constructor argument types do not
    3.78      contain either non-free datatypes or the function type.
    3.79  
    3.80 -  \end{description}
    3.81 -
    3.82    Integration with [@{attribute code} equation]: For total quotients,
    3.83    @{command (HOL) "lift_definition"} uses @{text f.abs_eq} as a code
    3.84    equation.
    3.85 @@ -1878,9 +1866,7 @@
    3.86    quickcheck uses exhaustive testing.  A number of configuration
    3.87    options are supported for @{command (HOL) "quickcheck"}, notably:
    3.88  
    3.89 -    \begin{description}
    3.90 -
    3.91 -    \item[@{text tester}] specifies which testing approach to apply.
    3.92 +    \<^descr>[@{text tester}] specifies which testing approach to apply.
    3.93      There are three testers, @{text exhaustive}, @{text random}, and
    3.94      @{text narrowing}.  An unknown configuration option is treated as
    3.95      an argument to tester, making @{text "tester ="} optional.  When
    3.96 @@ -1891,31 +1877,31 @@
    3.97      quickcheck_random_active}, @{attribute
    3.98      quickcheck_narrowing_active} are set to true.
    3.99  
   3.100 -    \item[@{text size}] specifies the maximum size of the search space
   3.101 +    \<^descr>[@{text size}] specifies the maximum size of the search space
   3.102      for assignment values.
   3.103  
   3.104 -    \item[@{text genuine_only}] sets quickcheck only to return genuine
   3.105 +    \<^descr>[@{text genuine_only}] sets quickcheck only to return genuine
   3.106      counterexample, but not potentially spurious counterexamples due
   3.107      to underspecified functions.
   3.108  
   3.109 -    \item[@{text abort_potential}] sets quickcheck to abort once it
   3.110 +    \<^descr>[@{text abort_potential}] sets quickcheck to abort once it
   3.111      found a potentially spurious counterexample and to not continue
   3.112      to search for a further genuine counterexample.
   3.113      For this option to be effective, the @{text genuine_only} option
   3.114      must be set to false.
   3.115  
   3.116 -    \item[@{text eval}] takes a term or a list of terms and evaluates
   3.117 +    \<^descr>[@{text eval}] takes a term or a list of terms and evaluates
   3.118      these terms under the variable assignment found by quickcheck.
   3.119      This option is currently only supported by the default
   3.120      (exhaustive) tester.
   3.121  
   3.122 -    \item[@{text iterations}] sets how many sets of assignments are
   3.123 +    \<^descr>[@{text iterations}] sets how many sets of assignments are
   3.124      generated for each particular size.
   3.125  
   3.126 -    \item[@{text no_assms}] specifies whether assumptions in
   3.127 +    \<^descr>[@{text no_assms}] specifies whether assumptions in
   3.128      structured proofs should be ignored.
   3.129  
   3.130 -    \item[@{text locale}] specifies how to process conjectures in
   3.131 +    \<^descr>[@{text locale}] specifies how to process conjectures in
   3.132      a locale context, i.e.\ they can be interpreted or expanded.
   3.133      The option is a whitespace-separated list of the two words
   3.134      @{text interpret} and @{text expand}. The list determines the
   3.135 @@ -1924,91 +1910,86 @@
   3.136      The option is only provided as attribute declaration, but not
   3.137      as parameter to the command.
   3.138  
   3.139 -    \item[@{text timeout}] sets the time limit in seconds.
   3.140 -
   3.141 -    \item[@{text default_type}] sets the type(s) generally used to
   3.142 +    \<^descr>[@{text timeout}] sets the time limit in seconds.
   3.143 +
   3.144 +    \<^descr>[@{text default_type}] sets the type(s) generally used to
   3.145      instantiate type variables.
   3.146  
   3.147 -    \item[@{text report}] if set quickcheck reports how many tests
   3.148 +    \<^descr>[@{text report}] if set quickcheck reports how many tests
   3.149      fulfilled the preconditions.
   3.150  
   3.151 -    \item[@{text use_subtype}] if set quickcheck automatically lifts
   3.152 +    \<^descr>[@{text use_subtype}] if set quickcheck automatically lifts
   3.153      conjectures to registered subtypes if possible, and tests the
   3.154      lifted conjecture.
   3.155  
   3.156 -    \item[@{text quiet}] if set quickcheck does not output anything
   3.157 +    \<^descr>[@{text quiet}] if set quickcheck does not output anything
   3.158      while testing.
   3.159  
   3.160 -    \item[@{text verbose}] if set quickcheck informs about the current
   3.161 +    \<^descr>[@{text verbose}] if set quickcheck informs about the current
   3.162      size and cardinality while testing.
   3.163  
   3.164 -    \item[@{text expect}] can be used to check if the user's
   3.165 +    \<^descr>[@{text expect}] can be used to check if the user's
   3.166      expectation was met (@{text no_expectation}, @{text
   3.167      no_counterexample}, or @{text counterexample}).
   3.168  
   3.169 -    \end{description}
   3.170 -
   3.171    These option can be given within square brackets.
   3.172  
   3.173    Using the following type classes, the testers generate values and convert
   3.174    them back into Isabelle terms for displaying counterexamples.
   3.175  
   3.176 -    \begin{description}
   3.177 -
   3.178 -    \item[@{text exhaustive}] The parameters of the type classes @{class exhaustive}
   3.179 -      and @{class full_exhaustive} implement the testing. They take a
   3.180 -      testing function as a parameter, which takes a value of type @{typ "'a"}
   3.181 -      and optionally produces a counterexample, and a size parameter for the test values.
   3.182 -      In @{class full_exhaustive}, the testing function parameter additionally
   3.183 -      expects a lazy term reconstruction in the type @{typ Code_Evaluation.term}
   3.184 -      of the tested value.
   3.185 -
   3.186 -      The canonical implementation for @{text exhaustive} testers calls the given
   3.187 -      testing function on all values up to the given size and stops as soon
   3.188 -      as a counterexample is found.
   3.189 -
   3.190 -    \item[@{text random}] The operation @{const Quickcheck_Random.random}
   3.191 -      of the type class @{class random} generates a pseudo-random
   3.192 -      value of the given size and a lazy term reconstruction of the value
   3.193 -      in the type @{typ Code_Evaluation.term}. A pseudo-randomness generator
   3.194 -      is defined in theory @{theory Random}.
   3.195 -
   3.196 -    \item[@{text narrowing}] implements Haskell's Lazy Smallcheck @{cite "runciman-naylor-lindblad"}
   3.197 -      using the type classes @{class narrowing} and @{class partial_term_of}.
   3.198 -      Variables in the current goal are initially represented as symbolic variables.
   3.199 -      If the execution of the goal tries to evaluate one of them, the test engine
   3.200 -      replaces it with refinements provided by @{const narrowing}.
   3.201 -      Narrowing views every value as a sum-of-products which is expressed using the operations
   3.202 -      @{const Quickcheck_Narrowing.cons} (embedding a value),
   3.203 -      @{const Quickcheck_Narrowing.apply} (product) and @{const Quickcheck_Narrowing.sum} (sum).
   3.204 -      The refinement should enable further evaluation of the goal.
   3.205 -
   3.206 -      For example, @{const narrowing} for the list type @{typ "'a :: narrowing list"}
   3.207 -      can be recursively defined as
   3.208 -      @{term "Quickcheck_Narrowing.sum (Quickcheck_Narrowing.cons [])
   3.209 +    \<^descr>[@{text exhaustive}] The parameters of the type classes @{class exhaustive}
   3.210 +    and @{class full_exhaustive} implement the testing. They take a
   3.211 +    testing function as a parameter, which takes a value of type @{typ "'a"}
   3.212 +    and optionally produces a counterexample, and a size parameter for the test values.
   3.213 +    In @{class full_exhaustive}, the testing function parameter additionally
   3.214 +    expects a lazy term reconstruction in the type @{typ Code_Evaluation.term}
   3.215 +    of the tested value.
   3.216 +
   3.217 +    The canonical implementation for @{text exhaustive} testers calls the given
   3.218 +    testing function on all values up to the given size and stops as soon
   3.219 +    as a counterexample is found.
   3.220 +
   3.221 +    \<^descr>[@{text random}] The operation @{const Quickcheck_Random.random}
   3.222 +    of the type class @{class random} generates a pseudo-random
   3.223 +    value of the given size and a lazy term reconstruction of the value
   3.224 +    in the type @{typ Code_Evaluation.term}. A pseudo-randomness generator
   3.225 +    is defined in theory @{theory Random}.
   3.226 +
   3.227 +    \<^descr>[@{text narrowing}] implements Haskell's Lazy Smallcheck @{cite "runciman-naylor-lindblad"}
   3.228 +    using the type classes @{class narrowing} and @{class partial_term_of}.
   3.229 +    Variables in the current goal are initially represented as symbolic variables.
   3.230 +    If the execution of the goal tries to evaluate one of them, the test engine
   3.231 +    replaces it with refinements provided by @{const narrowing}.
   3.232 +    Narrowing views every value as a sum-of-products which is expressed using the operations
   3.233 +    @{const Quickcheck_Narrowing.cons} (embedding a value),
   3.234 +    @{const Quickcheck_Narrowing.apply} (product) and @{const Quickcheck_Narrowing.sum} (sum).
   3.235 +    The refinement should enable further evaluation of the goal.
   3.236 +
   3.237 +    For example, @{const narrowing} for the list type @{typ "'a :: narrowing list"}
   3.238 +    can be recursively defined as
   3.239 +    @{term "Quickcheck_Narrowing.sum (Quickcheck_Narrowing.cons [])
   3.240 +              (Quickcheck_Narrowing.apply
   3.241                  (Quickcheck_Narrowing.apply
   3.242 -                  (Quickcheck_Narrowing.apply
   3.243 -                    (Quickcheck_Narrowing.cons (op #))
   3.244 -                    narrowing)
   3.245 -                  narrowing)"}.
   3.246 -      If a symbolic variable of type @{typ "_ list"} is evaluated, it is replaced by (i)~the empty
   3.247 -      list @{term "[]"} and (ii)~by a non-empty list whose head and tail can then be recursively
   3.248 -      refined if needed.
   3.249 -
   3.250 -      To reconstruct counterexamples, the operation @{const partial_term_of} transforms
   3.251 -      @{text narrowing}'s deep representation of terms to the type @{typ Code_Evaluation.term}.
   3.252 -      The deep representation models symbolic variables as
   3.253 -      @{const Quickcheck_Narrowing.Narrowing_variable}, which are normally converted to
   3.254 -      @{const Code_Evaluation.Free}, and refined values as
   3.255 -      @{term "Quickcheck_Narrowing.Narrowing_constructor i args"}, where @{term "i :: integer"}
   3.256 -      denotes the index in the sum of refinements. In the above example for lists,
   3.257 -      @{term "0"} corresponds to @{term "[]"} and @{term "1"}
   3.258 -      to @{term "op #"}.
   3.259 -
   3.260 -      The command @{command (HOL) "code_datatype"} sets up @{const partial_term_of}
   3.261 -      such that the @{term "i"}-th refinement is interpreted as the @{term "i"}-th constructor,
   3.262 -      but it does not ensures consistency with @{const narrowing}.
   3.263 -    \end{description}
   3.264 +                  (Quickcheck_Narrowing.cons (op #))
   3.265 +                  narrowing)
   3.266 +                narrowing)"}.
   3.267 +    If a symbolic variable of type @{typ "_ list"} is evaluated, it is replaced by (i)~the empty
   3.268 +    list @{term "[]"} and (ii)~by a non-empty list whose head and tail can then be recursively
   3.269 +    refined if needed.
   3.270 +
   3.271 +    To reconstruct counterexamples, the operation @{const partial_term_of} transforms
   3.272 +    @{text narrowing}'s deep representation of terms to the type @{typ Code_Evaluation.term}.
   3.273 +    The deep representation models symbolic variables as
   3.274 +    @{const Quickcheck_Narrowing.Narrowing_variable}, which are normally converted to
   3.275 +    @{const Code_Evaluation.Free}, and refined values as
   3.276 +    @{term "Quickcheck_Narrowing.Narrowing_constructor i args"}, where @{term "i :: integer"}
   3.277 +    denotes the index in the sum of refinements. In the above example for lists,
   3.278 +    @{term "0"} corresponds to @{term "[]"} and @{term "1"}
   3.279 +    to @{term "op #"}.
   3.280 +
   3.281 +    The command @{command (HOL) "code_datatype"} sets up @{const partial_term_of}
   3.282 +    such that the @{term "i"}-th refinement is interpreted as the @{term "i"}-th constructor,
   3.283 +    but it does not ensures consistency with @{const narrowing}.
   3.284  
   3.285    \<^descr> @{command (HOL) "quickcheck_params"} changes @{command (HOL)
   3.286    "quickcheck"} configuration options persistently.
   3.287 @@ -2207,9 +2188,7 @@
   3.288    @{cite \<open>\S3.2\<close> "Chaieb-thesis"}. The method handles deals with two main
   3.289    classes of problems:
   3.290  
   3.291 -  \begin{enumerate}
   3.292 -
   3.293 -    \item Universal problems over multivariate polynomials in a
   3.294 +    \<^enum> Universal problems over multivariate polynomials in a
   3.295      (semi)-ring/field/idom; the capabilities of the method are augmented
   3.296      according to properties of these structures. For this problem class
   3.297      the method is only complete for algebraically closed fields, since
   3.298 @@ -2219,7 +2198,7 @@
   3.299      The problems can contain equations @{text "p = 0"} or inequations
   3.300      @{text "q \<noteq> 0"} anywhere within a universal problem statement.
   3.301  
   3.302 -    \item All-exists problems of the following restricted (but useful)
   3.303 +    \<^enum> All-exists problems of the following restricted (but useful)
   3.304      form:
   3.305  
   3.306      @{text [display] "\<forall>x\<^sub>1 \<dots> x\<^sub>n.
   3.307 @@ -2232,8 +2211,6 @@
   3.308      Here @{text "e\<^sub>1, \<dots>, e\<^sub>n"} and the @{text "p\<^sub>i\<^sub>j"} are multivariate
   3.309      polynomials only in the variables mentioned as arguments.
   3.310  
   3.311 -  \end{enumerate}
   3.312 -
   3.313    The proof method is preceded by a simplification step, which may be
   3.314    modified by using the form @{text "(algebra add: ths\<^sub>1 del: ths\<^sub>2)"}.
   3.315    This acts like declarations for the Simplifier
     4.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Fri Oct 16 14:53:26 2015 +0200
     4.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Oct 17 19:26:34 2015 +0200
     4.3 @@ -818,30 +818,26 @@
     4.4    \<^item> Dummy variables (written as underscore) may occur in different
     4.5    roles.
     4.6  
     4.7 -  \begin{description}
     4.8 -
     4.9 -    \item A type ``@{text "_"}'' or ``@{text "_ :: sort"}'' acts like an
    4.10 +    \<^descr> A type ``@{text "_"}'' or ``@{text "_ :: sort"}'' acts like an
    4.11      anonymous inference parameter, which is filled-in according to the
    4.12      most general type produced by the type-checking phase.
    4.13  
    4.14 -    \item A bound ``@{text "_"}'' refers to a vacuous abstraction, where
    4.15 +    \<^descr> A bound ``@{text "_"}'' refers to a vacuous abstraction, where
    4.16      the body does not refer to the binding introduced here.  As in the
    4.17      term @{term "\<lambda>x _. x"}, which is @{text "\<alpha>"}-equivalent to @{text
    4.18      "\<lambda>x y. x"}.
    4.19  
    4.20 -    \item A free ``@{text "_"}'' refers to an implicit outer binding.
    4.21 +    \<^descr> A free ``@{text "_"}'' refers to an implicit outer binding.
    4.22      Higher definitional packages usually allow forms like @{text "f x _
    4.23      = x"}.
    4.24  
    4.25 -    \item A schematic ``@{text "_"}'' (within a term pattern, see
    4.26 +    \<^descr> A schematic ``@{text "_"}'' (within a term pattern, see
    4.27      \secref{sec:term-decls}) refers to an anonymous variable that is
    4.28      implicitly abstracted over its context of locally bound variables.
    4.29      For example, this allows pattern matching of @{text "{x. f x = g
    4.30      x}"} against @{text "{x. _ = _}"}, or even @{text "{_. _ = _}"} by
    4.31      using both bound and schematic dummies.
    4.32  
    4.33 -  \end{description}
    4.34 -
    4.35    \<^descr> The three literal dots ``@{verbatim "..."}'' may be also
    4.36    written as ellipsis symbol @{verbatim "\<dots>"}.  In both cases this
    4.37    refers to a special schematic variable, which is bound in the
    4.38 @@ -870,12 +866,10 @@
    4.39    current context.  The output can be quite large; the most important
    4.40    sections are explained below.
    4.41  
    4.42 -  \begin{description}
    4.43 -
    4.44 -    \item @{text "lexicon"} lists the delimiters of the inner token
    4.45 +    \<^descr> @{text "lexicon"} lists the delimiters of the inner token
    4.46      language; see \secref{sec:inner-lex}.
    4.47  
    4.48 -    \item @{text "prods"} lists the productions of the underlying
    4.49 +    \<^descr> @{text "prods"} lists the productions of the underlying
    4.50      priority grammar; see \secref{sec:priority-grammar}.
    4.51  
    4.52      The nonterminal @{text "A\<^sup>(\<^sup>p\<^sup>)"} is rendered in plain text as @{text
    4.53 @@ -896,22 +890,20 @@
    4.54      Priority information attached to chain productions is ignored; only
    4.55      the dummy value @{text "-1"} is displayed.
    4.56  
    4.57 -    \item @{text "print modes"} lists the alternative print modes
    4.58 +    \<^descr> @{text "print modes"} lists the alternative print modes
    4.59      provided by this grammar; see \secref{sec:print-modes}.
    4.60  
    4.61 -    \item @{text "parse_rules"} and @{text "print_rules"} relate to
    4.62 +    \<^descr> @{text "parse_rules"} and @{text "print_rules"} relate to
    4.63      syntax translations (macros); see \secref{sec:syn-trans}.
    4.64  
    4.65 -    \item @{text "parse_ast_translation"} and @{text
    4.66 +    \<^descr> @{text "parse_ast_translation"} and @{text
    4.67      "print_ast_translation"} list sets of constants that invoke
    4.68      translation functions for abstract syntax trees, which are only
    4.69      required in very special situations; see \secref{sec:tr-funs}.
    4.70  
    4.71 -    \item @{text "parse_translation"} and @{text "print_translation"}
    4.72 +    \<^descr> @{text "parse_translation"} and @{text "print_translation"}
    4.73      list the sets of constants that invoke regular translation
    4.74      functions; see \secref{sec:tr-funs}.
    4.75 -
    4.76 -  \end{description}
    4.77  \<close>
    4.78  
    4.79  
    4.80 @@ -1167,20 +1159,17 @@
    4.81    (@{verbatim "_"}).  The latter correspond to nonterminal symbols
    4.82    @{text "A\<^sub>i"} derived from the argument types @{text "\<tau>\<^sub>i"} as
    4.83    follows:
    4.84 -  \begin{itemize}
    4.85  
    4.86 -    \item @{text "prop"} if @{text "\<tau>\<^sub>i = prop"}
    4.87 +    \<^item> @{text "prop"} if @{text "\<tau>\<^sub>i = prop"}
    4.88  
    4.89 -    \item @{text "logic"} if @{text "\<tau>\<^sub>i = (\<dots>)\<kappa>"} for logical type
    4.90 +    \<^item> @{text "logic"} if @{text "\<tau>\<^sub>i = (\<dots>)\<kappa>"} for logical type
    4.91      constructor @{text "\<kappa> \<noteq> prop"}
    4.92  
    4.93 -    \item @{text any} if @{text "\<tau>\<^sub>i = \<alpha>"} for type variables
    4.94 +    \<^item> @{text any} if @{text "\<tau>\<^sub>i = \<alpha>"} for type variables
    4.95  
    4.96 -    \item @{text "\<kappa>"} if @{text "\<tau>\<^sub>i = \<kappa>"} for nonterminal @{text "\<kappa>"}
    4.97 +    \<^item> @{text "\<kappa>"} if @{text "\<tau>\<^sub>i = \<kappa>"} for nonterminal @{text "\<kappa>"}
    4.98      (syntactic type constructor)
    4.99  
   4.100 -  \end{itemize}
   4.101 -
   4.102    Each @{text "A\<^sub>i"} is decorated by priority @{text "p\<^sub>i"} from the
   4.103    given list @{text "ps"}; missing priorities default to 0.
   4.104  
   4.105 @@ -1243,19 +1232,15 @@
   4.106    AST rewrite rules @{text "(lhs, rhs)"} need to obey the following
   4.107    side-conditions:
   4.108  
   4.109 -  \begin{itemize}
   4.110 -
   4.111 -    \item Rules must be left linear: @{text "lhs"} must not contain
   4.112 +    \<^item> Rules must be left linear: @{text "lhs"} must not contain
   4.113      repeated variables.\footnote{The deeper reason for this is that AST
   4.114      equality is not well-defined: different occurrences of the ``same''
   4.115      AST could be decorated differently by accidental type-constraints or
   4.116      source position information, for example.}
   4.117  
   4.118 -    \item Every variable in @{text "rhs"} must also occur in @{text
   4.119 +    \<^item> Every variable in @{text "rhs"} must also occur in @{text
   4.120      "lhs"}.
   4.121  
   4.122 -  \end{itemize}
   4.123 -
   4.124    \<^descr> @{command "no_translations"}~@{text rules} removes syntactic
   4.125    translation rules, which are interpreted in the same manner as for
   4.126    @{command "translations"} above.
     5.1 --- a/src/Doc/Isar_Ref/Spec.thy	Fri Oct 16 14:53:26 2015 +0200
     5.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Sat Oct 17 19:26:34 2015 +0200
     5.3 @@ -565,37 +565,33 @@
     5.4  
     5.5    The @{text body} consists of context elements.
     5.6  
     5.7 -  \begin{description}
     5.8 -
     5.9 -    \item @{element "fixes"}~@{text "x :: \<tau> (mx)"} declares a local
    5.10 +    \<^descr> @{element "fixes"}~@{text "x :: \<tau> (mx)"} declares a local
    5.11      parameter of type @{text \<tau>} and mixfix annotation @{text mx} (both
    5.12      are optional).  The special syntax declaration ``@{text
    5.13      "("}@{keyword_ref "structure"}@{text ")"}'' means that @{text x} may
    5.14      be referenced implicitly in this context.
    5.15  
    5.16 -    \item @{element "constrains"}~@{text "x :: \<tau>"} introduces a type
    5.17 +    \<^descr> @{element "constrains"}~@{text "x :: \<tau>"} introduces a type
    5.18      constraint @{text \<tau>} on the local parameter @{text x}.  This
    5.19      element is deprecated.  The type constraint should be introduced in
    5.20      the @{keyword "for"} clause or the relevant @{element "fixes"} element.
    5.21  
    5.22 -    \item @{element "assumes"}~@{text "a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
    5.23 +    \<^descr> @{element "assumes"}~@{text "a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
    5.24      introduces local premises, similar to @{command "assume"} within a
    5.25      proof (cf.\ \secref{sec:proof-context}).
    5.26  
    5.27 -    \item @{element "defines"}~@{text "a: x \<equiv> t"} defines a previously
    5.28 +    \<^descr> @{element "defines"}~@{text "a: x \<equiv> t"} defines a previously
    5.29      declared parameter.  This is similar to @{command "def"} within a
    5.30      proof (cf.\ \secref{sec:proof-context}), but @{element "defines"}
    5.31      takes an equational proposition instead of variable-term pair.  The
    5.32      left-hand side of the equation may have additional arguments, e.g.\
    5.33      ``@{element "defines"}~@{text "f x\<^sub>1 \<dots> x\<^sub>n \<equiv> t"}''.
    5.34  
    5.35 -    \item @{element "notes"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}
    5.36 +    \<^descr> @{element "notes"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}
    5.37      reconsiders facts within a local context.  Most notably, this may
    5.38      include arbitrary declarations in any attribute specifications
    5.39      included here, e.g.\ a local @{attribute simp} rule.
    5.40  
    5.41 -  \end{description}
    5.42 -
    5.43    Both @{element "assumes"} and @{element "defines"} elements
    5.44    contribute to the locale specification.  When defining an operation
    5.45    derived from the parameters, @{command "definition"}
    5.46 @@ -865,28 +861,20 @@
    5.47    also \emph{rewrite definitions} may be specified.  Semantically, a
    5.48    rewrite definition
    5.49    
    5.50 -  \begin{itemize}
    5.51 -  
    5.52 -    \item produces a corresponding definition in
    5.53 +    \<^item> produces a corresponding definition in
    5.54      the local theory's underlying target \emph{and}
    5.55  
    5.56 -    \item augments the rewrite morphism with the equation
    5.57 +    \<^item> augments the rewrite morphism with the equation
    5.58      stemming from the symmetric of the corresponding definition.
    5.59 -
    5.60 -  \end{itemize}
    5.61    
    5.62    This is technically different to to a naive combination
    5.63    of a conventional definition and an explicit rewrite equation:
    5.64    
    5.65 -  \begin{itemize}
    5.66 -  
    5.67 -    \item Definitions are parsed in the syntactic interpretation
    5.68 +    \<^item> Definitions are parsed in the syntactic interpretation
    5.69      context, just like equations.
    5.70  
    5.71 -    \item The proof needs not consider the equations stemming from
    5.72 +    \<^item> The proof needs not consider the equations stemming from
    5.73      definitions -- they are proved implicitly by construction.
    5.74 -      
    5.75 -  \end{itemize}
    5.76    
    5.77    Rewrite definitions yield a pattern for introducing new explicit
    5.78    operations for existing terms after interpretation.
     6.1 --- a/src/Pure/Thy/markdown.ML	Fri Oct 16 14:53:26 2015 +0200
     6.2 +++ b/src/Pure/Thy/markdown.ML	Sat Oct 17 19:26:34 2015 +0200
     6.3 @@ -22,13 +22,12 @@
     6.4    val is_control: Symbol.symbol -> bool
     6.5    datatype kind = Itemize | Enumerate | Description
     6.6    val print_kind: kind -> string
     6.7 -  type marker = {indent: int, kind: kind}
     6.8    type line
     6.9    val line_source: line -> Antiquote.text_antiquote list
    6.10    val line_content: line -> Antiquote.text_antiquote list
    6.11    val make_line: Antiquote.text_antiquote list -> line
    6.12    val empty_line: line
    6.13 -  datatype block = Paragraph of line list | List of marker * block list
    6.14 +  datatype block = Paragraph of line list | List of {indent: int, kind: kind, body: block list}
    6.15    val read_lines: line list -> block list
    6.16    val read_antiquotes: Antiquote.text_antiquote list -> block list
    6.17    val read_source: Input.source -> block list
    6.18 @@ -49,23 +48,25 @@
    6.19    | print_kind Enumerate = "enumerate"
    6.20    | print_kind Description = "description";
    6.21  
    6.22 -type marker = {indent: int, kind: kind};
    6.23 -
    6.24  datatype line =
    6.25    Line of
    6.26     {source: Antiquote.text_antiquote list,
    6.27 -    content: Antiquote.text_antiquote list,
    6.28      is_empty: bool,
    6.29 -    marker: (marker * Position.T) option};
    6.30 +    indent: int,
    6.31 +    item: kind option,
    6.32 +    item_pos: Position.T,
    6.33 +    content: Antiquote.text_antiquote list};
    6.34  
    6.35  val eof_line =
    6.36    Line {source = [Antiquote.Text [(Symbol.eof, Position.none)]],
    6.37 -    content = [], is_empty = false, marker = NONE};
    6.38 +    is_empty = false, indent = 0, item = NONE, item_pos = Position.none, content = []};
    6.39  
    6.40  fun line_source (Line {source, ...}) = source;
    6.41 +fun line_is_empty (Line {is_empty, ...}) = is_empty;
    6.42 +fun line_indent (Line {indent, ...}) = indent;
    6.43 +fun line_item (Line {item, ...}) = item;
    6.44 +fun line_item_pos (Line {item_pos, ...}) = item_pos;
    6.45  fun line_content (Line {content, ...}) = content;
    6.46 -fun line_is_empty (Line {is_empty, ...}) = is_empty;
    6.47 -fun line_marker (Line {marker, ...}) = marker;
    6.48  
    6.49  
    6.50  (* make line *)
    6.51 @@ -86,24 +87,28 @@
    6.52  
    6.53  val scan_marker =
    6.54    Scan.many is_space -- Symbol_Pos.scan_pos --
    6.55 -  (Symbol_Pos.$$ "\\<^item>" >> K Itemize ||
    6.56 -   Symbol_Pos.$$ "\\<^enum>" >> K Enumerate ||
    6.57 -   Symbol_Pos.$$ "\\<^descr>" >> K Description)
    6.58 -  >> (fn ((spaces, pos), kind) => ({indent = length spaces, kind = kind}, pos));
    6.59 +  Scan.option
    6.60 +   (Symbol_Pos.$$ "\\<^item>" >> K Itemize ||
    6.61 +    Symbol_Pos.$$ "\\<^enum>" >> K Enumerate ||
    6.62 +    Symbol_Pos.$$ "\\<^descr>" >> K Description) --| Scan.many is_space
    6.63 +  >> (fn ((sp, pos), item) => (length sp, item, if is_some item then pos else Position.none));
    6.64  
    6.65  fun read_marker (Antiquote.Text ss :: rest) =
    6.66 -      (case Scan.finite Symbol_Pos.stopper (Scan.option scan_marker --| Scan.many is_space) ss of
    6.67 +      (case Scan.finite Symbol_Pos.stopper scan_marker ss of
    6.68          (marker, []) => (marker, rest)
    6.69        | (marker, ss') => (marker, Antiquote.Text ss' :: rest))
    6.70 -  | read_marker source = (NONE, source);
    6.71 +  | read_marker source = ((0, NONE, Position.none), source);
    6.72  
    6.73  in
    6.74  
    6.75  fun make_line source =
    6.76    let
    6.77      val _ = check_blanks source;
    6.78 -    val (marker, content) = read_marker source;
    6.79 -  in Line {source = source, content = content, is_empty = is_empty source, marker = marker} end;
    6.80 +    val ((indent, item, item_pos), content) = read_marker source;
    6.81 +  in
    6.82 +    Line {source = source, is_empty = is_empty source, indent = indent,
    6.83 +      item = item, item_pos = item_pos, content = content}
    6.84 +  end;
    6.85  
    6.86  val empty_line = make_line [];
    6.87  
    6.88 @@ -112,46 +117,53 @@
    6.89  
    6.90  (* document blocks *)
    6.91  
    6.92 -datatype block = Paragraph of line list | List of marker * block list;
    6.93 +datatype block =
    6.94 +  Paragraph of line list | List of {indent: int, kind: kind, body: block list};
    6.95  
    6.96  fun block_lines (Paragraph lines) = lines
    6.97 -  | block_lines (List (_, blocks)) = maps block_lines blocks;
    6.98 +  | block_lines (List {body, ...}) = maps block_lines body;
    6.99  
   6.100  fun block_range (Paragraph lines) = Antiquote.range (maps line_content lines)
   6.101 -  | block_range (List (_, blocks)) = Antiquote.range (maps line_source (maps block_lines blocks));
   6.102 +  | block_range (List {body, ...}) = Antiquote.range (maps line_source (maps block_lines body));
   6.103 +
   6.104 +fun block_indent (List {indent, ...}) = indent
   6.105 +  | block_indent (Paragraph (line :: _)) = line_indent line
   6.106 +  | block_indent _ = 0;
   6.107 +
   6.108 +fun block_list indent0 kind0 (List {indent, kind, body}) =
   6.109 +      if indent0 = indent andalso kind0 = kind then SOME body else NONE
   6.110 +  | block_list _ _ _ = NONE;
   6.111 +
   6.112 +val is_list = fn List _ => true | _ => false;
   6.113  
   6.114  
   6.115  (* read document *)
   6.116  
   6.117  local
   6.118  
   6.119 -fun add_span (opt_marker, body) document =
   6.120 -  (case (opt_marker, document) of
   6.121 -    (SOME marker, (list as List (list_marker, list_body)) :: rest) =>
   6.122 -      if marker = list_marker then
   6.123 -        List (list_marker, body @ list_body) :: rest
   6.124 -      else if #indent marker < #indent list_marker then
   6.125 -        add_span (opt_marker, body @ [list]) rest
   6.126 -      else
   6.127 -        List (marker, body) :: document
   6.128 -  | (SOME marker, _) => List (marker, body) :: document
   6.129 -  | (NONE, _) => body @ document);
   6.130 +fun build (indent, item, rev_body) document =
   6.131 +  (case (item, document) of
   6.132 +    (SOME kind, block :: blocks) =>
   6.133 +      (case block_list indent kind block of
   6.134 +        SOME list => List {indent = indent, kind = kind, body = fold cons rev_body list} :: blocks
   6.135 +      | NONE =>
   6.136 +          if (if is_list block then indent < block_indent block else indent <= block_indent block)
   6.137 +          then build (indent, item, block :: rev_body) blocks
   6.138 +          else List {indent = indent, kind = kind, body = rev rev_body} :: document)
   6.139 +  | (SOME kind, []) => [List {indent = indent, kind = kind, body = rev rev_body}]
   6.140 +  | (NONE, _) => fold cons rev_body document);
   6.141  
   6.142  fun plain_line line =
   6.143 -  not (line_is_empty line) andalso is_none (line_marker line) andalso line <> eof_line;
   6.144 -
   6.145 -val parse_paragraph = Scan.many1 plain_line >> Paragraph;
   6.146 +  not (line_is_empty line) andalso is_none (line_item line) andalso line <> eof_line;
   6.147  
   6.148 -val parse_span =
   6.149 -  parse_paragraph >> (fn par => (NONE, [par])) ||
   6.150 -  Scan.one (is_some o line_marker) -- Scan.many plain_line --
   6.151 -    Scan.repeat (Scan.one line_is_empty |-- parse_paragraph) >>
   6.152 -      (fn ((line, lines), pars) =>
   6.153 -        (Option.map #1 (line_marker line), Paragraph (line :: lines) :: pars));
   6.154 +val parse_paragraph =
   6.155 +  Scan.one (fn line => line <> eof_line) -- Scan.many plain_line >> (fn (line, lines) =>
   6.156 +    let val block = Paragraph (line :: lines)
   6.157 +    in (line_indent line, line_item line, [block]) end);
   6.158  
   6.159  val parse_document =
   6.160 -  parse_span ::: Scan.repeat (Scan.option (Scan.one line_is_empty) |-- parse_span)
   6.161 -    >> (fn spans => fold_rev add_span spans []);
   6.162 +  parse_paragraph ::: Scan.repeat (Scan.option (Scan.one line_is_empty) |-- parse_paragraph)
   6.163 +    >> (fn pars => fold_rev build pars []);
   6.164  
   6.165  in
   6.166  
   6.167 @@ -173,17 +185,16 @@
   6.168  
   6.169  local
   6.170  
   6.171 -fun line_reports depth (Line {marker = SOME (_, pos), content, ...}) =
   6.172 -      cons (pos, Markup.markdown_item depth) #>
   6.173 -      append (text_reports content)
   6.174 -  | line_reports _ _ = I;
   6.175 +fun line_reports depth line =
   6.176 +  cons (line_item_pos line, Markup.markdown_item depth) #>
   6.177 +  append (text_reports (line_content line));
   6.178  
   6.179  fun block_reports depth block =
   6.180    (case block of
   6.181      Paragraph lines =>
   6.182        cons (#1 (block_range block), Markup.markdown_paragraph) #>
   6.183        fold (line_reports depth) lines
   6.184 -  | List ({kind, ...}, body) =>
   6.185 +  | List {kind, body, ...} =>
   6.186        cons (#1 (block_range block), Markup.markdown_list (print_kind kind)) #>
   6.187        fold (block_reports (depth + 1)) body);
   6.188  
     7.1 --- a/src/Pure/Thy/thy_output.ML	Fri Oct 16 14:53:26 2015 +0200
     7.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Oct 17 19:26:34 2015 +0200
     7.3 @@ -195,8 +195,8 @@
     7.4      fun output_blocks blocks = space_implode "\n\n" (map output_block blocks)
     7.5      and output_block (Markdown.Paragraph lines) =
     7.6            cat_lines (map (output_antiquotes o Markdown.line_source) lines)
     7.7 -      | output_block (Markdown.List (marker, body)) =
     7.8 -          let val env = Markdown.print_kind (#kind marker) in
     7.9 +      | output_block (Markdown.List {kind, body, ...}) =
    7.10 +          let val env = Markdown.print_kind kind in
    7.11              "%\n\\begin{" ^ env ^ "}%\n" ^
    7.12              output_blocks body ^
    7.13              "%\n\\end{" ^ env ^ "}%\n"