--- a/NEWS Fri Apr 01 15:17:11 2016 +0200
+++ b/NEWS Fri Apr 01 22:33:31 2016 +0200
@@ -9,6 +9,12 @@
*** General ***
+* Mixfix annotations support general block properties, with syntax
+"(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent",
+"unbreakable", "markup". The existing notation "(DIGITS" is equivalent
+to "(\<open>indent=DIGITS\<close>". The former notation "(00" for unbreakable blocks
+is superseded by "(\<open>unbreabable\<close>" --- rare INCOMPATIBILITY.
+
* New symbol \<circle>, e.g. for temporal operator.
* Old 'header' command is no longer supported (legacy since
--- a/etc/options Fri Apr 01 15:17:11 2016 +0200
+++ b/etc/options Fri Apr 01 22:33:31 2016 +0200
@@ -68,6 +68,7 @@
-- "level of tracing information for multithreading"
option threads_stack_limit : real = 0.25
-- "maximum stack size for worker threads (in giga words, 0 = unlimited)"
+
public option parallel_print : bool = true
-- "parallel and asynchronous printing of results"
public option parallel_proofs : int = 2
@@ -75,6 +76,9 @@
option parallel_subproofs_threshold : real = 0.01
-- "lower bound of timing estimate for forked nested proofs (seconds)"
+option command_timing_threshold : real = 0.01
+ -- "default threshold for persistent command timing (seconds)"
+
section "Detail of Proof Checking"
@@ -175,4 +179,3 @@
public option completion_limit : int = 40
-- "limit for completion within the formal context"
-
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Fri Apr 01 22:33:31 2016 +0200
@@ -286,7 +286,7 @@
@'binder' @{syntax template} prios? @{syntax nat} |
@'structure') ')'
;
- template: string
+ @{syntax template}: string
;
prios: '[' (@{syntax nat} + ',') ']'
\<close>}
@@ -342,6 +342,7 @@
\<^verbatim>\<open>(\<close> & open parenthesis \\
\<^verbatim>\<open>)\<close> & close parenthesis \\
\<^verbatim>\<open>/\<close> & slash \\
+ \<open>\<open> \<close>\<close> & cartouche delimiters \\
\end{tabular}
\<^medskip>
@@ -360,10 +361,13 @@
\<^descr> \<open>s\<close> is a non-empty sequence of spaces for printing. This and the following
specifications do not affect parsing at all.
- \<^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.
+ \<^descr> \<^verbatim>\<open>(\<close>\<open>n\<close> opens a pretty printing block. The optional natural number
+ specifies the block indentation, i.e. how much spaces to add when a line
+ break occurs within the block. The default indentation is 0.
+
+ \<^descr> \<^verbatim>\<open>(\<close>\<open>\<open>properties\<close>\<close> opens a pretty printing block, with properties
+ specified within the given text cartouche. The syntax and semantics of
+ the category @{syntax_ref mixfix_properties} is described below.
\<^descr> \<^verbatim>\<open>)\<close> closes a pretty printing block.
@@ -374,8 +378,39 @@
is \<^emph>\<open>not\<close> taken.
- The general idea of pretty printing with blocks and breaks is also described
- in @{cite "paulson-ml2"}; it goes back to @{cite "Oppen:1980"}.
+ \<^medskip>
+ Block properties allow more control over the details of pretty-printed
+ output. The concrete syntax is defined as follows.
+
+ @{rail \<open>
+ @{syntax_def "mixfix_properties"}: (entry *)
+ ;
+ entry: atom ('=' atom)?
+ ;
+ atom: @{syntax ident} | @{syntax int} | @{syntax float} | @{syntax cartouche}
+ \<close>}
+
+ Each @{syntax entry} is a name-value pair: if the value is omitted, if
+ defaults to \<^verbatim>\<open>true\<close> (intended for Boolean properties). The following
+ standard block properties are supported:
+
+ \<^item> \<open>indent\<close> (natural number): the block indentation --- the same as for the
+ simple syntax without block properties.
+
+ \<^item> \<open>consistent\<close> (Boolean): this block has consistent breaks (if one break
+ is taken, all breaks are taken).
+
+ \<^item> \<open>unbreakable\<close> (Boolean): all possible breaks of the block are disabled
+ (turned into spaces).
+
+ \<^item> \<open>markup\<close> (string): the optional name of the markup node. If this is
+ provided, all remaining properties are turned into its XML attributes.
+ This allows to specify free-form PIDE markup, e.g.\ for specialized
+ output.
+
+ \<^medskip>
+ Note that the general idea of pretty printing with blocks and breaks is
+ described in @{cite "paulson-ml2"}; it goes back to @{cite "Oppen:1980"}.
\<close>
--- a/src/HOL/Complete_Lattices.thy Fri Apr 01 15:17:11 2016 +0200
+++ b/src/HOL/Complete_Lattices.thy Fri Apr 01 22:33: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/Eisbach/method_closure.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/HOL/Eisbach/method_closure.ML Fri Apr 01 22:33:31 2016 +0200
@@ -85,8 +85,7 @@
SOME (text, range) =>
if Method.checked_text text then text
else (Method.report (text, range); Method.check_text ctxt text)
- | NONE =>
- error ("Failed to parse method" ^ Position.here (Position.set_range (Token.range_of src))));
+ | NONE => error ("Failed to parse method" ^ Position.here (#1 (Token.range_of src))));
fun read_closure ctxt src0 =
let
--- a/src/HOL/Set_Interval.thy Fri Apr 01 15:17:11 2016 +0200
+++ b/src/HOL/Set_Interval.thy Fri Apr 01 22:33: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/HOL/ex/Hebrew.thy Fri Apr 01 15:17:11 2016 +0200
+++ b/src/HOL/ex/Hebrew.thy Fri Apr 01 22:33:31 2016 +0200
@@ -10,7 +10,20 @@
imports Main
begin
-text \<open>The Hebrew Alef-Bet (א-ב).\<close>
+subsection \<open>Warning: formal Unicode considered harmful\<close>
+
+text \<open>
+ Important note: editors or browsers that implement the \<^emph>\<open>Unicode
+ Bidirectional Algorithm\<close> correctly (!) will display the following mix of
+ left-to-right versus right-to-left characters in a way that is logical
+ nonsense.
+
+ To avoid such uncertainty, formal notation should be restricted to
+ well-known Isabelle symbols and their controlled rendering (in Unicode or
+ LaTeX).
+\<close>
+
+subsection \<open>The Hebrew Alef-Bet (א-ב).\<close>
datatype alef_bet =
Alef ("א")
@@ -39,9 +52,9 @@
thm alef_bet.induct
-text \<open>Interpreting Hebrew letters as numbers.\<close>
+subsection \<open>Interpreting Hebrew letters as numbers.\<close>
-primrec mispar :: "alef_bet => nat"
+primrec mispar :: "alef_bet \<Rightarrow> nat"
where
"mispar א = 1"
| "mispar ב = 2"
--- a/src/Pure/General/antiquote.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/General/antiquote.ML Fri Apr 01 22:33:31 2016 +0200
@@ -37,7 +37,7 @@
fun range ants =
if null ants then Position.no_range
- else Position.range (#1 (antiquote_range (hd ants))) (#2 (antiquote_range (List.last ants)));
+ else Position.range (#1 (antiquote_range (hd ants)), #2 (antiquote_range (List.last ants)));
(* split lines *)
@@ -110,9 +110,9 @@
Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace")
(Scan.repeats scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) >>
(fn (pos1, (pos2, ((body, pos3), pos4))) =>
- {start = Position.set_range (pos1, pos2),
- stop = Position.set_range (pos3, pos4),
- range = Position.range pos1 pos4,
+ {start = Position.range_position (pos1, pos2),
+ stop = Position.range_position (pos3, pos4),
+ range = Position.range (pos1, pos4),
body = body});
val scan_antiquote =
--- a/src/Pure/General/position.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/General/position.ML Fri Apr 01 22:33:31 2016 +0200
@@ -51,9 +51,9 @@
val here_list: T list -> string
type range = T * T
val no_range: range
- val set_range: range -> T
- val reset_range: T -> T
- val range: T -> T -> range
+ val no_range_position: T -> T
+ val range_position: range -> T
+ val range: T * T -> range
val range_of_properties: Properties.T -> range
val properties_of_range: range -> Properties.T
val thread_data: unit -> T
@@ -214,7 +214,7 @@
else s1 ^ Markup.markup (Markup.properties props Markup.position) s2
end;
-val here_list = space_implode " " o map here;
+val here_list = implode o map here;
(* range *)
@@ -223,10 +223,9 @@
val no_range = (none, none);
-fun set_range (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props);
-fun reset_range (Pos ((i, j, _), props)) = Pos ((i, j, 0), props);
-
-fun range pos pos' = (set_range (pos, pos'), pos');
+fun no_range_position (Pos ((i, j, _), props)) = Pos ((i, j, 0), props);
+fun range_position (Pos ((i, j, _), props), Pos ((_, j', _), _)) = Pos ((i, j, j'), props);
+fun range (pos, pos') = (range_position (pos, pos'), no_range_position pos');
fun range_of_properties props =
let
--- a/src/Pure/General/pretty.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/General/pretty.ML Fri Apr 01 22:33:31 2016 +0200
@@ -23,7 +23,9 @@
val default_indent: string -> int -> Output.output
val add_mode: string -> (string -> int -> Output.output) -> unit
type T
- val make_block: Output.output * Output.output -> bool -> int -> T list -> T
+ val make_block: {markup: Output.output * Output.output, consistent: bool, indent: int} ->
+ T list -> T
+ val markup_block: {markup: Markup.T, consistent: bool, indent: int} -> T list -> T
val str: string -> T
val brk: int -> T
val brk_indent: int -> int -> T
@@ -72,7 +74,7 @@
val block_enclose: T * T -> T list -> T
val writeln_chunks: T list -> unit
val writeln_chunks2: T list -> unit
- val to_ML: int -> T -> ML_Pretty.pretty
+ val to_ML: FixedInt.int -> T -> ML_Pretty.pretty
val from_ML: ML_Pretty.pretty -> T
val to_polyml: T -> PolyML.pretty
val from_polyml: PolyML.pretty -> T
@@ -108,6 +110,8 @@
(** printing items: compound phrases, strings, and breaks **)
+val force_nat = Integer.max 0;
+
abstype T =
Block of (Output.output * Output.output) * bool * int * T list * int
(*markup output, consistent, indentation, body, length*)
@@ -119,8 +123,9 @@
| length (Break (_, wd, _)) = wd
| length (Str (_, len)) = len;
-fun make_block markup consistent indent body =
+fun make_block {markup, consistent, indent} body =
let
+ val indent' = force_nat indent;
fun body_length prts len =
let
val (line, rest) = take_prefix (fn Break (true, _, _) => false | _ => true) prts;
@@ -128,32 +133,34 @@
in
(case rest of
Break (true, _, ind) :: rest' =>
- body_length (Break (false, indent + ind, 0) :: rest') len'
+ body_length (Break (false, indent' + ind, 0) :: rest') len'
| [] => len')
end;
- in Block (markup, consistent, indent, body, body_length body 0) end;
+ in Block (markup, consistent, indent', body, body_length body 0) end;
-fun markup_block markup indent es =
- make_block (Markup.output markup) false indent es;
+fun markup_block {markup, consistent, indent} es =
+ make_block {markup = Markup.output markup, consistent = consistent, indent = indent} es;
(** derived operations to create formatting expressions **)
-val str = Str o Output.output_width;
+val str = Output.output_width ##> force_nat #> Str;
-fun brk wd = Break (false, wd, 0);
-fun brk_indent wd ind = Break (false, wd, ind);
+fun brk wd = Break (false, force_nat wd, 0);
+fun brk_indent wd ind = Break (false, force_nat wd, ind);
val fbrk = Break (true, 1, 0);
fun breaks prts = Library.separate (brk 1) prts;
fun fbreaks prts = Library.separate fbrk prts;
-fun blk (ind, es) = markup_block Markup.empty ind es;
+fun blk (indent, es) =
+ markup_block {markup = Markup.empty, consistent = false, indent = indent} es;
+
fun block prts = blk (2, prts);
val strs = block o breaks o map str;
-fun markup m = markup_block m 0;
+fun markup m = markup_block {markup = m, consistent = false, indent = 0};
fun mark m prt = if m = Markup.empty then prt else markup m [prt];
fun mark_str (m, s) = mark m (str s);
fun marks_str (ms, s) = fold_rev mark ms (str s);
@@ -384,10 +391,11 @@
| to_ML _ (Str (s, len)) = ML_Pretty.String (s, FixedInt.fromInt len);
fun from_ML (ML_Pretty.Block (m, consistent, indent, prts)) =
- make_block m consistent (FixedInt.toInt indent) (map from_ML prts)
+ make_block {markup = m, consistent = consistent, indent = FixedInt.toInt indent}
+ (map from_ML prts)
| from_ML (ML_Pretty.Break (force, wd, ind)) =
Break (force, FixedInt.toInt wd, FixedInt.toInt ind)
- | from_ML (ML_Pretty.String (s, len)) = Str (s, FixedInt.toInt len);
+ | from_ML (ML_Pretty.String (s, len)) = Str (s, FixedInt.toInt (force_nat len));
val to_polyml = to_ML ~1 #> ML_Pretty.to_polyml;
val from_polyml = ML_Pretty.from_polyml #> from_ML;
--- a/src/Pure/General/pretty.scala Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/General/pretty.scala Fri Apr 01 22:33:31 2016 +0200
@@ -64,6 +64,8 @@
indent: Int,
body: List[Tree]): Tree =
{
+ val indent1 = force_nat(indent)
+
def body_length(prts: List[Tree], len: Double): Double =
{
val (line, rest) =
@@ -71,16 +73,18 @@
val len1 = ((0.0 /: line) { case (l, t) => l + t.length }) max len
rest match {
case Break(true, _, ind) :: rest1 =>
- body_length(Break(false, indent + ind, 0) :: rest1, len1)
+ body_length(Break(false, indent1 + ind, 0) :: rest1, len1)
case Nil => len1
}
}
- Block(markup, consistent, indent, body, body_length(body, 0.0))
+ Block(markup, consistent, indent1, body, body_length(body, 0.0))
}
/* formatted output */
+ private def force_nat(i: Int): Int = i max 0
+
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)
@@ -125,7 +129,7 @@
case Markup.Block(consistent, indent) =>
List(make_block(None, consistent, indent, make_tree(body)))
case Markup.Break(width, indent) =>
- List(Break(false, width, indent))
+ List(Break(false, force_nat(width), force_nat(indent)))
case Markup(Markup.ITEM, _) =>
List(make_block(None, false, 2,
make_tree(XML.elem(Markup.BULLET, space) :: space ::: body)))
--- a/src/Pure/General/symbol.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/General/symbol.ML Fri Apr 01 22:33:31 2016 +0200
@@ -13,6 +13,7 @@
val open_: symbol
val close: symbol
val space: symbol
+ val is_space: symbol -> bool
val comment: symbol
val is_char: symbol -> bool
val is_utf8: symbol -> bool
@@ -99,6 +100,7 @@
val close = "\<close>";
val space = chr 32;
+fun is_space s = s = space;
local
val small_spaces = Vector.tabulate (65, fn i => replicate_string i space);
--- a/src/Pure/General/symbol_pos.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/General/symbol_pos.ML Fri Apr 01 22:33:31 2016 +0200
@@ -30,9 +30,10 @@
val quote_string_q: string -> string
val quote_string_qq: string -> string
val quote_string_bq: string -> string
+ val cartouche_content: T list -> T list
val scan_cartouche: string -> T list -> T list * T list
+ val scan_cartouche_content: string -> T list -> T list * T list
val recover_cartouche: T list -> T list * T list
- val cartouche_content: T list -> T list
val scan_comment: string -> T list -> T list * T list
val scan_comment_body: string -> T list -> T list * T list
val recover_comment: T list -> T list * T list
@@ -45,6 +46,8 @@
val explode0: string -> T list
val scan_ident: T list -> T list * T list
val is_identifier: string -> bool
+ val scan_nat: T list -> T list * T list
+ val scan_float: T list -> T list * T list
end;
structure Symbol_Pos: SYMBOL_POS =
@@ -60,7 +63,7 @@
fun range (syms as (_, pos) :: _) =
let val pos' = List.last syms |-> Position.advance
- in Position.range pos pos' end
+ in Position.range (pos, pos') end
| range [] = Position.no_range;
@@ -177,6 +180,20 @@
(* nested text cartouches *)
+fun cartouche_content syms =
+ let
+ fun err () =
+ error ("Malformed text cartouche: "
+ ^ quote (content syms) ^ Position.here (#1 (range syms)));
+ in
+ (case syms of
+ ("\<open>", _) :: rest =>
+ (case rev rest of
+ ("\<close>", _) :: rrest => rev rrest
+ | _ => err ())
+ | _ => err ())
+ end;
+
val scan_cartouche_depth =
Scan.repeat1 (Scan.depend (fn (depth: int option) =>
(case depth of
@@ -193,21 +210,10 @@
!!! (fn () => err_prefix ^ "unclosed text cartouche")
(Scan.provide is_none (SOME 0) scan_cartouche_depth);
-val recover_cartouche = Scan.pass (SOME 0) scan_cartouche_depth;
+fun scan_cartouche_content err_prefix =
+ scan_cartouche err_prefix >> cartouche_content;
-fun cartouche_content syms =
- let
- fun err () =
- error ("Malformed text cartouche: "
- ^ quote (content syms) ^ Position.here (#1 (range syms)));
- in
- (case syms of
- ("\<open>", _) :: rest =>
- (case rev rest of
- ("\<close>", _) :: rrest => rev rrest
- | _ => err ())
- | _ => err ())
- end;
+val recover_cartouche = Scan.pass (SOME 0) scan_cartouche_depth;
(* ML-style comments *)
@@ -269,7 +275,7 @@
let
val (res, _) =
fold (fn s => fn (res, p) => ((s, p) :: res, Position.advance s p))
- (Symbol.explode str) ([], Position.reset_range pos);
+ (Symbol.explode str) ([], Position.no_range_position pos);
in fold (fn (s, p) => if s = Symbol.DEL then I else cons (s, p)) res [] end;
fun explode0 str = explode (str, Position.none);
@@ -296,6 +302,12 @@
SOME (_, []) => true
| _ => false);
+
+(* numerals *)
+
+val scan_nat = Scan.many1 (Symbol.is_digit o symbol);
+val scan_float = scan_nat @@@ $$$ "." @@@ scan_nat;
+
end;
structure Basic_Symbol_Pos = (*not open by default*)
--- a/src/Pure/Isar/attrib.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/Isar/attrib.ML Fri Apr 01 22:33:31 2016 +0200
@@ -153,9 +153,7 @@
let
val _ =
if Token.checked_src src then ()
- else
- Context_Position.report ctxt
- (Position.set_range (Token.range_of src)) Markup.language_attribute;
+ else Context_Position.report ctxt (#1 (Token.range_of src)) Markup.language_attribute;
in #1 (Token.check_src ctxt get_attributes src) end;
val attribs =
--- a/src/Pure/Isar/method.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/Isar/method.ML Fri Apr 01 22:33:31 2016 +0200
@@ -621,7 +621,7 @@
Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd;
val modifier_report =
- (Position.set_range (Token.range_of modifier_toks),
+ (#1 (Token.range_of modifier_toks),
Markup.properties (Position.def_properties_of pos)
(Markup.entity Markup.method_modifierN ""));
val _ =
@@ -747,7 +747,7 @@
if detect_closure_state st then NONE
else
SOME (fn () => ("Excessive case name(s): " ^ commas_quote (map Token.content_of bad) ^
- Position.here (Position.set_range (Token.range_of bad)))))
+ Position.here (#1 (Token.range_of bad)))))
|> (fn SOME msg => Seq.single (Seq.Error msg)
| NONE => goal_cases_tac (map Token.content_of names) (ctxt, st)))))
"bind cases for goals" #>
--- a/src/Pure/Isar/token.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/Isar/token.ML Fri Apr 01 22:33:31 2016 +0200
@@ -183,13 +183,9 @@
fun pos_of (Token ((_, (pos, _)), _, _)) = pos;
fun end_pos_of (Token ((_, (_, pos)), _, _)) = pos;
-fun reset_pos pos (Token ((x, _), y, z)) =
- let val pos' = Position.reset_range pos
- in Token ((x, (pos', pos')), y, z) end;
-
fun range_of (toks as tok :: _) =
let val pos' = end_pos_of (List.last toks)
- in Position.range (pos_of tok) pos' end
+ in Position.range (pos_of tok, pos') end
| range_of [] = Position.no_range;
@@ -620,8 +616,8 @@
Lexicon.scan_var >> pair Var ||
Lexicon.scan_tid >> pair Type_Ident ||
Lexicon.scan_tvar >> pair Type_Var ||
- Lexicon.scan_float >> pair Float ||
- Lexicon.scan_nat >> pair Nat ||
+ Symbol_Pos.scan_float >> pair Float ||
+ Symbol_Pos.scan_nat >> pair Nat ||
scan_symid >> pair Sym_Ident) >> uncurry token));
fun recover msg =
@@ -666,7 +662,7 @@
fun make ((k, n), s) pos =
let
val pos' = Position.advance_offset n pos;
- val range = Position.range pos pos';
+ val range = Position.range (pos, pos');
val tok =
if 0 <= k andalso k < Vector.length immediate_kinds then
Token ((s, range), (Vector.sub (immediate_kinds, k), s), Slot)
@@ -677,8 +673,10 @@
in (tok, pos') end;
fun make_string (s, pos) =
- #1 (make ((~1, 0), Symbol_Pos.quote_string_qq s) Position.none)
- |> reset_pos pos;
+ let
+ val Token ((x, _), y, z) = #1 (make ((~1, 0), Symbol_Pos.quote_string_qq s) Position.none);
+ val pos' = Position.no_range_position pos;
+ in Token ((x, (pos', pos')), y, z) end;
fun make_src a args = make_string a :: args;
--- a/src/Pure/ML/ml_compiler.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/ML/ml_compiler.ML Fri Apr 01 22:33:31 2016 +0200
@@ -38,7 +38,7 @@
(* parse trees *)
fun breakpoint_position loc =
- let val pos = Position.reset_range (Exn_Properties.position_of_location loc) in
+ let val pos = Position.no_range_position (Exn_Properties.position_of_location loc) in
(case Position.offset_of pos of
NONE => pos
| SOME 1 => pos
--- a/src/Pure/ML/ml_lex.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/ML/ml_lex.ML Fri Apr 01 22:33:31 2016 +0200
@@ -312,7 +312,7 @@
let
val pos1 = List.last syms |-> Position.advance;
val pos2 = Position.advance Symbol.space pos1;
- in [Antiquote.Text (Token (Position.range pos1 pos2, (Space, Symbol.space)))] end;
+ in [Antiquote.Text (Token (Position.range (pos1, pos2), (Space, Symbol.space)))] end;
val scan = if SML then scan_sml else scan_ml_antiq;
fun check (Antiquote.Text tok) = (check_content_of tok; if SML then () else warn tok)
--- a/src/Pure/ML/ml_pretty.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/ML/ml_pretty.ML Fri Apr 01 22:33:31 2016 +0200
@@ -13,8 +13,10 @@
val block: pretty list -> pretty
val str: string -> pretty
val brk: FixedInt.int -> pretty
- val pair: ('a * int -> pretty) -> ('b * int -> pretty) -> ('a * 'b) * int -> pretty
- val enum: string -> string -> string -> ('a * int -> pretty) -> 'a list * int -> pretty
+ val pair: ('a * FixedInt.int -> pretty) -> ('b * FixedInt.int -> pretty) ->
+ ('a * 'b) * FixedInt.int -> pretty
+ val enum: string -> string -> string -> ('a * FixedInt.int -> pretty) ->
+ 'a list * FixedInt.int -> pretty
val to_polyml: pretty -> PolyML.pretty
val from_polyml: PolyML.pretty -> pretty
val get_print_depth: unit -> int
--- a/src/Pure/PIDE/markup.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/PIDE/markup.ML Fri Apr 01 22:33:31 2016 +0200
@@ -8,6 +8,7 @@
sig
val parse_bool: string -> bool
val print_bool: bool -> string
+ val parse_nat: string -> int
val parse_int: string -> int
val print_int: int -> string
val parse_real: string -> real
@@ -60,11 +61,15 @@
val position_properties': string list
val position_properties: string list
val positionN: string val position: T
- val expressionN: string val expression: T
+ val expressionN: string val expression: string -> T
val citationN: string val citation: string -> T
val pathN: string val path: string -> T
val urlN: string val url: string -> T
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
val blockN: string val block: bool -> int -> T
@@ -226,23 +231,32 @@
fun parse_bool "true" = true
| parse_bool "false" = false
- | parse_bool s = raise Fail ("Bad boolean: " ^ quote s);
+ | parse_bool s = raise Fail ("Bad boolean " ^ quote s);
val print_bool = Bool.toString;
+
+fun parse_nat s =
+ let val i = Int.fromString s in
+ if is_none i orelse the i < 0
+ then raise Fail ("Bad natural number " ^ quote s)
+ else the i
+ end;
+
fun parse_int s =
let val i = Int.fromString s in
if is_none i orelse String.isPrefix "~" s
- then raise Fail ("Bad integer: " ^ quote s)
+ then raise Fail ("Bad integer " ^ quote s)
else the i
end;
val print_int = signed_string_of_int;
+
fun parse_real s =
(case Real.fromString s of
SOME x => x
- | NONE => raise Fail ("Bad real: " ^ quote s));
+ | NONE => raise Fail ("Bad real " ^ quote s));
fun print_real x =
let val s = signed_string_of_real x in
@@ -365,7 +379,8 @@
(* expression *)
-val (expressionN, expression) = markup_elem "expression";
+val expressionN = "expression";
+fun expression kind = (expressionN, if kind = "" then [] else [(kindN, kind)]);
(* citation *)
@@ -382,8 +397,13 @@
(* pretty printing *)
+val markupN = "markup";
val consistentN = "consistent";
+val unbreakableN = "unbreakable";
val indentN = "indent";
+
+val block_properties = [markupN, consistentN, unbreakableN, indentN];
+
val widthN = "width";
val blockN = "block";
--- a/src/Pure/PIDE/markup.scala Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/PIDE/markup.scala Fri Apr 01 22:33:31 2016 +0200
@@ -131,6 +131,15 @@
/* expression */
val EXPRESSION = "expression"
+ object Expression
+ {
+ def unapply(markup: Markup): Option[String] =
+ markup match {
+ case Markup(EXPRESSION, Kind(kind)) => Some(kind)
+ case Markup(EXPRESSION, _) => Some("")
+ case _ => None
+ }
+ }
/* citation */
--- a/src/Pure/Syntax/lexicon.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/Syntax/lexicon.ML Fri Apr 01 22:33:31 2016 +0200
@@ -15,8 +15,6 @@
val scan_id: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
val scan_longid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
val scan_tid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
- val scan_nat: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
- val scan_float: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
val scan_hex: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
val scan_bin: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
val scan_var: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
@@ -96,13 +94,11 @@
val scan_longid = scan_id @@@ Scan.repeats1 ($$$ "." @@@ scan_id);
val scan_tid = $$$ "'" @@@ scan_id;
-val scan_nat = Scan.many1 (Symbol.is_digit o Symbol_Pos.symbol);
-val scan_float = scan_nat @@@ $$$ "." @@@ scan_nat;
val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol);
val scan_bin = $$$ "0" @@@ $$$ "b" @@@ Scan.many1 (fn (s, _) => s = "0" orelse s = "1");
-val scan_num = scan_hex || scan_bin || scan_nat;
+val scan_num = scan_hex || scan_bin || Symbol_Pos.scan_nat;
-val scan_id_nat = scan_id @@@ Scan.optional ($$$ "." @@@ scan_nat) [];
+val scan_id_nat = scan_id @@@ Scan.optional ($$$ "." @@@ Symbol_Pos.scan_nat) [];
val scan_var = $$$ "?" @@@ scan_id_nat;
val scan_tvar = $$$ "?" @@@ $$$ "'" @@@ scan_id_nat;
@@ -264,7 +260,7 @@
scan_tvar >> token TVarSy ||
scan_var >> token VarSy ||
scan_tid >> token TFreeSy ||
- scan_float >> token FloatSy ||
+ Symbol_Pos.scan_float >> token FloatSy ||
scan_num >> token NumSy ||
scan_longid >> token LongIdentSy ||
scan_xid >> token IdentSy;
@@ -310,7 +306,7 @@
val scan =
(scan_id >> map Symbol_Pos.symbol) --
- Scan.optional ($$ "." |-- scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1;
+ Scan.optional ($$ "." |-- Symbol_Pos.scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1;
in
scan >>
(fn (cs, ~1) => chop_idx (rev cs) []
@@ -357,7 +353,7 @@
fun nat cs =
Option.map (#1 o Library.read_int o map Symbol_Pos.symbol)
- (Scan.read Symbol_Pos.stopper scan_nat cs);
+ (Scan.read Symbol_Pos.stopper Symbol_Pos.scan_nat cs);
in
--- a/src/Pure/Syntax/mixfix.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/Syntax/mixfix.ML Fri Apr 01 22:33:31 2016 +0200
@@ -71,7 +71,7 @@
| range_of (Binder (_, _, _, range)) = range
| range_of (Structure range) = range;
-val pos_of = Position.set_range o range_of;
+val pos_of = Position.range_position o range_of;
fun reset_pos NoSyn = NoSyn
| reset_pos (Mixfix (sy, ps, p, _)) = Mixfix (Input.reset_pos sy, ps, p, Position.no_range)
@@ -125,18 +125,20 @@
fun syn_ext_types type_decls =
let
- fun mk_infix sy ty t p1 p2 p3 range =
+ fun mk_infix sy ty t p1 p2 p3 pos =
Syntax_Ext.Mfix
(Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)",
- ty, t, [p1, p2], p3, Position.set_range range);
+ ty, t, [p1, p2], p3, pos);
- fun mfix_of (_, _, NoSyn) = NONE
- | mfix_of (t, ty, Mixfix (sy, ps, p, range)) =
- SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, ps, p, Position.set_range range))
- | mfix_of (t, ty, Infix (sy, p, range)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p range)
- | mfix_of (t, ty, Infixl (sy, p, range)) = SOME (mk_infix sy ty t p (p + 1) p range)
- | mfix_of (t, ty, Infixr (sy, p, range)) = SOME (mk_infix sy ty t (p + 1) p p range)
- | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t);
+ fun mfix_of (mfix as (_, _, mx)) =
+ (case mfix of
+ (_, _, NoSyn) => NONE
+ | (t, ty, Mixfix (sy, ps, p, _)) =>
+ SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, ps, p, pos_of mx))
+ | (t, ty, Infix (sy, p, _)) => SOME (mk_infix sy ty t (p + 1) (p + 1) p (pos_of mx))
+ | (t, ty, Infixl (sy, p, _)) => SOME (mk_infix sy ty t p (p + 1) p (pos_of mx))
+ | (t, ty, Infixr (sy, p, _)) => SOME (mk_infix sy ty t (p + 1) p p (pos_of mx))
+ | (t, _, _) => error ("Bad mixfix declaration for " ^ quote t ^ Position.here (pos_of mx)));
fun check_args (_, ty, mx) (SOME (Syntax_Ext.Mfix (sy, _, _, _, _, _))) =
if length (Term.binder_types ty) = Syntax_Ext.mfix_args sy then ()
@@ -158,30 +160,32 @@
fun syn_ext_consts logical_types const_decls =
let
- fun mk_infix sy ty c p1 p2 p3 range =
+ fun mk_infix sy ty c p1 p2 p3 pos =
[Syntax_Ext.Mfix
(Symbol_Pos.explode0 "op " @ Input.source_explode (Input.reset_pos sy),
ty, c, [], 1000, Position.none),
Syntax_Ext.Mfix
(Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)",
- ty, c, [p1, p2], p3, Position.set_range range)];
+ ty, c, [p1, p2], p3, pos)];
fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
[Type ("idts", []), ty2] ---> ty3
| binder_typ c _ = error ("Bad type of binder: " ^ quote c);
- fun mfix_of (_, _, NoSyn) = []
- | mfix_of (c, ty, Mixfix (sy, ps, p, range)) =
- [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, ps, p, Position.set_range range)]
- | mfix_of (c, ty, Infix (sy, p, range)) = mk_infix sy ty c (p + 1) (p + 1) p range
- | mfix_of (c, ty, Infixl (sy, p, range)) = mk_infix sy ty c p (p + 1) p range
- | mfix_of (c, ty, Infixr (sy, p, range)) = mk_infix sy ty c (p + 1) p p range
- | mfix_of (c, ty, Binder (sy, p, q, range)) =
+ fun mfix_of (mfix as (_, _, mx)) =
+ (case mfix of
+ (_, _, NoSyn) => []
+ | (c, ty, Mixfix (sy, ps, p, _)) =>
+ [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, ps, p, pos_of mx)]
+ | (c, ty, Infix (sy, p, _)) => mk_infix sy ty c (p + 1) (p + 1) p (pos_of mx)
+ | (c, ty, Infixl (sy, p, _)) => mk_infix sy ty c p (p + 1) p (pos_of mx)
+ | (c, ty, Infixr (sy, p, _)) => mk_infix sy ty c (p + 1) p p (pos_of mx)
+ | (c, ty, Binder (sy, p, q, _)) =>
[Syntax_Ext.Mfix
(Symbol_Pos.explode0 "(3" @ Input.source_explode sy @ Symbol_Pos.explode0 "_./ _)",
- binder_typ c ty, (binder_name c), [0, p], q, Position.set_range range)]
- | mfix_of (c, _, mx) =
- error ("Bad mixfix declaration for " ^ quote c ^ Position.here (pos_of mx));
+ binder_typ c ty, (binder_name c), [0, p], q, pos_of mx)]
+ | (c, _, mx) =>
+ error ("Bad mixfix declaration for " ^ quote c ^ Position.here (pos_of mx)));
fun binder (c, _, Binder _) = SOME (binder_name c, c)
| binder _ = NONE;
--- a/src/Pure/Syntax/printer.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/Syntax/printer.ML Fri Apr 01 22:33:31 2016 +0200
@@ -86,7 +86,7 @@
TypArg of int |
String of bool * string |
Break of int |
- Block of int * symb list;
+ Block of Syntax_Ext.block_info * symb list;
type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;
@@ -110,12 +110,12 @@
apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
| xsyms_to_syms (Syntax_Ext.Space s :: xsyms) =
apfst (cons (String (false, s))) (xsyms_to_syms xsyms)
- | xsyms_to_syms (Syntax_Ext.Bg i :: xsyms) =
+ | xsyms_to_syms (Syntax_Ext.Bg info :: xsyms) =
let
val (bsyms, xsyms') = xsyms_to_syms xsyms;
val (syms, xsyms'') = xsyms_to_syms xsyms';
in
- (Block (i, bsyms) :: syms, xsyms'')
+ (Block (info, bsyms) :: syms, xsyms'')
end
| xsyms_to_syms (Syntax_Ext.Brk i :: xsyms) =
apfst (cons (Break i)) (xsyms_to_syms xsyms)
@@ -202,13 +202,13 @@
then Pretty.marks_str (m @ [Lexicon.literal_markup s], s)
else Pretty.str s;
in (T :: Ts, args') end
- | synT m (Block (i, 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 =
- if i < 0 then Pretty.unbreakable (Pretty.block bTs)
- else Pretty.blk (i, bTs);
+ 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
@@ -217,8 +217,8 @@
in (T :: Ts, args') end
and parT m (pr, args, p, p': int) = #1 (synT m
- (if p > p' orelse (show_brackets andalso p' <> 1000 andalso not (is_chain pr))
- then [Block (1, String (false, "(") :: pr @ [String (false, ")")])]
+ (if p > p' orelse (show_brackets andalso p' <> 1000 andalso not (is_chain pr)) then
+ [Block (Syntax_Ext.block_indent 1, String (false, "(") :: pr @ [String (false, ")")])]
else pr, args))
and atomT a = Pretty.marks_str (markup_extern a)
--- a/src/Pure/Syntax/syntax_ext.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML Fri Apr 01 22:33:31 2016 +0200
@@ -8,11 +8,15 @@
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, unbreakable: bool, indent: int}
+ val block_indent: int -> block_info
datatype xsymb =
Delim of string |
Argument of string * int |
Space of string |
- Bg of int | Brk of int | En
+ Bg of block_info |
+ Brk of int |
+ En
datatype xprod = XProd of string * xsymb list * string * int
val chain_pri: int
val delims_of: xprod list -> string list list
@@ -62,11 +66,18 @@
Space s: some white space for printing
Bg, Brk, En: blocks and breaks for pretty printing*)
+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 |
Argument of string * int |
Space of string |
- Bg of int | Brk of int | En;
+ Bg of block_info |
+ Brk of int |
+ En;
fun is_delim (Delim _) = true
| is_delim _ = false;
@@ -99,14 +110,6 @@
fold (fn Delim s => insert (op =) s | _ => I) xsymbs) xprods []
|> map Symbol.explode;
-fun reports_of (xsym, pos: Position.T) =
- (case xsym of
- Delim _ => [(pos, Markup.literal)]
- | Bg _ => [(pos, Markup.keyword3)]
- | Brk _ => [(pos, Markup.keyword3)]
- | En => [(pos, Markup.keyword3)]
- | _ => []);
-
(** datatype mfix **)
@@ -134,39 +137,139 @@
val typ_to_nonterm1 = typ_to_nt "logic";
+(* properties *)
+
+local
+
+open Basic_Symbol_Pos;
+
+val err_prefix = "Error in mixfix block properties: ";
+val !!! = Symbol_Pos.!!! (fn () => err_prefix ^ "atom expected (identifier, numeral, cartouche)");
+
+val scan_atom =
+ Symbol_Pos.scan_ident ||
+ ($$$ "-" @@@ (Symbol_Pos.scan_float || Symbol_Pos.scan_nat)) ||
+ Symbol_Pos.scan_float || Symbol_Pos.scan_nat ||
+ Symbol_Pos.scan_cartouche_content err_prefix;
+
+val scan_blanks = Scan.many (Symbol.is_blank o Symbol_Pos.symbol);
+val scan_item =
+ scan_blanks |-- scan_atom --| scan_blanks
+ >> (fn ss => (Symbol_Pos.content ss, #1 (Symbol_Pos.range ss)));
+
+val scan_prop =
+ scan_item -- Scan.optional ($$ "=" |-- !!! scan_item >> #1) "true"
+ >> (fn ((x, pos), y) => (x, (y, pos)));
+
+fun get_property default parse name props =
+ (case AList.lookup (op =) props name of
+ NONE => default
+ | SOME (s, pos) =>
+ (parse s handle Fail msg => error (msg ^ " for property " ^ quote name ^ Position.here pos)));
+
+in
+
+fun read_properties ss =
+ let
+ val props =
+ (case Scan.error (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_prop)) ss of
+ (props, []) => props
+ | (_, (_, pos) :: _) => error (err_prefix ^ "bad input" ^ Position.here pos));
+ val _ =
+ (case AList.group (op =) props |> filter (fn (_, [_]) => false | _ => true) of
+ [] => ()
+ | dups => error ("Duplicate properties: " ^ commas_quote (map #1 dups) ^
+ Position.here_list (map #2 (maps #2 dups))));
+ in props end;
+
+val get_string = get_property "" I;
+val get_bool = get_property false Markup.parse_bool;
+val get_nat = get_property 0 Markup.parse_nat;
+
+end;
+
+
(* read mixfix annotations *)
local
open Basic_Symbol_Pos;
+val err_prefix = "Error in mixfix annotation: ";
+
fun scan_one pred = Scan.one (pred o Symbol_Pos.symbol);
fun scan_many pred = Scan.many (pred o Symbol_Pos.symbol);
fun scan_many1 pred = Scan.many1 (pred o Symbol_Pos.symbol);
-val is_meta = member (op =) ["(", ")", "/", "_", "\<index>"];
+fun reports_of_block pos =
+ [(pos, Markup.expression "mixfix block begin"), (pos, Markup.keyword3)];
+
+fun reports_of (xsym, pos) =
+ (case xsym of
+ Delim _ => [(pos, Markup.expression "mixfix delimiter"), (pos, Markup.literal)]
+ | Argument _ => [(pos, Markup.expression "mixfix argument")]
+ | Space _ => [(pos, Markup.expression "mixfix space")]
+ | Bg _ => reports_of_block pos
+ | Brk _ => [(pos, Markup.expression "mixfix break"), (pos, Markup.keyword3)]
+ | En => [(pos, Markup.expression "mixfix block end"), (pos, Markup.keyword3)]);
+
+fun reports_text_of (xsym, pos) =
+ (case xsym of
+ Delim s =>
+ if Position.is_reported pos andalso exists Symbol.is_utf8 (Symbol.explode s) then
+ [((pos, Markup.bad),
+ "Mixfix delimiter contains raw Unicode -- this is non-portable and unreliable")]
+ else []
+ | _ => []);
+
+fun read_block_properties ss =
+ let
+ val props = read_properties ss;
+
+ val markup_name = get_string Markup.markupN props;
+ val markup_props = fold (AList.delete (op =)) Markup.block_properties props;
+ val markup = (markup_name, map (apsnd #1) markup_props);
+ val _ =
+ if markup_name = "" andalso not (null markup_props) then
+ error ("Markup name required for block properties: " ^
+ commas_quote (map #1 markup_props) ^ Position.here_list (map (#2 o #2) markup_props))
+ 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, unbreakable = unbreakable, indent = indent} end
+ handle ERROR msg =>
+ let
+ val reported_texts =
+ reports_of_block (#1 (Symbol_Pos.range ss))
+ |> map (fn (p, m) => Markup.markup_report (Position.reported_text p m ""))
+ in error (msg ^ implode reported_texts) end;
+
+val read_block_indent =
+ Bg o block_indent o #1 o Library.read_int o map Symbol_Pos.symbol;
+
+val is_meta = member (op =) ["(", ")", "/", "_", "\<index>", Symbol.open_, Symbol.close];
val scan_delim_char =
$$ "'" |-- scan_one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
scan_one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof);
-fun read_int ["0", "0"] = ~1
- | read_int cs = #1 (Library.read_int cs);
-
val scan_sym =
$$ "_" >> K (Argument ("", 0)) ||
$$ "\<index>" >> K index ||
- $$ "(" |-- scan_many Symbol.is_digit >> (Bg o read_int o map Symbol_Pos.symbol) ||
+ $$ "(" |--
+ (Symbol_Pos.scan_cartouche_content err_prefix >> read_block_properties ||
+ scan_many Symbol.is_digit >> read_block_indent) ||
$$ ")" >> K En ||
$$ "/" -- $$ "/" >> K (Brk ~1) ||
- $$ "/" |-- scan_many Symbol.is_blank >> (Brk o length) ||
- scan_many1 Symbol.is_blank >> (Space o Symbol_Pos.content) ||
+ $$ "/" |-- scan_many Symbol.is_space >> (Brk o length) ||
+ scan_many1 Symbol.is_space >> (Space o Symbol_Pos.content) ||
Scan.repeat1 scan_delim_char >> (Delim o Symbol_Pos.content);
val scan_symb =
- Scan.trace scan_sym >>
- (fn (syms, trace) => SOME (syms, Position.set_range (Symbol_Pos.range trace))) ||
- $$ "'" -- scan_one Symbol.is_blank >> K NONE;
+ Scan.trace scan_sym >> (fn (syms, trace) => SOME (syms, #1 (Symbol_Pos.range trace))) ||
+ $$ "'" -- scan_one Symbol.is_space >> K NONE;
val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (~$$ "'");
@@ -174,8 +277,12 @@
fun read_mfix ss =
let
- val xsymbs = map_filter I (the (Scan.read Symbol_Pos.stopper scan_symbs ss));
+ val xsymbs =
+ (case Scan.error (Scan.finite Symbol_Pos.stopper scan_symbs) ss of
+ (res, []) => map_filter I res
+ | (_, (_, pos) :: _) => error (err_prefix ^ "bad input" ^ Position.here pos));
val _ = Position.reports (maps reports_of xsymbs);
+ val _ = Position.reports_text (maps reports_text_of xsymbs);
in xsymbs end;
val mfix_args = length o filter (is_argument o #1) o read_mfix o map (apsnd (K Position.none));
--- a/src/Pure/Syntax/syntax_phases.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Fri Apr 01 22:33:31 2016 +0200
@@ -338,7 +338,7 @@
if len <= 1 then []
else
[cat_lines
- (("Ambiguous input" ^ Position.here (Position.reset_range pos) ^
+ (("Ambiguous input" ^ Position.here (Position.no_range_position pos) ^
" produces " ^ string_of_int len ^ " parse trees" ^
(if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
map (Pretty.string_of o Pretty.item o single o Parser.pretty_parsetree)
@@ -750,7 +750,8 @@
let
val ((bg1, bg2), en) = typing_elem;
val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty ty) ^ bg2;
- in SOME (Pretty.make_block (bg, en) false 0 [pretty_ast Markup.empty t]) end
+ val info = {markup = (bg, en), consistent = false, indent = 0};
+ in SOME (Pretty.make_block info [pretty_ast Markup.empty t]) end
else NONE
and ofsort_trans ty s =
@@ -758,7 +759,8 @@
let
val ((bg1, bg2), en) = sorting_elem;
val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty s) ^ bg2;
- in SOME (Pretty.make_block (bg, en) false 0 [pretty_typ_ast Markup.empty ty]) end
+ val info = {markup = (bg, en), consistent = false, indent = 0};
+ in SOME (Pretty.make_block info [pretty_typ_ast Markup.empty ty]) end
else NONE
and pretty_typ_ast m ast = ast
--- a/src/Pure/System/options.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/System/options.ML Fri Apr 01 22:33:31 2016 +0200
@@ -19,6 +19,7 @@
val bool: T -> string -> bool
val int: T -> string -> int
val real: T -> string -> real
+ val seconds: T -> string -> Time.time
val string: T -> string -> string
val put_bool: string -> bool -> T -> T
val put_int: string -> int -> T -> T
@@ -33,6 +34,7 @@
val default_bool: string -> bool
val default_int: string -> int
val default_real: string -> real
+ val default_seconds: string -> Time.time
val default_string: string -> string
val default_put_bool: string -> bool -> unit
val default_put_int: string -> int -> unit
@@ -115,6 +117,7 @@
val bool = get boolT (try Markup.parse_bool);
val int = get intT (try Markup.parse_int);
val real = get realT (try Markup.parse_real);
+val seconds = Time.fromReal oo real;
val string = get stringT SOME;
val put_bool = put boolT Markup.print_bool;
@@ -191,6 +194,7 @@
fun default_bool name = bool (default ()) name;
fun default_int name = int (default ()) name;
fun default_real name = real (default ()) name;
+fun default_seconds name = seconds (default ()) name;
fun default_string name = string (default ()) name;
val default_put_bool = change_default put_bool;
--- a/src/Pure/Thy/document_antiquotations.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML Fri Apr 01 22:33:31 2016 +0200
@@ -15,7 +15,7 @@
Thy_Output.antiquotation binding (Scan.succeed ())
(fn {source, ...} => fn _ =>
error ("Bad Markdown structure: illegal " ^ quote (Binding.name_of binding) ^
- Position.here (Position.reset_range (#1 (Token.range_of source)))))
+ Position.here (Position.no_range_position (#1 (Token.range_of source)))))
in
--- a/src/Pure/Thy/markdown.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/Thy/markdown.ML Fri Apr 01 22:33:31 2016 +0200
@@ -86,7 +86,7 @@
| (c, pos) :: _ =>
error ("Bad blank character " ^ quote (ML_Syntax.print_char c) ^ Position.here pos));
-fun is_space ((s, _): Symbol_Pos.T) = s = Symbol.space;
+val is_space = Symbol.is_space o Symbol_Pos.symbol;
val is_empty = forall (fn Antiquote.Text ss => forall is_space ss | _ => false);
fun strip_spaces (Antiquote.Text ss :: rest) =
--- a/src/Pure/Tools/build.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/Tools/build.ML Fri Apr 01 22:33:31 2016 +0200
@@ -81,8 +81,11 @@
val name = the_default "" (Properties.get args Markup.nameN);
val pos = Position.of_properties args;
val {elapsed, ...} = Markup.parse_timing_properties args;
+ val is_significant =
+ Timing.is_relevant_time elapsed andalso
+ Time.>= (elapsed, Options.default_seconds "command_timing_threshold");
in
- if Timing.is_relevant_time elapsed then
+ if is_significant then
(case approximative_id name pos of
SOME id => inline_message (#2 function) (Markup.command_timing_properties id elapsed)
| NONE => ())
--- a/src/Pure/Tools/rail.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/Tools/rail.ML Fri Apr 01 22:33:31 2016 +0200
@@ -53,7 +53,7 @@
fun range_of (toks as tok :: _) =
let val pos' = end_pos_of (List.last toks)
- in Position.range (pos_of tok) pos' end
+ in Position.range (pos_of tok, pos') end
| range_of [] = Position.no_range;
fun kind_of (Token (_, (k, _))) = k;
@@ -116,7 +116,7 @@
scan_keyword >> (token Keyword o single) ||
Lexicon.scan_id >> token Ident ||
Symbol_Pos.scan_string_q err_prefix >> (fn (pos1, (ss, pos2)) =>
- [Token (Position.range pos1 pos2, (String, Symbol_Pos.content ss))]);
+ [Token (Position.range (pos1, pos2), (String, Symbol_Pos.content ss))]);
val scan =
Scan.repeats scan_token --|
@@ -188,7 +188,7 @@
let
fun reports r =
if r = Position.no_range then []
- else [(Position.set_range r, Markup.expression)];
+ else [(Position.range_position r, Markup.expression "")];
fun trees (CAT (ts, r)) = reports r @ maps tree ts
and tree (BAR (Ts, r)) = reports r @ maps trees Ts
| tree (STAR ((T1, T2), r)) = reports r @ trees T1 @ trees T2
--- a/src/Pure/pure_thy.ML Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Pure/pure_thy.ML Fri Apr 01 22:33: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),
--- a/src/Tools/jEdit/etc/options Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Tools/jEdit/etc/options Fri Apr 01 22:33:31 2016 +0200
@@ -37,7 +37,7 @@
-- "maximum number of symbols in search result"
public option jedit_timing_threshold : real = 0.1
- -- "default threshold for timing display"
+ -- "default threshold for timing display (seconds)"
section "Completion"
--- a/src/Tools/jEdit/src/rendering.scala Fri Apr 01 15:17:11 2016 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Fri Apr 01 22:33:31 2016 +0200
@@ -172,7 +172,6 @@
private val tooltip_descriptions =
Map(
- Markup.EXPRESSION -> "expression",
Markup.CITATION -> "citation",
Markup.TOKEN_RANGE -> "inner syntax token",
Markup.FREE -> "free variable",
@@ -183,9 +182,9 @@
Markup.TVAR -> "schematic type variable")
private val tooltip_elements =
- Markup.Elements(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
- Markup.TYPING, Markup.ML_TYPING, Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC,
- Markup.URL, Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name) ++
+ Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
+ Markup.SORTING, Markup.TYPING, Markup.ML_TYPING, Markup.ML_BREAKPOINT, Markup.PATH,
+ Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name) ++
Markup.Elements(tooltip_descriptions.keySet)
private val gutter_elements =
@@ -567,10 +566,15 @@
if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
else "breakpoint (disabled)"
Some(add(prev, r, (true, XML.Text(text))))
+
case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
val lang = Word.implode(Word.explode('_', language))
Some(add(prev, r, (true, XML.Text("language: " + lang))))
+ case (prev, Text.Info(r, XML.Elem(Markup.Expression(kind), _))) =>
+ val descr = if (kind == "") "expression" else "expression: " + kind
+ Some(add(prev, r, (true, XML.Text(descr))))
+
case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))
case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) =>