--- 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 ***
--- 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}
--- 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}
--- 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
--- 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;
--- 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 =
--- 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,
--- 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 = [];