# HG changeset patch # User wenzelm # Date 1459542811 -7200 # Node ID ab870893d7b14d32aee3bb3799fbea6b91d25e94 # Parent 7737e26cd3c6973ce12d160a369bebb0831942ee# Parent 4b8f08de279270c5ee664f1f4a13ef89cde04b37 merged diff -r 7737e26cd3c6 -r ab870893d7b1 NEWS --- 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 +"(\x=a y=b z \\". Notable property names are "indent", "consistent", +"unbreakable", "markup". The existing notation "(DIGITS" is equivalent +to "(\indent=DIGITS\". The former notation "(00" for unbreakable blocks +is superseded by "(\unbreabable\" --- rare INCOMPATIBILITY. + * New symbol \, e.g. for temporal operator. * Old 'header' command is no longer supported (legacy since diff -r 7737e26cd3c6 -r ab870893d7b1 etc/options --- 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" - diff -r 7737e26cd3c6 -r ab870893d7b1 src/Doc/Isar_Ref/Inner_Syntax.thy --- 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} + ',') ']' \} @@ -342,6 +342,7 @@ \<^verbatim>\(\ & open parenthesis \\ \<^verbatim>\)\ & close parenthesis \\ \<^verbatim>\/\ & slash \\ + \\ \\ & cartouche delimiters \\ \end{tabular} \<^medskip> @@ -360,10 +361,13 @@ \<^descr> \s\ is a non-empty sequence of spaces for printing. This and the following specifications do not affect parsing at all. - \<^descr> \<^verbatim>\(\\n\ 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>\(00\ is unbreakable. + \<^descr> \<^verbatim>\(\\n\ 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>\(\\\properties\\ 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>\)\ closes a pretty printing block. @@ -374,8 +378,39 @@ is \<^emph>\not\ 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 \ + @{syntax_def "mixfix_properties"}: (entry *) + ; + entry: atom ('=' atom)? + ; + atom: @{syntax ident} | @{syntax int} | @{syntax float} | @{syntax cartouche} + \} + + Each @{syntax entry} is a name-value pair: if the value is omitted, if + defaults to \<^verbatim>\true\ (intended for Boolean properties). The following + standard block properties are supported: + + \<^item> \indent\ (natural number): the block indentation --- the same as for the + simple syntax without block properties. + + \<^item> \consistent\ (Boolean): this block has consistent breaks (if one break + is taken, all breaks are taken). + + \<^item> \unbreakable\ (Boolean): all possible breaks of the block are disabled + (turned into spaces). + + \<^item> \markup\ (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"}. \ diff -r 7737e26cd3c6 -r ab870893d7b1 src/HOL/Complete_Lattices.thy --- 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 \ 'a set \ 'b set \ 'b set" ("(3INT _:_./ _)" [0, 0, 10] 10) syntax (latex output) - "_INTER1" :: "pttrns \ 'b set \ 'b set" ("(3\(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10) - "_INTER" :: "pttrn \ 'a set \ 'b set \ 'b set" ("(3\(00\<^bsub>_\_\<^esub>)/ _)" [0, 0, 10] 10) + "_INTER1" :: "pttrns \ 'b set \ 'b set" ("(3\(\unbreakable\\<^bsub>_\<^esub>)/ _)" [0, 10] 10) + "_INTER" :: "pttrn \ 'a set \ 'b set \ 'b set" ("(3\(\unbreakable\\<^bsub>_\_\<^esub>)/ _)" [0, 0, 10] 10) syntax "_INTER1" :: "pttrns \ 'b set \ 'b set" ("(3\_./ _)" [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\(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10) - "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\(00\<^bsub>_\_\<^esub>)/ _)" [0, 0, 10] 10) + "_UNION1" :: "pttrns => 'b set => 'b set" ("(3\(\unbreakable\\<^bsub>_\<^esub>)/ _)" [0, 10] 10) + "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\(\unbreakable\\<^bsub>_\_\<^esub>)/ _)" [0, 0, 10] 10) syntax "_UNION1" :: "pttrns => 'b set => 'b set" ("(3\_./ _)" [0, 10] 10) diff -r 7737e26cd3c6 -r ab870893d7b1 src/HOL/Eisbach/method_closure.ML --- 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 diff -r 7737e26cd3c6 -r ab870893d7b1 src/HOL/Set_Interval.thy --- 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 \ 'a => 'b set => 'b set" ("(3\(00_ \ _)/ _)" [0, 0, 10] 10) - "_UNION_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ < _)/ _)" [0, 0, 10] 10) - "_INTER_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ \ _)/ _)" [0, 0, 10] 10) - "_INTER_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(00_ < _)/ _)" [0, 0, 10] 10) + "_UNION_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(\unbreakable\_ \ _)/ _)" [0, 0, 10] 10) + "_UNION_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(\unbreakable\_ < _)/ _)" [0, 0, 10] 10) + "_INTER_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(\unbreakable\_ \ _)/ _)" [0, 0, 10] 10) + "_INTER_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(\unbreakable\_ < _)/ _)" [0, 0, 10] 10) syntax "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\_\_./ _)" [0, 0, 10] 10) diff -r 7737e26cd3c6 -r ab870893d7b1 src/HOL/ex/Hebrew.thy --- 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 \The Hebrew Alef-Bet (א-ב).\ +subsection \Warning: formal Unicode considered harmful\ + +text \ + Important note: editors or browsers that implement the \<^emph>\Unicode + Bidirectional Algorithm\ 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). +\ + +subsection \The Hebrew Alef-Bet (א-ב).\ datatype alef_bet = Alef ("א") @@ -39,9 +52,9 @@ thm alef_bet.induct -text \Interpreting Hebrew letters as numbers.\ +subsection \Interpreting Hebrew letters as numbers.\ -primrec mispar :: "alef_bet => nat" +primrec mispar :: "alef_bet \ nat" where "mispar א = 1" | "mispar ב = 2" diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/General/antiquote.ML --- 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 = diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/General/position.ML --- 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 diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/General/pretty.ML --- 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; diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/General/pretty.scala --- 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))) diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/General/symbol.ML --- 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 = "\"; val space = chr 32; +fun is_space s = s = space; local val small_spaces = Vector.tabulate (65, fn i => replicate_string i space); diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/General/symbol_pos.ML --- 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 + ("\", _) :: rest => + (case rev rest of + ("\", _) :: 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 - ("\", _) :: rest => - (case rev rest of - ("\", _) :: 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*) diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/Isar/attrib.ML --- 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 = diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/Isar/method.ML --- 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" #> diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/Isar/token.ML --- 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; diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/ML/ml_compiler.ML --- 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 diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/ML/ml_lex.ML --- 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) diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/ML/ml_pretty.ML --- 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 diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/PIDE/markup.ML --- 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"; diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/PIDE/markup.scala --- 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 */ diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/Syntax/lexicon.ML --- 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 diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/Syntax/mixfix.ML --- 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; diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/Syntax/printer.ML --- 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) diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/Syntax/syntax_ext.ML --- 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 =) ["(", ")", "/", "_", "\"]; +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 =) ["(", ")", "/", "_", "\", 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)) || $$ "\" >> 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)); diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/Syntax/syntax_phases.ML --- 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 diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/System/options.ML --- 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; diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/Thy/document_antiquotations.ML --- 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 diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/Thy/markdown.ML --- 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) = diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/Tools/build.ML --- 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 => ()) diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/Tools/rail.ML --- 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 diff -r 7737e26cd3c6 -r ab870893d7b1 src/Pure/pure_thy.ML --- 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 "(\unbreakable\\<^bsub>_\<^esub>)"), ("_indexdefault", typ "index", Mixfix.mixfix ""), ("_indexvar", typ "index", Mixfix.mixfix "'\"), ("_struct", typ "index => logic", NoSyn), diff -r 7737e26cd3c6 -r ab870893d7b1 src/Tools/jEdit/etc/options --- 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" diff -r 7737e26cd3c6 -r ab870893d7b1 src/Tools/jEdit/src/rendering.scala --- 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), _))) =>