--- a/NEWS Fri Apr 01 15:32:25 2016 +0200
+++ b/NEWS Fri Apr 01 16:15:31 2016 +0200
@@ -9,6 +9,9 @@
*** General ***
+* Mixfix annotation syntax: "(\<open>unbreakable\<close>" supersedes "(00"; the old
+form has been discontinued. INCOMPATIBILITY.
+
* New symbol \<circle>, e.g. for temporal operator.
* Old 'header' command is no longer supported (legacy since
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Fri Apr 01 15:32:25 2016 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Fri Apr 01 16:15:31 2016 +0200
@@ -362,8 +362,7 @@
\<^descr> \<^verbatim>\<open>(\<close>\<open>n\<close> opens a pretty printing block. The optional number specifies how
much indentation to add when a line break occurs within the block. If the
- parenthesis is not followed by digits, the indentation defaults to 0. A
- block specified via \<^verbatim>\<open>(00\<close> is unbreakable.
+ parenthesis is not followed by digits, the indentation defaults to 0.
\<^descr> \<^verbatim>\<open>)\<close> closes a pretty printing block.
--- a/src/HOL/Complete_Lattices.thy Fri Apr 01 15:32:25 2016 +0200
+++ b/src/HOL/Complete_Lattices.thy Fri Apr 01 16:15:31 2016 +0200
@@ -975,8 +975,8 @@
"_INTER" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set" ("(3INT _:_./ _)" [0, 0, 10] 10)
syntax (latex output)
- "_INTER1" :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set" ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
- "_INTER" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set" ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
+ "_INTER1" :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set" ("(3\<Inter>(\<open>unbreakable\<close>\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
+ "_INTER" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set" ("(3\<Inter>(\<open>unbreakable\<close>\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
syntax
"_INTER1" :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set" ("(3\<Inter>_./ _)" [0, 10] 10)
@@ -1144,8 +1144,8 @@
"_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" [0, 0, 10] 10)
syntax (latex output)
- "_UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
- "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
+ "_UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>(\<open>unbreakable\<close>\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
+ "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>(\<open>unbreakable\<close>\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
syntax
"_UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>_./ _)" [0, 10] 10)
--- a/src/HOL/Set_Interval.thy Fri Apr 01 15:32:25 2016 +0200
+++ b/src/HOL/Set_Interval.thy Fri Apr 01 16:15:31 2016 +0200
@@ -66,10 +66,10 @@
"_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3INT _<_./ _)" [0, 0, 10] 10)
syntax (latex output)
- "_UNION_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00_ \<le> _)/ _)" [0, 0, 10] 10)
- "_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00_ < _)/ _)" [0, 0, 10] 10)
- "_INTER_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(00_ \<le> _)/ _)" [0, 0, 10] 10)
- "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(00_ < _)/ _)" [0, 0, 10] 10)
+ "_UNION_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(\<open>unbreakable\<close>_ \<le> _)/ _)" [0, 0, 10] 10)
+ "_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(\<open>unbreakable\<close>_ < _)/ _)" [0, 0, 10] 10)
+ "_INTER_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(\<open>unbreakable\<close>_ \<le> _)/ _)" [0, 0, 10] 10)
+ "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(\<open>unbreakable\<close>_ < _)/ _)" [0, 0, 10] 10)
syntax
"_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Union>_\<le>_./ _)" [0, 0, 10] 10)
--- a/src/Pure/PIDE/markup.ML Fri Apr 01 15:32:25 2016 +0200
+++ b/src/Pure/PIDE/markup.ML Fri Apr 01 16:15:31 2016 +0200
@@ -68,6 +68,7 @@
val docN: string val doc: string -> T
val markupN: string
val consistentN: string
+ val unbreakableN: string
val block_properties: string list
val indentN: string
val widthN: string
@@ -397,9 +398,10 @@
val markupN = "markup";
val consistentN = "consistent";
+val unbreakableN = "unbreakable";
val indentN = "indent";
-val block_properties = [markupN, consistentN, indentN];
+val block_properties = [markupN, consistentN, unbreakableN, indentN];
val widthN = "width";
--- a/src/Pure/Syntax/printer.ML Fri Apr 01 15:32:25 2016 +0200
+++ b/src/Pure/Syntax/printer.ML Fri Apr 01 16:15:31 2016 +0200
@@ -86,7 +86,7 @@
TypArg of int |
String of bool * string |
Break of int |
- Block of {markup: Markup.T, consistent: bool, indent: int} * symb list;
+ Block of Syntax_Ext.block_info * symb list;
type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;
@@ -202,11 +202,13 @@
then Pretty.marks_str (m @ [Lexicon.literal_markup s], s)
else Pretty.str s;
in (T :: Ts, args') end
- | synT m (Block (info, bsymbs) :: symbs, args) =
+ | synT m (Block ({markup, consistent, unbreakable, indent}, bsymbs) :: symbs, args) =
let
val (bTs, args') = synT m (bsymbs, args);
val (Ts, args'') = synT m (symbs, args');
- val T = Pretty.markup_block info bTs |> #indent info < 0 ? Pretty.unbreakable;
+ val T =
+ Pretty.markup_block {markup = markup, consistent = consistent, indent = indent} bTs
+ |> unbreakable ? Pretty.unbreakable;
in (T :: Ts, args'') end
| synT m (Break i :: symbs, args) =
let
--- a/src/Pure/Syntax/syntax_ext.ML Fri Apr 01 15:32:25 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML Fri Apr 01 16:15:31 2016 +0200
@@ -8,7 +8,7 @@
sig
datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int * Position.T
val typ_to_nonterm: typ -> string
- type block_info = {markup: Markup.T, consistent: bool, indent: int}
+ type block_info = {markup: Markup.T, consistent: bool, unbreakable: bool, indent: int}
val block_indent: int -> block_info
datatype xsymb =
Delim of string |
@@ -66,8 +66,10 @@
Space s: some white space for printing
Bg, Brk, En: blocks and breaks for pretty printing*)
-type block_info = {markup: Markup.T, consistent: bool, indent: int};
-fun block_indent indent = {markup = Markup.empty, consistent = false, indent = indent};
+type block_info = {markup: Markup.T, consistent: bool, unbreakable: bool, indent: int};
+
+fun block_indent indent : block_info =
+ {markup = Markup.empty, consistent = false, unbreakable = false, indent = indent};
datatype xsymb =
Delim of string |
@@ -220,14 +222,14 @@
else ();
val consistent = get_bool Markup.consistentN props;
+ val unbreakable = get_bool Markup.unbreakableN props;
val indent = get_nat Markup.indentN props;
- in Bg {markup = markup, consistent = consistent, indent = indent} end
+ in Bg {markup = markup, consistent = consistent, unbreakable = unbreakable, indent = indent} end
handle ERROR msg => error (msg ^
Markup.markup_report (Position.reported_text (#1 (Symbol_Pos.range ss)) Markup.keyword3 ""));
val read_block_indent =
- map Symbol_Pos.symbol #> (fn ss =>
- Bg (block_indent (if ss = ["0", "0"] then ~1 else #1 (Library.read_int ss))));
+ Bg o block_indent o #1 o Library.read_int o map Symbol_Pos.symbol;
val is_meta = member (op =) ["(", ")", "/", "_", "\<index>"];
--- a/src/Pure/pure_thy.ML Fri Apr 01 15:32:25 2016 +0200
+++ b/src/Pure/pure_thy.ML Fri Apr 01 16:15:31 2016 +0200
@@ -153,7 +153,7 @@
("_position", typ "float_token => float_position", Mixfix.mixfix "_"),
("_constify", typ "num_position => num_const", Mixfix.mixfix "_"),
("_constify", typ "float_position => float_const", Mixfix.mixfix "_"),
- ("_index", typ "logic => index", Mixfix.mixfix "(00\<^bsub>_\<^esub>)"),
+ ("_index", typ "logic => index", Mixfix.mixfix "(\<open>unbreakable\<close>\<^bsub>_\<^esub>)"),
("_indexdefault", typ "index", Mixfix.mixfix ""),
("_indexvar", typ "index", Mixfix.mixfix "'\<index>"),
("_struct", typ "index => logic", NoSyn),