explicit property for unbreakable block;
authorwenzelm
Fri Apr 01 16:15:31 2016 +0200 (2016-04-01)
changeset 62789ce15dd971965
parent 62788 374820748c70
child 62790 0c526d2fb609
explicit property for unbreakable block;
NEWS
src/Doc/Isar_Ref/Inner_Syntax.thy
src/HOL/Complete_Lattices.thy
src/HOL/Set_Interval.thy
src/Pure/PIDE/markup.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syntax_ext.ML
src/Pure/pure_thy.ML
     1.1 --- a/NEWS	Fri Apr 01 15:32:25 2016 +0200
     1.2 +++ b/NEWS	Fri Apr 01 16:15:31 2016 +0200
     1.3 @@ -9,6 +9,9 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Mixfix annotation syntax: "(\<open>unbreakable\<close>" supersedes "(00"; the old
     1.8 +form has been discontinued. INCOMPATIBILITY.
     1.9 +
    1.10  * New symbol \<circle>, e.g. for temporal operator.
    1.11  
    1.12  * Old 'header' command is no longer supported (legacy since
     2.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Fri Apr 01 15:32:25 2016 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Fri Apr 01 16:15:31 2016 +0200
     2.3 @@ -362,8 +362,7 @@
     2.4  
     2.5    \<^descr> \<^verbatim>\<open>(\<close>\<open>n\<close> opens a pretty printing block. The optional number specifies how
     2.6    much indentation to add when a line break occurs within the block. If the
     2.7 -  parenthesis is not followed by digits, the indentation defaults to 0. A
     2.8 -  block specified via \<^verbatim>\<open>(00\<close> is unbreakable.
     2.9 +  parenthesis is not followed by digits, the indentation defaults to 0.
    2.10  
    2.11    \<^descr> \<^verbatim>\<open>)\<close> closes a pretty printing block.
    2.12  
     3.1 --- a/src/HOL/Complete_Lattices.thy	Fri Apr 01 15:32:25 2016 +0200
     3.2 +++ b/src/HOL/Complete_Lattices.thy	Fri Apr 01 16:15:31 2016 +0200
     3.3 @@ -975,8 +975,8 @@
     3.4    "_INTER"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set"  ("(3INT _:_./ _)" [0, 0, 10] 10)
     3.5  
     3.6  syntax (latex output)
     3.7 -  "_INTER1"     :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
     3.8 -  "_INTER"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
     3.9 +  "_INTER1"     :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set"           ("(3\<Inter>(\<open>unbreakable\<close>\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
    3.10 +  "_INTER"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set"  ("(3\<Inter>(\<open>unbreakable\<close>\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
    3.11  
    3.12  syntax
    3.13    "_INTER1"     :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set"           ("(3\<Inter>_./ _)" [0, 10] 10)
    3.14 @@ -1144,8 +1144,8 @@
    3.15    "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 0, 10] 10)
    3.16  
    3.17  syntax (latex output)
    3.18 -  "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
    3.19 -  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
    3.20 +  "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(\<open>unbreakable\<close>\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
    3.21 +  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(\<open>unbreakable\<close>\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
    3.22  
    3.23  syntax
    3.24    "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" [0, 10] 10)
     4.1 --- a/src/HOL/Set_Interval.thy	Fri Apr 01 15:32:25 2016 +0200
     4.2 +++ b/src/HOL/Set_Interval.thy	Fri Apr 01 16:15:31 2016 +0200
     4.3 @@ -66,10 +66,10 @@
     4.4    "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3INT _<_./ _)" [0, 0, 10] 10)
     4.5  
     4.6  syntax (latex output)
     4.7 -  "_UNION_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ \<le> _)/ _)" [0, 0, 10] 10)
     4.8 -  "_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ < _)/ _)" [0, 0, 10] 10)
     4.9 -  "_INTER_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ \<le> _)/ _)" [0, 0, 10] 10)
    4.10 -  "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ < _)/ _)" [0, 0, 10] 10)
    4.11 +  "_UNION_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(\<open>unbreakable\<close>_ \<le> _)/ _)" [0, 0, 10] 10)
    4.12 +  "_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(\<open>unbreakable\<close>_ < _)/ _)" [0, 0, 10] 10)
    4.13 +  "_INTER_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(\<open>unbreakable\<close>_ \<le> _)/ _)" [0, 0, 10] 10)
    4.14 +  "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(\<open>unbreakable\<close>_ < _)/ _)" [0, 0, 10] 10)
    4.15  
    4.16  syntax
    4.17    "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Union>_\<le>_./ _)" [0, 0, 10] 10)
     5.1 --- a/src/Pure/PIDE/markup.ML	Fri Apr 01 15:32:25 2016 +0200
     5.2 +++ b/src/Pure/PIDE/markup.ML	Fri Apr 01 16:15:31 2016 +0200
     5.3 @@ -68,6 +68,7 @@
     5.4    val docN: string val doc: string -> T
     5.5    val markupN: string
     5.6    val consistentN: string
     5.7 +  val unbreakableN: string
     5.8    val block_properties: string list
     5.9    val indentN: string
    5.10    val widthN: string
    5.11 @@ -397,9 +398,10 @@
    5.12  
    5.13  val markupN = "markup";
    5.14  val consistentN = "consistent";
    5.15 +val unbreakableN = "unbreakable";
    5.16  val indentN = "indent";
    5.17  
    5.18 -val block_properties = [markupN, consistentN, indentN];
    5.19 +val block_properties = [markupN, consistentN, unbreakableN, indentN];
    5.20  
    5.21  val widthN = "width";
    5.22  
     6.1 --- a/src/Pure/Syntax/printer.ML	Fri Apr 01 15:32:25 2016 +0200
     6.2 +++ b/src/Pure/Syntax/printer.ML	Fri Apr 01 16:15:31 2016 +0200
     6.3 @@ -86,7 +86,7 @@
     6.4    TypArg of int |
     6.5    String of bool * string |
     6.6    Break of int |
     6.7 -  Block of {markup: Markup.T, consistent: bool, indent: int} * symb list;
     6.8 +  Block of Syntax_Ext.block_info * symb list;
     6.9  
    6.10  type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;
    6.11  
    6.12 @@ -202,11 +202,13 @@
    6.13                then Pretty.marks_str (m @ [Lexicon.literal_markup s], s)
    6.14                else Pretty.str s;
    6.15            in (T :: Ts, args') end
    6.16 -      | synT m (Block (info, bsymbs) :: symbs, args) =
    6.17 +      | synT m (Block ({markup, consistent, unbreakable, indent}, bsymbs) :: symbs, args) =
    6.18            let
    6.19              val (bTs, args') = synT m (bsymbs, args);
    6.20              val (Ts, args'') = synT m (symbs, args');
    6.21 -            val T = Pretty.markup_block info bTs |> #indent info < 0 ? Pretty.unbreakable;
    6.22 +            val T =
    6.23 +              Pretty.markup_block {markup = markup, consistent = consistent, indent = indent} bTs
    6.24 +              |> unbreakable ? Pretty.unbreakable;
    6.25            in (T :: Ts, args'') end
    6.26        | synT m (Break i :: symbs, args) =
    6.27            let
     7.1 --- a/src/Pure/Syntax/syntax_ext.ML	Fri Apr 01 15:32:25 2016 +0200
     7.2 +++ b/src/Pure/Syntax/syntax_ext.ML	Fri Apr 01 16:15:31 2016 +0200
     7.3 @@ -8,7 +8,7 @@
     7.4  sig
     7.5    datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int * Position.T
     7.6    val typ_to_nonterm: typ -> string
     7.7 -  type block_info = {markup: Markup.T, consistent: bool, indent: int}
     7.8 +  type block_info = {markup: Markup.T, consistent: bool, unbreakable: bool, indent: int}
     7.9    val block_indent: int -> block_info
    7.10    datatype xsymb =
    7.11      Delim of string |
    7.12 @@ -66,8 +66,10 @@
    7.13    Space s: some white space for printing
    7.14    Bg, Brk, En: blocks and breaks for pretty printing*)
    7.15  
    7.16 -type block_info = {markup: Markup.T, consistent: bool, indent: int};
    7.17 -fun block_indent indent = {markup = Markup.empty, consistent = false, indent = indent};
    7.18 +type block_info = {markup: Markup.T, consistent: bool, unbreakable: bool, indent: int};
    7.19 +
    7.20 +fun block_indent indent : block_info =
    7.21 +  {markup = Markup.empty, consistent = false, unbreakable = false, indent = indent};
    7.22  
    7.23  datatype xsymb =
    7.24    Delim of string |
    7.25 @@ -220,14 +222,14 @@
    7.26        else ();
    7.27  
    7.28      val consistent = get_bool Markup.consistentN props;
    7.29 +    val unbreakable = get_bool Markup.unbreakableN props;
    7.30      val indent = get_nat Markup.indentN props;
    7.31 -  in Bg {markup = markup, consistent = consistent, indent = indent} end
    7.32 +  in Bg {markup = markup, consistent = consistent, unbreakable = unbreakable, indent = indent} end
    7.33    handle ERROR msg => error (msg ^
    7.34      Markup.markup_report (Position.reported_text (#1 (Symbol_Pos.range ss)) Markup.keyword3 ""));
    7.35  
    7.36  val read_block_indent =
    7.37 -  map Symbol_Pos.symbol #> (fn ss =>
    7.38 -    Bg (block_indent (if ss = ["0", "0"] then ~1 else #1 (Library.read_int ss))));
    7.39 +  Bg o block_indent o #1 o Library.read_int o map Symbol_Pos.symbol;
    7.40  
    7.41  val is_meta = member (op =) ["(", ")", "/", "_", "\<index>"];
    7.42  
     8.1 --- a/src/Pure/pure_thy.ML	Fri Apr 01 15:32:25 2016 +0200
     8.2 +++ b/src/Pure/pure_thy.ML	Fri Apr 01 16:15:31 2016 +0200
     8.3 @@ -153,7 +153,7 @@
     8.4      ("_position",   typ "float_token => float_position", Mixfix.mixfix "_"),
     8.5      ("_constify",   typ "num_position => num_const",   Mixfix.mixfix "_"),
     8.6      ("_constify",   typ "float_position => float_const", Mixfix.mixfix "_"),
     8.7 -    ("_index",      typ "logic => index",              Mixfix.mixfix "(00\<^bsub>_\<^esub>)"),
     8.8 +    ("_index",      typ "logic => index",              Mixfix.mixfix "(\<open>unbreakable\<close>\<^bsub>_\<^esub>)"),
     8.9      ("_indexdefault", typ "index",                     Mixfix.mixfix ""),
    8.10      ("_indexvar",   typ "index",                       Mixfix.mixfix "'\<index>"),
    8.11      ("_struct",     typ "index => logic",              NoSyn),