# HG changeset patch # User wenzelm # Date 1735756973 -3600 # Node ID 7c3f7e992889546e02a32ad1bbf5a00f7e823b1b # Parent bac9b067c768597574a6a6941c2ff141c47826e9# Parent dc105ee2d759f26f2c52913514432ef8b8fe3329 merged diff -r bac9b067c768 -r 7c3f7e992889 NEWS --- a/NEWS Sat Dec 28 21:20:33 2024 +0100 +++ b/NEWS Wed Jan 01 19:42:53 2025 +0100 @@ -209,15 +209,17 @@ \renewcommand{\isatconst}[1]{{\color{darkgray}#1}} \renewcommand{\isaconst}[1]{\textsl{\color{darkgray}#1}} -* LaTeX presentation of outer syntax keywords now distinguishes -keyword1, keyword2, keyword3 more carefully. This allows to imitate -Isabelle/jEdit rendering like this: +* LaTeX presentation now distinguishes keywords of outer and inner +syntax more carefully. This allows to imitate Isabelle/jEdit rendering +like this: \renewcommand{\isacommand}[1]{\isakeywordONE{#1}} \renewcommand{\isakeywordONE}[1]{\isakeyword{\color[RGB]{0,102,153}#1}} \renewcommand{\isakeywordTWO}[1]{\isakeyword{\color[RGB]{0,153,102}#1}} \renewcommand{\isakeywordTHREE}[1]{\isakeyword{\color[RGB]{0,153,255}#1}} + \renewcommand{\isaliteral}[1]{\isakeyword{\color[RGB]{0,102,153}#1}} + \renewcommand{\isadelimiter}[1]{#1} *** HOL *** diff -r bac9b067c768 -r 7c3f7e992889 lib/texinputs/isabelle.sty --- a/lib/texinputs/isabelle.sty Sat Dec 28 21:20:33 2024 +0100 +++ b/lib/texinputs/isabelle.sty Wed Jan 01 19:42:53 2025 +0100 @@ -154,6 +154,8 @@ \newcommand{\isakeywordONE}[1]{\isakeyword{#1}} \newcommand{\isakeywordTWO}[1]{\isakeyword{#1}} \newcommand{\isakeywordTHREE}[1]{\isakeyword{#1}} +\newcommand{\isaliteral}[1]{#1} +\newcommand{\isadelimiter}[1]{#1} \newcommand{\isatclass}[1]{#1} \newcommand{\isatconst}[1]{#1} \newcommand{\isatfree}[1]{#1} diff -r bac9b067c768 -r 7c3f7e992889 src/HOL/HOLCF/Tutorial/document/root.tex --- a/src/HOL/HOLCF/Tutorial/document/root.tex Sat Dec 28 21:20:33 2024 +0100 +++ b/src/HOL/HOLCF/Tutorial/document/root.tex Wed Jan 01 19:42:53 2025 +0100 @@ -2,6 +2,7 @@ % HOLCF/document/root.tex \documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} \usepackage{graphicx,isabelle,isabellesym,latexsym} \usepackage[only,bigsqcap]{stmaryrd} \usepackage{textcomp} diff -r bac9b067c768 -r 7c3f7e992889 src/HOL/ZF/document/root.tex --- a/src/HOL/ZF/document/root.tex Sat Dec 28 21:20:33 2024 +0100 +++ b/src/HOL/ZF/document/root.tex Wed Jan 01 19:42:53 2025 +0100 @@ -1,4 +1,5 @@ \documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} \usepackage{isabelle,isabellesym} % this should be the last package used diff -r bac9b067c768 -r 7c3f7e992889 src/Pure/General/latex.ML --- a/src/Pure/General/latex.ML Sat Dec 28 21:20:33 2024 +0100 +++ b/src/Pure/General/latex.ML Wed Jan 01 19:42:53 2025 +0100 @@ -244,13 +244,15 @@ local val markup_macro = YXML.output_markup o Markup.latex_macro; -val markup_indent = markup_macro "isaindent"; + val markup_latex = Symtab.make [(Markup.commandN, markup_macro "isakeywordONE"), (Markup.keyword1N, markup_macro "isakeywordONE"), (Markup.keyword2N, markup_macro "isakeywordTWO"), (Markup.keyword3N, markup_macro "isakeywordTHREE"), + (Markup.literalN, markup_macro "isaliteral"), + (Markup.delimiterN, markup_macro "isadelimiter"), (Markup.tclassN, markup_macro "isatclass"), (Markup.tconstN, markup_macro "isatconst"), (Markup.tfreeN, markup_macro "isatfree"), @@ -270,16 +272,13 @@ SOME (XML.Elem (m, _)) => latex_markup m | _ => Markup.no_output); -fun latex_indent s (_: int) = - if s = "" then s else uncurry enclose markup_indent s; - in fun output_ops opt_margin : Pretty.output_ops = {symbolic = false, output = output_width, markup = latex_markup_output, - indent = latex_indent, + indent_markup = markup_macro "isaindent", margin = ML_Pretty.get_margin opt_margin}; end; diff -r bac9b067c768 -r 7c3f7e992889 src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Sat Dec 28 21:20:33 2024 +0100 +++ b/src/Pure/General/pretty.ML Wed Jan 01 19:42:53 2025 +0100 @@ -75,7 +75,7 @@ {symbolic: bool, output: string -> Output.output * int, markup: Markup.output -> Markup.output, - indent: string -> int -> Output.output, + indent_markup: Markup.output, margin: int} val output_ops: int option -> output_ops val pure_output_ops: int option -> output_ops @@ -243,14 +243,14 @@ {symbolic: bool, output: string -> Output.output * int, markup: Markup.output -> Markup.output, - indent: string -> int -> Output.output, + indent_markup: Markup.output, margin: int}; fun make_output_ops {symbolic, markup} opt_margin : output_ops = {symbolic = symbolic, output = fn s => (s, size s), markup = markup, - indent = fn _ => Symbol.spaces, + indent_markup = Markup.no_output, margin = ML_Pretty.get_margin opt_margin}; val pure_output_ops = make_output_ops {symbolic = false, markup = K Markup.no_output}; @@ -264,14 +264,14 @@ fun output_newline (ops: output_ops) = #1 (#output ops "\n"); fun output_spaces (ops: output_ops) = #output ops o Symbol.spaces; -fun output_spaces_buffer ops = Buffer.add o #1 o output_spaces ops; fun output_spaces_bytes ops = Bytes.add o #1 o output_spaces ops; (* output tree *) datatype tree = - Block of + End (*end of markup*) + | Block of {markup: Markup.output, open_block: bool, consistent: bool, @@ -279,13 +279,12 @@ body: tree list, length: int} | Break of bool * int * int (*mandatory flag, width if not taken, extra indentation if taken*) - | Str of Output.output * int (*string output, length*) - | Raw of Output.output; (*raw output: no length, no indent*) + | Str of Output.output * int; (*string output, length*) -fun tree_length (Block {length = len, ...}) = len +fun tree_length End = 0 + | tree_length (Block {length = len, ...}) = len | tree_length (Break (_, wd, _)) = wd - | tree_length (Str (_, len)) = len - | tree_length (Raw _) = 0; + | tree_length (Str (_, len)) = len; local @@ -335,32 +334,57 @@ local -type text = {tx: Bytes.T, ind: Buffer.T, pos: int, nl: int}; +type context = Markup.output list; (*stack of pending markup*) + +abstype state = State of context * Bytes.T +with + +fun state_output (State (_, output)) = output; -val empty: text = - {tx = Bytes.empty, - ind = Buffer.empty, - pos = 0, - nl = 0}; +val empty_state = State ([], Bytes.empty); + +fun add_state s (State (context, output)) = + State (context, Bytes.add s output); + +fun push_state (markup as (bg, _)) (State (context, output)) = + State (markup :: context, Bytes.add bg output); -fun newline s {tx, ind = _, pos = _, nl} : text = - {tx = Bytes.add s tx, - ind = Buffer.empty, - pos = 0, - nl = nl + 1}; +fun pop_state (State ((_, en) :: context, output)) = + State (context, Bytes.add en output); + +fun close_state (State (context, output)) = + State ([], fold (Bytes.add o #2) context output); + +fun reopen_state (State (old_context, _)) (State (context, output)) = + State (old_context @ context, fold_rev (Bytes.add o #1) old_context output); -fun string (s, len) {tx, ind, pos: int, nl} : text = - {tx = Bytes.add s tx, - ind = Buffer.add s ind, +end; + +type text = {main: state, line: state option, pos: int, nl: int}; + +val empty: text = {main = empty_state, line = NONE, pos = 0, nl = 0}; +val empty_line: text = {main = empty_state, line = SOME empty_state, pos = 0, nl = 0}; + +fun string (s, len) {main, line, pos, nl} : text = + {main = add_state s main, + line = Option.map (add_state s) line, pos = pos + len, nl = nl}; -fun raw s {tx, ind, pos: int, nl} : text = - {tx = Bytes.add s tx, - ind = ind, +fun push m {main, line, pos, nl} : text = + {main = push_state m main, + line = Option.map (push_state m) line, pos = pos, nl = nl}; +fun pop {main, line, pos, nl} : text = + {main = pop_state main, + line = Option.map pop_state line, + pos = pos, + nl = nl}; + +fun result ({main, ...}: text) = state_output main; + (*Add the lengths of the expressions until the next Break; if no Break then include "after", to account for text following this block.*) fun break_dist (Break _ :: _, _) = 0 @@ -374,6 +398,8 @@ | force_next ((prt as Break _) :: prts) = force_break prt :: prts | force_next (prt :: prts) = prt :: force_next prts; +nonfix before; + in fun format_tree (ops: output_ops) input = @@ -382,53 +408,68 @@ val breakgain = margin div 20; (*minimum added space required of a break*) val emergencypos = margin div 2; (*position too far to right*) - val linebreak = newline (output_newline ops); + fun blanks_state n state = add_state (#1 (output_spaces ops n)) state; val blanks = string o output_spaces ops; - val blanks_buffer = output_spaces_buffer ops; + + val indent_markup = #indent_markup ops; + val no_indent_markup = indent_markup = Markup.no_output; - fun indentation (buf, len) {tx, ind, pos, nl} : text = - let val s = Buffer.content buf in - {tx = Bytes.add (#indent ops s len) tx, - ind = Buffer.add s ind, - pos = pos + len, - nl = nl} - end; + val break_state = add_state (output_newline ops); + fun break (state, pos) ({main, nl, ...}: text) : text = + let + val (main', line') = + if no_indent_markup then + (main |> break_state |> add_state (Symbol.spaces pos), NONE) + else + let + val ss = Bytes.contents (state_output (the state)); + val main' = + if null ss then main |> break_state + else + main |> close_state |> break_state + |> push_state indent_markup |> fold add_state ss |> pop_state + |> reopen_state main; + val line' = empty_state |> fold add_state ss |> reopen_state main; + in (main', SOME line') end; + in {main = main', line = line', pos = pos, nl = nl + 1} end; - (*blockin is the indentation of the current block; - after is the width of the following context until next break.*) - fun format ([], _, _) text = text - | format (prt :: prts, block as (_, blockin), after) (text as {ind, pos, nl, ...}) = - (case prt of - Block {markup = (bg, en), open_block = true, body, ...} => - format (Raw bg :: body @ Raw en :: prts, block, after) text - | Block {markup = (bg, en), consistent, indent, body, length = blen, ...} => - let - val pos' = pos + indent; - val pos'' = pos' mod emergencypos; - val block' = - if pos' < emergencypos then (ind |> blanks_buffer indent, pos') - else (blanks_buffer pos'' Buffer.empty, pos''); - val d = break_dist (prts, after) - val body' = body |> (consistent andalso pos + blen > margin - d) ? map force_break; - val btext: text = text - |> raw bg - |> format (body', block', d) - |> raw en; - (*if this block was broken then force the next break*) - val prts' = if nl < #nl btext then force_next prts else prts; - in format (prts', block, after) btext end - | Break (force, wd, ind) => - (*no break if text to next break fits on this line - or if breaking would add only breakgain to space*) - format (prts, block, after) - (if not force andalso - pos + wd <= Int.max (margin - break_dist (prts, after), blockin + breakgain) - then text |> blanks wd (*just insert wd blanks*) - else text |> linebreak |> indentation block |> blanks ind) - | Str str => format (prts, block, after) (string str text) - | Raw s => format (prts, block, after) (raw s text)); + (*'before' is the indentation context of the current block*) + (*'after' is the width of the input context until the next break*) + fun format (trees, before, after) (text as {pos, ...}) = + (case trees of + [] => text + | End :: ts => format (ts, before, after) (pop text) + | Block {markup, open_block = true, body, ...} :: ts => + text |> push markup |> format (body @ End :: ts, before, after) + | Block {markup, consistent, indent, body, length = blen, ...} :: ts => + let + val pos' = pos + indent; + val pos'' = pos' mod emergencypos; + val before' = + if pos' < emergencypos + then (Option.map (close_state o blanks_state indent) (#line text), pos') + else (Option.map (fn _ => blanks_state pos'' empty_state) (#line text), pos''); + val after' = break_dist (ts, after) + val body' = body + |> (consistent andalso pos + blen > margin - after') ? map force_break; + val btext: text = + text |> push markup |> format (body' @ [End], before', after'); + (*if this block was broken then force the next break*) + val ts' = if #nl text < #nl btext then force_next ts else ts; + in format (ts', before, after) btext end + | Break (force, wd, ind) :: ts => + (*no break if text to next break fits on this line + or if breaking would add only breakgain to space*) + format (ts, before, after) + (if not force andalso + pos + wd <= Int.max (margin - break_dist (ts, after), #2 before + breakgain) + then text |> blanks wd (*just insert wd blanks*) + else text |> break before |> blanks ind) + | Str str :: ts => format (ts, before, after) (string str text)); + + val init = if no_indent_markup then empty else empty_line; in - #tx (format ([output_tree ops true input], (Buffer.empty, 0), 0) empty) + result (format ([output_tree ops true input], (#line init, 0), 0) init) end; end; @@ -447,7 +488,8 @@ let val (bg, en) = #markup ops (YXML.output_markup m) in Bytes.add bg #> output_body #> Bytes.add en end; - fun output (Block {markup = (bg, en), body = [], ...}) = Bytes.add bg #> Bytes.add en + fun output End = I + | output (Block {markup = (bg, en), body = [], ...}) = Bytes.add bg #> Bytes.add en | output (Block {markup = (bg, en), open_block = true, body, ...}) = Bytes.add bg #> fold output body #> Bytes.add en | output (Block {markup = (bg, en), consistent, indent, body, ...}) = @@ -456,8 +498,7 @@ | output (Break (false, wd, ind)) = markup_bytes (Markup.break {width = wd, indent = ind}) (output_spaces_bytes ops wd) | output (Break (true, _, _)) = Bytes.add (output_newline ops) - | output (Str (s, _)) = Bytes.add s - | output (Raw s) = Bytes.add s; + | output (Str (s, _)) = Bytes.add s; in Bytes.build o output o output_tree ops false end; val symbolic_string_of = Bytes.content o symbolic_output; @@ -467,11 +508,11 @@ fun unformatted ops = let - fun output (Block ({markup = (bg, en), body, ...})) = + fun output End = I + | output (Block ({markup = (bg, en), body, ...})) = Bytes.add bg #> fold output body #> Bytes.add en | output (Break (_, wd, _)) = output_spaces_bytes ops wd - | output (Str (s, _)) = Bytes.add s - | output (Raw s) = Bytes.add s; + | output (Str (s, _)) = Bytes.add s; in Bytes.build o output o output_tree ops false end; fun unformatted_string_of prt = diff -r bac9b067c768 -r 7c3f7e992889 src/Pure/General/pretty.scala --- a/src/Pure/General/pretty.scala Sat Dec 28 21:20:33 2024 +0100 +++ b/src/Pure/General/pretty.scala Wed Jan 01 19:42:53 2025 +0100 @@ -60,10 +60,22 @@ private def force_nat(i: Int): Int = i max 0 + type Markup_Body = (Markup, Option[XML.Body]) + val no_markup: Markup_Body = (Markup.Empty, None) + val item_markup: Markup_Body = (Markup.Expression.item, None) + + def markup_elem(markup: Markup_Body, body: XML.Body): XML.Elem = + markup match { + case (m, None) => XML.Elem(m, body) + case (m1, Some(m2)) => XML.Wrapped_Elem(m1, m2, body) + } + private sealed abstract class Tree { def length: Double } + private case object End extends Tree { + override def length: Double = 0.0 + } private case class Block( - markup: Markup, - markup_body: Option[XML.Body], + markup: Markup_Body, open_block: Boolean, consistent: Boolean, indent: Int, @@ -78,8 +90,7 @@ private val FBreak = Break(true, 1, 0) private def make_block(body: List[Tree], - markup: Markup = Markup.Empty, - markup_body: Option[XML.Body] = None, + markup: Markup_Body = no_markup, open_block: Boolean = false, consistent: Boolean = false, indent: Int = 0 @@ -96,7 +107,7 @@ case Nil => len1 } } - Block(markup, markup_body, open_block, consistent, indent1, body, body_length(body, 0.0)) + Block(markup, open_block, consistent, indent1, body, body_length(body, 0.0)) } @@ -107,8 +118,8 @@ def unbreakable(input: XML.Body): XML.Body = input flatMap { - case XML.Wrapped_Elem(markup, body1, body2) => - List(XML.Wrapped_Elem(markup, body1, unbreakable(body2))) + case XML.Wrapped_Elem(markup1, markup2, body) => + List(XML.Wrapped_Elem(markup1, markup2, unbreakable(body))) case XML.Elem(Markup.Break(width, _), _) => spaces(width) case XML.Elem(markup, body) => List(XML.Elem(markup, unbreakable(body))) case XML.Text(text) => XML.string(split_lines(text).mkString(Symbol.space)) @@ -120,12 +131,43 @@ /* formatting */ - private sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0) { - def newline: Text = copy(tx = fbrk :: tx, pos = 0.0, nl = nl + 1) + private type State = List[(Markup_Body, List[XML.Tree])] + private val init_state: State = List((no_markup, Nil)) + + private sealed case class Text( + state: State = init_state, + pos: Double = 0.0, + nl: Int = 0 + ) { + def add(t: XML.Tree, len: Double = 0.0): Text = + (state: @unchecked) match { + case (m, ts) :: rest => copy(state = (m, t :: ts) :: rest, pos = pos + len) + } + + def push(m: Markup_Body): Text = + copy(state = (m, Nil) :: state) + + def pop: Text = + (state: @unchecked) match { + case (m1, ts1) :: (m2, ts2) :: rest => + copy(state = (m2, markup_elem(m1, ts1.reverse) :: ts2) :: rest) + } + + def result: XML.Body = + (state: @unchecked) match { + case List((m, ts)) if m == no_markup => ts.reverse + } + + def reset: Text = copy(state = init_state) + def restore(other: Text): Text = copy(state = other.state) + + def newline: Text = add(fbrk).copy(pos = 0.0, nl = nl + 1) + def string(s: String, len: Double): Text = - copy(tx = if (s == "") tx else XML.Text(s) :: tx, pos = pos + len) + if (s.isEmpty) copy(pos = pos + len) + else add(XML.Text(s), len = len) + def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble) - def content: XML.Body = tx.reverse } private def break_dist(trees: List[Tree], after: Double): Double = @@ -158,65 +200,54 @@ def make_tree(inp: XML.Body): List[Tree] = inp flatMap { - case XML.Wrapped_Elem(markup, body1, body2) => - List(make_block(make_tree(body2), markup = markup, markup_body = Some(body1))) + case XML.Wrapped_Elem(markup1, markup2, body) => + List(make_block(make_tree(body), markup = (markup1, Some(markup2)), open_block = true)) case XML.Elem(markup, body) => markup match { case Markup.Block(consistent, indent) => - List( - make_block(make_tree(body), - consistent = consistent, indent = indent, open_block = false)) + List(make_block(make_tree(body), consistent = consistent, indent = indent)) case Markup.Break(width, indent) => List(Break(false, force_nat(width), force_nat(indent))) case Markup(Markup.ITEM, _) => - List(make_block(make_tree(bullet ::: body), - markup = Markup.Expression.item, indent = 2)) + List(make_block(make_tree(bullet ::: body), markup = item_markup, indent = 2)) case _ => - List(make_block(make_tree(body), markup = markup, open_block = true)) + List(make_block(make_tree(body), markup = (markup, None), open_block = true)) } case XML.Text(text) => Library.separate(FBreak, split_lines(text).map(s => Str(s, metric(s)))) } - def format(trees: List[Tree], blockin: Int, after: Double, text: Text): Text = + def format(trees: List[Tree], before: Double, after: Double, text: Text): Text = trees match { case Nil => text - + case End :: ts => format(ts, before, after, text.pop) case (block: Block) :: ts if block.open_block => - val btext = format(block.body, blockin, break_dist(ts, after), text.copy(tx = Nil)) - val ts1 = if (text.nl < btext.nl) force_next(ts) else ts - val btext1 = btext.copy(tx = XML.Elem(block.markup, btext.content) :: text.tx) - format(ts1, blockin, after, btext1) - - case Block(markup, markup_body, _, consistent, indent, body, blen) :: ts => - val pos1 = (text.pos + indent).ceil.toInt - val pos2 = pos1 % emergencypos - val blockin1 = if (pos1 < emergencypos) pos1 else pos2 - val d = break_dist(ts, after) - val body1 = if (consistent && text.pos + blen > margin - d) force_all(body) else body - val btext = - if (markup.is_empty && markup_body.isEmpty) format(body1, blockin1, d, text) + format(block.body ::: End :: ts, before, after, text.push(block.markup)) + case (block: Block) :: ts => + val pos1 = text.pos + block.indent + val pos2 = (pos1.round.toInt % emergencypos).toDouble + val before1 = if (pos1 < emergencypos) pos1 else pos2 + val after1 = break_dist(ts, after) + val body1 = + if (block.consistent && text.pos + block.length > margin - after1) force_all(block.body) + else block.body + val btext1 = + if (block.markup == no_markup) format(body1, before1, after1, text) else { - val btext0 = format(body1, blockin1, d, text.copy(tx = Nil)) - val elem = - markup_body match { - case None => XML.Elem(markup, btext0.content) - case Some(body1) => XML.Wrapped_Elem(markup, body1, btext0.content) - } - btext0.copy(tx = elem :: text.tx) + val btext = format(body1, before1, after1, text.reset) + val elem = markup_elem(block.markup, btext.result) + btext.restore(text.add(elem)) } - val ts1 = if (text.nl < btext.nl) force_next(ts) else ts - format(ts1, blockin, after, btext) - + val ts1 = if (text.nl < btext1.nl) force_next(ts) else ts + format(ts1, before, after, btext1) case Break(force, wd, ind) :: ts => if (!force && - text.pos + wd <= ((margin - break_dist(ts, after)) max (blockin + breakgain))) - format(ts, blockin, after, text.blanks(wd)) - else format(ts, blockin, after, text.newline.blanks(blockin + ind)) - - case Str(s, len) :: ts => format(ts, blockin, after, text.string(s, len)) + text.pos + wd <= ((margin - break_dist(ts, after)) max (before + breakgain))) + format(ts, before, after, text.blanks(wd)) + else format(ts, before, after, text.newline.blanks((before + ind).ceil.toInt)) + case Str(s, len) :: ts => format(ts, before, after, text.string(s, len)) } - format(make_tree(input), 0, 0.0, Text()).content + format(make_tree(input), 0.0, 0.0, Text()).result } def string_of(input: XML.Body, diff -r bac9b067c768 -r 7c3f7e992889 src/Pure/ML/ml_pretty.ML --- a/src/Pure/ML/ml_pretty.ML Sat Dec 28 21:20:33 2024 +0100 +++ b/src/Pure/ML/ml_pretty.ML Wed Jan 01 19:42:53 2025 +0100 @@ -61,12 +61,13 @@ (* open_block flag *) -val open_block = ContextProperty ("open_block", "true"); +val open_block = ContextProperty ("open_block", ""); -val open_block_detect = List.exists (fn c => c = open_block); +val open_block_detect = + List.exists (fn ContextProperty ("open_block", _) => true | _ => false); -fun open_block_context false = [] - | open_block_context true = [open_block]; +fun open_block_context true = [open_block] + | open_block_context false = [];