# HG changeset patch
# User wenzelm
# Date 1459520131 -7200
# Node ID ce15dd971965141762ef8b20894b9d7fbbfde941
# Parent  374820748c70673777e5f4fe816096c1705403b9
explicit property for unbreakable block;

diff -r 374820748c70 -r ce15dd971965 NEWS
--- 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
diff -r 374820748c70 -r ce15dd971965 src/Doc/Isar_Ref/Inner_Syntax.thy
--- 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.
 
diff -r 374820748c70 -r ce15dd971965 src/HOL/Complete_Lattices.thy
--- 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)
diff -r 374820748c70 -r ce15dd971965 src/HOL/Set_Interval.thy
--- 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)
diff -r 374820748c70 -r ce15dd971965 src/Pure/PIDE/markup.ML
--- 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";
 
diff -r 374820748c70 -r ce15dd971965 src/Pure/Syntax/printer.ML
--- 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
diff -r 374820748c70 -r ce15dd971965 src/Pure/Syntax/syntax_ext.ML
--- 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>"];
 
diff -r 374820748c70 -r ce15dd971965 src/Pure/pure_thy.ML
--- 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),