more explicit output of list items;
authorwenzelm
Sat Oct 17 19:47:34 2015 +0200 (2015-10-17)
changeset 6146177c9643a6353
parent 61460 732028edfbc7
child 61462 e16649b70107
more explicit output of list items;
NEWS
lib/texinputs/isabelle.sty
src/Pure/Thy/markdown.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/NEWS	Sat Oct 17 19:32:01 2015 +0200
     1.2 +++ b/NEWS	Sat Oct 17 19:47:34 2015 +0200
     1.3 @@ -64,9 +64,12 @@
     1.4    \<^medskip>   \medskip
     1.5    \<^bigskip>   \bigskip
     1.6  
     1.7 -  \<^item>  \item  (itemize)
     1.8 -  \<^enum>  \item  (enumerate)
     1.9 -  \<^descr>  \item  (description)
    1.10 +* Paragraphs and nested lists may be specified similarly to Markdown,
    1.11 +with control symbols to indicate list items as follows:
    1.12 +
    1.13 +  \<^item>  itemize
    1.14 +  \<^enum>  enumerate
    1.15 +  \<^descr>  description
    1.16  
    1.17  
    1.18  *** Isar ***
     2.1 --- a/lib/texinputs/isabelle.sty	Sat Oct 17 19:32:01 2015 +0200
     2.2 +++ b/lib/texinputs/isabelle.sty	Sat Oct 17 19:47:34 2015 +0200
     2.3 @@ -43,9 +43,6 @@
     2.4  \def\isactrlsmallskip{\smallskip}
     2.5  \def\isactrlmedskip{\medskip}
     2.6  \def\isactrlbigskip{\bigskip}
     2.7 -\def\isactrlitem{\item}
     2.8 -\def\isactrlenum{\item}
     2.9 -\def\isactrldescr{\item}
    2.10  
    2.11  \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
    2.12  
     3.1 --- a/src/Pure/Thy/markdown.ML	Sat Oct 17 19:32:01 2015 +0200
     3.2 +++ b/src/Pure/Thy/markdown.ML	Sat Oct 17 19:47:34 2015 +0200
     3.3 @@ -24,6 +24,7 @@
     3.4    val print_kind: kind -> string
     3.5    type line
     3.6    val line_source: line -> Antiquote.text_antiquote list
     3.7 +  val line_is_item: line -> bool
     3.8    val line_content: line -> Antiquote.text_antiquote list
     3.9    val make_line: Antiquote.text_antiquote list -> line
    3.10    val empty_line: line
    3.11 @@ -63,6 +64,7 @@
    3.12  
    3.13  fun line_source (Line {source, ...}) = source;
    3.14  fun line_is_empty (Line {is_empty, ...}) = is_empty;
    3.15 +fun line_is_item (Line {item, ...}) = is_some item;
    3.16  fun line_content (Line {content, ...}) = content;
    3.17  
    3.18  
     4.1 --- a/src/Pure/Thy/thy_output.ML	Sat Oct 17 19:32:01 2015 +0200
     4.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Oct 17 19:47:34 2015 +0200
     4.3 @@ -192,9 +192,12 @@
     4.4      val output_antiquote = eval_antiquote state #> Symbol.explode #> Latex.output_ctrl_symbols;
     4.5      val output_antiquotes = map output_antiquote #> implode;
     4.6  
     4.7 +    fun output_line line =
     4.8 +      (if Markdown.line_is_item line then "\\item " else "") ^
     4.9 +        output_antiquotes (Markdown.line_content line);
    4.10 +
    4.11      fun output_blocks blocks = space_implode "\n\n" (map output_block blocks)
    4.12 -    and output_block (Markdown.Paragraph lines) =
    4.13 -          cat_lines (map (output_antiquotes o Markdown.line_source) lines)
    4.14 +    and output_block (Markdown.Paragraph lines) = cat_lines (map output_line lines)
    4.15        | output_block (Markdown.List {kind, body, ...}) =
    4.16            let val env = Markdown.print_kind kind in
    4.17              "%\n\\begin{" ^ env ^ "}%\n" ^