--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Mar 29 21:25:19 2016 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Mar 29 23:45:28 2016 +0200
@@ -87,29 +87,31 @@
type atom_pool = ((string * int) * int list) list
+fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range)
+
fun add_wacky_syntax ctxt =
let
val name_of = fst o dest_Const
val thy = Proof_Context.theory_of ctxt
val (unrep_s, thy) = thy
|> Sign.declare_const_global ((@{binding nitpick_unrep}, @{typ 'a}),
- Mixfix (unrep_mixfix (), [], 1000))
+ mixfix (unrep_mixfix (), [], 1000))
|>> name_of
val (maybe_s, thy) = thy
|> Sign.declare_const_global ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
- Mixfix (maybe_mixfix (), [1000], 1000))
+ mixfix (maybe_mixfix (), [1000], 1000))
|>> name_of
val (abs_s, thy) = thy
|> Sign.declare_const_global ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
- Mixfix (abs_mixfix (), [40], 40))
+ mixfix (abs_mixfix (), [40], 40))
|>> name_of
val (base_s, thy) = thy
|> Sign.declare_const_global ((@{binding nitpick_base}, @{typ "'a => 'a"}),
- Mixfix (base_mixfix (), [1000], 1000))
+ mixfix (base_mixfix (), [1000], 1000))
|>> name_of
val (step_s, thy) = thy
|> Sign.declare_const_global ((@{binding nitpick_step}, @{typ "'a => 'a"}),
- Mixfix (step_mixfix (), [1000], 1000))
+ mixfix (step_mixfix (), [1000], 1000))
|>> name_of
in
(((unrep_s, maybe_s, abs_s), (base_s, step_s)),
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Mar 29 21:25:19 2016 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Mar 29 23:45:28 2016 +0200
@@ -1959,8 +1959,8 @@
val ((T, ts), statistics) = eval ctxt stats param_user_modes comp_options k t_compr
val setT = HOLogic.mk_setT T
val elems = HOLogic.mk_set T ts
- val ([dots], ctxt') =
- Proof_Context.add_fixes [(@{binding dots}, SOME setT, Mixfix ("...", [], 1000))] ctxt
+ val ([dots], ctxt') = ctxt
+ |> Proof_Context.add_fixes [(@{binding dots}, SOME setT, Delimfix (\<open>...\<close>, Position.no_range))]
(* check expected values *)
val union = Const (@{const_abbrev Set.union}, setT --> setT --> setT)
val () =
--- a/src/Pure/General/antiquote.ML Tue Mar 29 21:25:19 2016 +0200
+++ b/src/Pure/General/antiquote.ML Tue Mar 29 23:45:28 2016 +0200
@@ -16,7 +16,7 @@
val scan_control: Symbol_Pos.T list -> control * Symbol_Pos.T list
val scan_antiq: Symbol_Pos.T list -> antiq * Symbol_Pos.T list
val scan_antiquote: Symbol_Pos.T list -> text_antiquote * Symbol_Pos.T list
- val read': Position.T -> Symbol_Pos.T list -> text_antiquote list
+ val parse: Position.T -> Symbol_Pos.T list -> text_antiquote list
val read: Input.source -> text_antiquote list
end;
@@ -123,11 +123,15 @@
(* read *)
-fun read' pos syms =
+fun parse pos syms =
(case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
- SOME ants => (Position.reports (antiq_reports ants); ants)
+ SOME ants => ants
| NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos));
-fun read source = read' (Input.pos_of source) (Input.source_explode source);
+fun read source =
+ let
+ val ants = parse (Input.pos_of source) (Input.source_explode source);
+ val _ = Position.reports (antiq_reports ants);
+ in ants end;
end;
--- a/src/Pure/General/input.ML Tue Mar 29 21:25:19 2016 +0200
+++ b/src/Pure/General/input.ML Tue Mar 29 23:45:28 2016 +0200
@@ -15,6 +15,7 @@
val string: string -> source
val source_explode: source -> Symbol_Pos.T list
val source_content: source -> string
+ val equal_content: source * source -> bool
end;
structure Input: INPUT =
@@ -38,6 +39,8 @@
val source_content = source_explode #> Symbol_Pos.content;
+val equal_content = (op =) o apply2 source_content;
+
end;
end;
--- a/src/Pure/General/position.ML Tue Mar 29 21:25:19 2016 +0200
+++ b/src/Pure/General/position.ML Tue Mar 29 23:45:28 2016 +0200
@@ -135,7 +135,7 @@
fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
-fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props);
+fun put_id id (Pos (count, props)) = Pos (count, norm_props (Properties.put (Markup.idN, id) props));
fun parse_id pos = Option.map Markup.parse_int (get_id pos);
--- a/src/Pure/General/symbol_pos.ML Tue Mar 29 21:25:19 2016 +0200
+++ b/src/Pure/General/symbol_pos.ML Tue Mar 29 23:45:28 2016 +0200
@@ -42,6 +42,7 @@
val implode: T list -> text
val implode_range: Position.range -> T list -> text * Position.range
val explode: text * Position.T -> T list
+ val explode0: string -> T list
val scan_ident: T list -> T list * T list
val is_identifier: string -> bool
end;
@@ -271,6 +272,8 @@
(Symbol.explode str) ([], Position.reset_range 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);
+
(* identifiers *)
@@ -289,7 +292,7 @@
fun is_identifier s =
Symbol.is_ascii_identifier s orelse
- (case try (Scan.finite stopper scan_ident) (explode (s, Position.none)) of
+ (case try (Scan.finite stopper scan_ident) (explode0 s) of
SOME (_, []) => true
| _ => false);
@@ -302,4 +305,3 @@
val $$$ = Symbol_Pos.$$$;
val ~$$$ = Symbol_Pos.~$$$;
end;
-
--- a/src/Pure/Isar/class.ML Tue Mar 29 21:25:19 2016 +0200
+++ b/src/Pure/Isar/class.ML Tue Mar 29 23:45:28 2016 +0200
@@ -616,8 +616,10 @@
fun foundation (((b, U), mx), (b_def, rhs)) params lthy =
(case instantiation_param lthy b of
SOME c =>
- if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
- else lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs)
+ if Mixfix.is_empty mx then lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs)
+ else
+ error ("Illegal mixfix syntax for overloaded constant " ^ quote c ^
+ Position.here (Mixfix.pos_of mx))
| NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params);
fun pretty lthy =
--- a/src/Pure/Isar/expression.ML Tue Mar 29 21:25:19 2016 +0200
+++ b/src/Pure/Isar/expression.ML Tue Mar 29 23:45:28 2016 +0200
@@ -85,8 +85,11 @@
[] => ()
| dups => error (message ^ commas dups));
- fun parm_eq ((p1: string, mx1: mixfix), (p2, mx2)) = p1 = p2 andalso
- (mx1 = mx2 orelse error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression"));
+ fun parm_eq ((p1, mx1), (p2, mx2)) =
+ p1 = p2 andalso
+ (Mixfix.equal (mx1, mx2) orelse
+ error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression" ^
+ Position.here_list [Mixfix.pos_of mx1, Mixfix.pos_of mx2]));
fun params_loc loc = Locale.params_of thy loc |> map (apfst #1);
fun params_inst (loc, (prfx, Positional insts)) =
--- a/src/Pure/Isar/generic_target.ML Tue Mar 29 21:25:19 2016 +0200
+++ b/src/Pure/Isar/generic_target.ML Tue Mar 29 23:45:28 2016 +0200
@@ -103,14 +103,17 @@
warning
("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^
commas (map (Syntax.string_of_typ ctxt o TFree) (sort_by #1 extra_tfrees)) ^
- (if mx = NoSyn then ""
- else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)))
+ (if Mixfix.is_empty mx then ""
+ else
+ "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx) ^
+ Position.here (Mixfix.pos_of mx)))
else (); NoSyn);
fun check_mixfix_global (b, no_params) mx =
- if no_params orelse mx = NoSyn then mx
- else (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^
- Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn);
+ if no_params orelse Mixfix.is_empty mx then mx
+ else
+ (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^
+ Pretty.string_of (Mixfix.pretty_mixfix mx) ^ Position.here (Mixfix.pos_of mx)); NoSyn);
fun same_const (Const (c, _), Const (c', _)) = c = c'
| same_const (t $ _, t' $ _) = same_const (t, t')
--- a/src/Pure/Isar/overloading.ML Tue Mar 29 21:25:19 2016 +0200
+++ b/src/Pure/Isar/overloading.ML Tue Mar 29 23:45:28 2016 +0200
@@ -158,9 +158,11 @@
fun foundation (((b, U), mx), (b_def, rhs)) params lthy =
(case operation lthy b of
SOME (c, (v, checked)) =>
- if mx <> NoSyn
- then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
- else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs)
+ if Mixfix.is_empty mx then
+ lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs)
+ else
+ error ("Illegal mixfix syntax for overloaded constant " ^ quote c ^
+ Position.here (Mixfix.pos_of mx))
| NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params);
fun pretty lthy =
--- a/src/Pure/Isar/parse.ML Tue Mar 29 21:25:19 2016 +0200
+++ b/src/Pure/Isar/parse.ML Tue Mar 29 23:45:28 2016 +0200
@@ -317,22 +317,33 @@
local
-val mfix = string --
- !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] --
- Scan.optional nat 1000) >> (Mixfix o Scan.triple2);
+val mfix =
+ input string --
+ !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] -- Scan.optional nat 1000)
+ >> (fn (sy, (ps, p)) => Mixfix (sy, ps, p, Position.no_range));
+
+val infx =
+ $$$ "infix" |-- !!! (input string -- nat >> (fn (sy, p) => Infix (sy, p, Position.no_range)));
-val infx = $$$ "infix" |-- !!! (string -- nat >> Infix);
-val infxl = $$$ "infixl" |-- !!! (string -- nat >> Infixl);
-val infxr = $$$ "infixr" |-- !!! (string -- nat >> Infixr);
-val strcture = $$$ "structure" >> K Structure;
+val infxl =
+ $$$ "infixl" |-- !!! (input string -- nat >> (fn (sy, p) => Infixl (sy, p, Position.no_range)));
+
+val infxr =
+ $$$ "infixr" |-- !!! (input string -- nat >> (fn (sy, p) => Infixr (sy, p, Position.no_range)));
-val binder = $$$ "binder" |--
- !!! (string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n))))
- >> (Binder o Scan.triple2);
+val strcture = $$$ "structure" >> K (Structure Position.no_range);
+
+val binder =
+ $$$ "binder" |--
+ !!! (input string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n))))
+ >> (fn (sy, (p, q)) => Binder (sy, p, q, Position.no_range));
val mixfix_body = mfix || strcture || binder || infxl || infxr || infx;
-fun annotation guard body = $$$ "(" |-- guard (body --| $$$ ")");
+fun annotation guard body =
+ Scan.trace ($$$ "(" |-- guard (body --| $$$ ")"))
+ >> (fn (mx, toks) => Mixfix.set_range (Token.range_of toks) mx);
+
fun opt_annotation guard body = Scan.optional (annotation guard body) NoSyn;
in
--- a/src/Pure/Proof/proof_syntax.ML Tue Mar 29 21:25:19 2016 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Tue Mar 29 23:45:28 2016 +0200
@@ -30,6 +30,7 @@
val idtT = Type ("idt", []);
val aT = TFree (Name.aT, []);
+
(** constants for theorems and axioms **)
fun add_proof_atom_consts names thy =
@@ -37,8 +38,12 @@
|> Sign.root_path
|> Sign.add_consts (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names);
+
(** constants for application and abstraction **)
+fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range);
+fun delimfix sy = Delimfix (Input.string sy, Position.no_range);
+
fun add_proof_syntax thy =
thy
|> Sign.root_path
@@ -46,29 +51,29 @@
|> Sign.add_types_global
[(Binding.make ("proof", @{here}), 0, NoSyn)]
|> fold (snd oo Sign.declare_const_global)
- [((Binding.make ("Appt", @{here}), [proofT, aT] ---> proofT), Mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
- ((Binding.make ("AppP", @{here}), [proofT, proofT] ---> proofT), Mixfix ("(1_ \<bullet>/ _)", [4, 5], 4)),
+ [((Binding.make ("Appt", @{here}), [proofT, aT] ---> proofT), mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
+ ((Binding.make ("AppP", @{here}), [proofT, proofT] ---> proofT), mixfix ("(1_ \<bullet>/ _)", [4, 5], 4)),
((Binding.make ("Abst", @{here}), (aT --> proofT) --> proofT), NoSyn),
((Binding.make ("AbsP", @{here}), [propT, proofT --> proofT] ---> proofT), NoSyn),
((Binding.make ("Hyp", @{here}), propT --> proofT), NoSyn),
((Binding.make ("Oracle", @{here}), propT --> proofT), NoSyn),
((Binding.make ("OfClass", @{here}), (Term.a_itselfT --> propT) --> proofT), NoSyn),
- ((Binding.make ("MinProof", @{here}), proofT), Delimfix "?")]
+ ((Binding.make ("MinProof", @{here}), proofT), delimfix "?")]
|> Sign.add_nonterminals_global
[Binding.make ("param", @{here}),
Binding.make ("params", @{here})]
|> Sign.add_syntax Syntax.mode_default
- [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
- ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
- ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
- ("_Lam1", [idtT, propT] ---> paramT, Mixfix ("_: _", [0, 0], 0)),
- ("", paramT --> paramT, Delimfix "'(_')"),
- ("", idtT --> paramsT, Delimfix "_"),
- ("", paramT --> paramsT, Delimfix "_")]
+ [("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
+ ("_Lam0", [paramT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)),
+ ("_Lam0", [idtT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)),
+ ("_Lam1", [idtT, propT] ---> paramT, mixfix ("_: _", [0, 0], 0)),
+ ("", paramT --> paramT, delimfix "'(_')"),
+ ("", idtT --> paramsT, delimfix "_"),
+ ("", paramT --> paramsT, delimfix "_")]
|> Sign.add_syntax (Print_Mode.ASCII, true)
- [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
- (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
- (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4))]
+ [("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1Lam _./ _)", [0, 3], 3)),
+ (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, mixfix ("(1_ %/ _)", [4, 5], 4)),
+ (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ %%/ _)", [4, 5], 4))]
|> Sign.add_trrules (map Syntax.Parse_Print_Rule
[(Ast.mk_appl (Ast.Constant "_Lam")
[Ast.mk_appl (Ast.Constant "_Lam0")
--- a/src/Pure/Syntax/lexicon.ML Tue Mar 29 21:25:19 2016 +0200
+++ b/src/Pure/Syntax/lexicon.ML Tue Mar 29 23:45:28 2016 +0200
@@ -327,7 +327,7 @@
(* indexname *)
fun read_indexname s =
- (case Scan.read Symbol_Pos.stopper scan_indexname (Symbol_Pos.explode (s, Position.none)) of
+ (case Scan.read Symbol_Pos.stopper scan_indexname (Symbol_Pos.explode0 s) of
SOME xi => xi
| _ => error ("Lexical error in variable name: " ^ quote s));
@@ -341,14 +341,14 @@
>> Syntax.var ||
Scan.many (Symbol.not_eof o Symbol_Pos.symbol)
>> (Syntax.free o implode o map Symbol_Pos.symbol);
- in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none))) end;
+ in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode0 str)) end;
(* read_variable *)
fun read_variable str =
let val scan = $$ "?" |-- scan_indexname || scan_indexname
- in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none)) end;
+ in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode0 str) end;
(* read numbers *)
@@ -361,10 +361,10 @@
in
-fun read_nat s = nat (Symbol_Pos.explode (s, Position.none));
+fun read_nat s = nat (Symbol_Pos.explode0 s);
fun read_int s =
- (case Symbol_Pos.explode (s, Position.none) of
+ (case Symbol_Pos.explode0 s of
("-", _) :: cs => Option.map ~ (nat cs)
| cs => nat cs);
--- a/src/Pure/Syntax/local_syntax.ML Tue Mar 29 21:25:19 2016 +0200
+++ b/src/Pure/Syntax/local_syntax.ML Tue Mar 29 23:45:28 2016 +0200
@@ -76,20 +76,21 @@
local
-fun prep_mixfix _ _ (_, (_, _, Structure)) = NONE
+fun prep_mixfix _ _ (_, (_, _, Structure _)) = NONE
| prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl))
| prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl))
| prep_mixfix add mode (Fixed, (x, T, mx)) =
SOME ((x, true), ((false, add, mode), (Lexicon.mark_fixed x, T, mx)));
-fun prep_struct (Fixed, (c, _, Structure)) = SOME c
- | prep_struct (_, (c, _, Structure)) = error ("Bad mixfix declaration for " ^ quote c)
+fun prep_struct (Fixed, (c, _, Structure _)) = SOME c
+ | prep_struct (_, (c, _, mx as Structure _)) =
+ error ("Bad mixfix declaration for " ^ quote c ^ Position.here (Mixfix.pos_of mx))
| prep_struct _ = NONE;
in
fun update_syntax ctxt add raw_decls (syntax as (Syntax {mode, mixfixes, ...})) =
- (case filter_out (fn (_, (_, _, mx)) => mx = NoSyn) raw_decls of
+ (case filter_out (Mixfix.is_empty o #3 o #2) raw_decls of
[] => (NONE, syntax)
| decls =>
let
--- a/src/Pure/Syntax/mixfix.ML Tue Mar 29 21:25:19 2016 +0200
+++ b/src/Pure/Syntax/mixfix.ML Tue Mar 29 23:45:28 2016 +0200
@@ -8,18 +8,23 @@
sig
datatype mixfix =
NoSyn |
- Mixfix of string * int list * int |
- Delimfix of string |
- Infix of string * int |
- Infixl of string * int |
- Infixr of string * int |
- Binder of string * int * int |
- Structure
+ Mixfix of Input.source * int list * int * Position.range |
+ Delimfix of Input.source * Position.range |
+ Infix of Input.source * int * Position.range |
+ Infixl of Input.source * int * Position.range |
+ Infixr of Input.source * int * Position.range |
+ Binder of Input.source * int * int * Position.range |
+ Structure of Position.range
end;
signature MIXFIX =
sig
include BASIC_MIXFIX
+ val is_empty: mixfix -> bool
+ val equal: mixfix * mixfix -> bool
+ val set_range: Position.range -> mixfix -> mixfix
+ val range_of: mixfix -> Position.range
+ val pos_of: mixfix -> Position.T
val pretty_mixfix: mixfix -> Pretty.T
val mixfix_args: mixfix -> int
val mixfixT: mixfix -> typ
@@ -36,20 +41,57 @@
datatype mixfix =
NoSyn |
- Mixfix of string * int list * int |
- Delimfix of string |
- Infix of string * int |
- Infixl of string * int |
- Infixr of string * int |
- Binder of string * int * int |
- Structure;
+ Mixfix of Input.source * int list * int * Position.range |
+ Delimfix of Input.source * Position.range |
+ Infix of Input.source * int * Position.range |
+ Infixl of Input.source * int * Position.range |
+ Infixr of Input.source * int * Position.range |
+ Binder of Input.source * int * int * Position.range |
+ Structure of Position.range;
+
+fun is_empty NoSyn = true
+ | is_empty _ = false;
+
+fun equal (NoSyn, NoSyn) = true
+ | equal (Mixfix (sy, ps, p, _), Mixfix (sy', ps', p', _)) =
+ Input.equal_content (sy, sy') andalso ps = ps' andalso p = p'
+ | equal (Delimfix (sy, _), Delimfix (sy', _)) = Input.equal_content (sy, sy')
+ | equal (Infix (sy, p, _), Infix (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p'
+ | equal (Infixl (sy, p, _), Infixl (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p'
+ | equal (Infixr (sy, p, _), Infixr (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p'
+ | equal (Binder (sy, p, q, _), Binder (sy', p', q', _)) =
+ Input.equal_content (sy, sy') andalso p = p' andalso q = q'
+ | equal (Structure _, Structure _) = true
+ | equal _ = false;
+
+fun set_range range mx =
+ (case mx of
+ NoSyn => NoSyn
+ | Mixfix (sy, ps, p, _) => Mixfix (sy, ps, p, range)
+ | Delimfix (sy, _) => Delimfix (sy, range)
+ | Infix (sy, p, _) => Infix (sy, p, range)
+ | Infixl (sy, p, _) => Infixl (sy, p, range)
+ | Infixr (sy, p, _) => Infixr (sy, p, range)
+ | Binder (sy, p, q, _) => Binder (sy, p, q, range)
+ | Structure _ => Structure range);
+
+fun range_of NoSyn = Position.no_range
+ | range_of (Mixfix (_, _, _, range)) = range
+ | range_of (Delimfix (_, range)) = range
+ | range_of (Infix (_, _, range)) = range
+ | range_of (Infixl (_, _, range)) = range
+ | range_of (Infixr (_, _, range)) = range
+ | range_of (Binder (_, _, _, range)) = range
+ | range_of (Structure range) = range;
+
+val pos_of = Position.set_range o range_of;
(* pretty_mixfix *)
local
-val quoted = Pretty.quote o Pretty.str;
+val quoted = Pretty.quote o Pretty.str o Input.source_content;
val keyword = Pretty.keyword2;
val parens = Pretty.enclose "(" ")";
val brackets = Pretty.enclose "[" "]";
@@ -58,15 +100,15 @@
in
fun pretty_mixfix NoSyn = Pretty.str ""
- | pretty_mixfix (Mixfix (s, ps, p)) =
+ | pretty_mixfix (Mixfix (s, ps, p, _)) =
parens (Pretty.breaks [quoted s, brackets (Pretty.commas (map int ps)), int p])
- | pretty_mixfix (Delimfix s) = parens [quoted s]
- | pretty_mixfix (Infix (s, p)) = parens (Pretty.breaks [keyword "infix", quoted s, int p])
- | pretty_mixfix (Infixl (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
- | pretty_mixfix (Infixr (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
- | pretty_mixfix (Binder (s, p1, p2)) =
+ | pretty_mixfix (Delimfix (s, _)) = parens [quoted s]
+ | pretty_mixfix (Infix (s, p, _)) = parens (Pretty.breaks [keyword "infix", quoted s, int p])
+ | pretty_mixfix (Infixl (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
+ | pretty_mixfix (Infixr (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
+ | pretty_mixfix (Binder (s, p1, p2, _)) =
parens (Pretty.breaks [keyword "binder", quoted s, brackets [int p1], int p2])
- | pretty_mixfix Structure = parens [keyword "structure"];
+ | pretty_mixfix (Structure _) = parens [keyword "structure"];
end;
@@ -74,13 +116,13 @@
(* syntax specifications *)
fun mixfix_args NoSyn = 0
- | mixfix_args (Mixfix (sy, _, _)) = Syntax_Ext.mfix_args sy
- | mixfix_args (Delimfix sy) = Syntax_Ext.mfix_args sy
- | mixfix_args (Infix (sy, _)) = 2 + Syntax_Ext.mfix_args sy
- | mixfix_args (Infixl (sy, _)) = 2 + Syntax_Ext.mfix_args sy
- | mixfix_args (Infixr (sy, _)) = 2 + Syntax_Ext.mfix_args sy
+ | mixfix_args (Mixfix (sy, _, _, _)) = Syntax_Ext.mixfix_args sy
+ | mixfix_args (Delimfix (sy, _)) = Syntax_Ext.mixfix_args sy
+ | mixfix_args (Infix (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy
+ | mixfix_args (Infixl (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy
+ | mixfix_args (Infixr (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy
| mixfix_args (Binder _) = 1
- | mixfix_args Structure = 0;
+ | mixfix_args (Structure _) = 0;
fun mixfixT (Binder _) = (dummyT --> dummyT) --> dummyT
| mixfixT mx = replicate (mixfix_args mx) dummyT ---> dummyT;
@@ -93,19 +135,26 @@
fun syn_ext_types type_decls =
let
- fun mk_infix sy ty t p1 p2 p3 = Syntax_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, t, [p1, p2], p3);
+ fun mk_infix sy ty t p1 p2 p3 range =
+ Syntax_Ext.Mfix
+ (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)",
+ ty, t, [p1, p2], p3, Position.set_range range);
fun mfix_of (_, _, NoSyn) = NONE
- | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (Syntax_Ext.Mfix (sy, ty, t, ps, p))
- | mfix_of (t, ty, Delimfix sy) = SOME (Syntax_Ext.Mfix (sy, ty, t, [], 1000))
- | mfix_of (t, ty, Infix (sy, p)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p)
- | mfix_of (t, ty, Infixl (sy, p)) = SOME (mk_infix sy ty t p (p + 1) p)
- | mfix_of (t, ty, Infixr (sy, p)) = SOME (mk_infix sy ty t (p + 1) p p)
+ | 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, Delimfix (sy, range)) =
+ SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, [], 1000, 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 check_args (_, ty, _) (SOME (mfix as Syntax_Ext.Mfix (sy, _, _, _, _))) =
+ fun check_args (_, ty, mx) (SOME (Syntax_Ext.Mfix (sy, _, _, _, _, _))) =
if length (Term.binder_types ty) = Syntax_Ext.mfix_args sy then ()
- else Syntax_Ext.err_in_mfix "Bad number of type constructor arguments" mfix
+ else
+ error ("Bad number of type constructor arguments in mixfix annotation" ^
+ Position.here (pos_of mx))
| check_args _ NONE = ();
val mfix = map mfix_of type_decls;
@@ -121,23 +170,32 @@
fun syn_ext_consts logical_types const_decls =
let
- fun mk_infix sy ty c p1 p2 p3 =
- [Syntax_Ext.Mfix ("op " ^ sy, ty, c, [], 1000),
- Syntax_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
+ fun mk_infix sy ty c p1 p2 p3 range =
+ [Syntax_Ext.Mfix
+ (Symbol_Pos.explode0 "op " @ Input.source_explode sy,
+ ty, c, [], 1000, Position.set_range range),
+ Syntax_Ext.Mfix
+ (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)",
+ ty, c, [p1, p2], p3, Position.set_range range)];
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)) = [Syntax_Ext.Mfix (sy, ty, c, ps, p)]
- | mfix_of (c, ty, Delimfix sy) = [Syntax_Ext.Mfix (sy, ty, c, [], 1000)]
- | mfix_of (c, ty, Infix (sy, p)) = mk_infix sy ty c (p + 1) (p + 1) p
- | mfix_of (c, ty, Infixl (sy, p)) = mk_infix sy ty c p (p + 1) p
- | mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p
- | mfix_of (c, ty, Binder (sy, p, q)) =
- [Syntax_Ext.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)]
- | mfix_of (c, _, _) = error ("Bad mixfix declaration for " ^ quote c);
+ | 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, Delimfix (sy, range)) =
+ [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, [], 1000, 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)) =
+ [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));
fun binder (c, _, Binder _) = SOME (binder_name c, c)
| binder _ = NONE;
@@ -159,4 +217,3 @@
structure Basic_Mixfix: BASIC_MIXFIX = Mixfix;
open Basic_Mixfix;
-
--- a/src/Pure/Syntax/simple_syntax.ML Tue Mar 29 21:25:19 2016 +0200
+++ b/src/Pure/Syntax/simple_syntax.ML Tue Mar 29 23:45:28 2016 +0200
@@ -21,7 +21,7 @@
fun read scan s =
(case
- Symbol_Pos.explode (s, Position.none) |>
+ Symbol_Pos.explode0 s |>
Lexicon.tokenize lexicon false |>
filter Lexicon.is_proper |>
Scan.read Lexicon.stopper scan of
--- a/src/Pure/Syntax/syntax.ML Tue Mar 29 21:25:19 2016 +0200
+++ b/src/Pure/Syntax/syntax.ML Tue Mar 29 23:45:28 2016 +0200
@@ -602,9 +602,9 @@
fun guess_infix (Syntax ({gram, ...}, _)) c =
(case Parser.guess_infix_lr (Lazy.force gram) c of
SOME (s, l, r, j) => SOME
- (if l then Mixfix.Infixl (s, j)
- else if r then Mixfix.Infixr (s, j)
- else Mixfix.Infix (s, j))
+ (if l then Mixfix.Infixl (Input.string s, j, Position.no_range)
+ else if r then Mixfix.Infixr (Input.string s, j, Position.no_range)
+ else Mixfix.Infix (Input.string s, j, Position.no_range))
| NONE => NONE);
--- a/src/Pure/Syntax/syntax_ext.ML Tue Mar 29 21:25:19 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML Tue Mar 29 23:45:28 2016 +0200
@@ -7,8 +7,7 @@
signature SYNTAX_EXT =
sig
val dddot_indexname: indexname
- datatype mfix = Mfix of string * typ * string * int list * int
- val err_in_mfix: string -> mfix -> 'a
+ datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int * Position.T
val typ_to_nonterm: typ -> string
datatype xsymb =
Delim of string |
@@ -28,8 +27,8 @@
print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list,
print_rules: (Ast.ast * Ast.ast) list,
print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list}
- val mfix_delims: string -> string list
- val mfix_args: string -> int
+ val mfix_args: Symbol_Pos.T list -> int
+ val mixfix_args: Input.source -> int
val escape: string -> string
val syn_ext': string list -> mfix list ->
(string * string) list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
@@ -111,17 +110,15 @@
(** datatype mfix **)
-(*Mfix (sy, ty, c, ps, p):
- sy: rhs of production as symbolic string
+(*Mfix (sy, ty, c, ps, p, pos):
+ sy: rhs of production as symbolic text
ty: type description of production
c: head of parse tree
ps: priorities of arguments in sy
- p: priority of production*)
+ p: priority of production
+ pos: source position*)
-datatype mfix = Mfix of string * typ * string * int list * int;
-
-fun err_in_mfix msg (Mfix (sy, _, const, _, _)) =
- cat_error msg ("in mixfix annotation " ^ quote sy ^ " for " ^ quote const);
+datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int * Position.T;
(* typ_to_nonterm *)
@@ -140,11 +137,17 @@
local
+open Basic_Symbol_Pos;
+
+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>"];
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);
+ $$ "'" |-- 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);
@@ -152,19 +155,19 @@
val scan_sym =
$$ "_" >> K (Argument ("", 0)) ||
$$ "\<index>" >> K index ||
- $$ "(" |-- Scan.many Symbol.is_digit >> (Bg o read_int) ||
+ $$ "(" |-- scan_many Symbol.is_digit >> (Bg o read_int o map Symbol_Pos.symbol) ||
$$ ")" >> K En ||
$$ "/" -- $$ "/" >> K (Brk ~1) ||
- $$ "/" |-- Scan.many Symbol.is_blank >> (Brk o length) ||
- Scan.many1 Symbol.is_blank >> (Space o implode) ||
- Scan.repeat1 scan_delim_char >> (Delim o implode);
+ $$ "/" |-- scan_many Symbol.is_blank >> (Brk o length) ||
+ scan_many1 Symbol.is_blank >> (Space o Symbol_Pos.content) ||
+ Scan.repeat1 scan_delim_char >> (Delim o Symbol_Pos.content);
val scan_symb =
scan_sym >> SOME ||
- $$ "'" -- Scan.one Symbol.is_blank >> K NONE;
+ $$ "'" -- scan_one Symbol.is_blank >> K NONE;
val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (~$$ "'");
-val read_symbs = map_filter I o the o Scan.read Symbol.stopper scan_symbs;
+val read_symbs = map_filter I o the o Scan.read Symbol_Pos.stopper scan_symbs;
fun unique_index xsymbs =
if length (filter is_index xsymbs) <= 1 then xsymbs
@@ -172,10 +175,10 @@
in
-val read_mfix = unique_index o read_symbs o Symbol.explode;
+val read_mfix = unique_index o read_symbs;
-fun mfix_delims sy = fold_rev (fn Delim s => cons s | _ => I) (read_mfix sy) [];
val mfix_args = length o filter is_argument o read_mfix;
+val mixfix_args = mfix_args o Input.source_explode;
val escape = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode;
@@ -184,13 +187,15 @@
(* mfix_to_xprod *)
-fun mfix_to_xprod logical_types (mfix as Mfix (sy, typ, const, pris, pri)) =
+fun mfix_to_xprod logical_types (Mfix (sy, typ, const, pris, pri, pos)) =
let
val is_logtype = member (op =) logical_types;
+ fun err msg = error (msg ^ " in mixfix annotation" ^ Position.here pos);
+
fun check_pri p =
if p >= 0 andalso p <= 1000 then ()
- else err_in_mfix ("Precedence out of range: " ^ string_of_int p) mfix;
+ else err ("Precedence " ^ string_of_int p ^ " out of range");
fun blocks_ok [] 0 = true
| blocks_ok [] _ = false
@@ -201,21 +206,20 @@
fun check_blocks syms =
if blocks_ok syms 0 then ()
- else err_in_mfix "Unbalanced block parentheses" mfix;
+ else err "Unbalanced block parentheses";
val cons_fst = apfst o cons;
fun add_args [] ty [] = ([], typ_to_nonterm1 ty)
- | add_args [] _ _ = err_in_mfix "Too many precedences" mfix
+ | add_args [] _ _ = err "Too many precedences"
| add_args ((arg as Argument ("index", _)) :: syms) ty ps =
cons_fst arg (add_args syms ty ps)
| add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) [] =
cons_fst (Argument (typ_to_nonterm ty, 0)) (add_args syms tys [])
| add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) =
cons_fst (Argument (typ_to_nonterm ty, p)) (add_args syms tys ps)
- | add_args (Argument _ :: _) _ _ =
- err_in_mfix "More arguments than in corresponding type" mfix
+ | add_args (Argument _ :: _) _ _ = err "More arguments than in corresponding type"
| add_args (sym :: syms) ty ps = cons_fst sym (add_args syms ty ps);
fun rem_pri (Argument (s, _)) = Argument (s, chain_pri)
@@ -226,7 +230,7 @@
| logify_types a = a;
- val raw_symbs = read_mfix sy handle ERROR msg => err_in_mfix msg mfix;
+ val raw_symbs = read_mfix sy handle ERROR msg => err msg;
val args = filter (fn Argument _ => true | _ => false) raw_symbs;
val (const', typ', syntax_consts, parse_rules) =
if not (exists is_index args) then (const, typ, NONE, NONE)
@@ -234,9 +238,9 @@
let
val indexed_const =
if const <> "" then const ^ "_indexed"
- else err_in_mfix "Missing constant name for indexed syntax" mfix;
+ else err "Missing constant name for indexed syntax";
val rangeT = Term.range_type typ handle Match =>
- err_in_mfix "Missing structure argument for indexed syntax" mfix;
+ err "Missing structure argument for indexed syntax";
val xs = map Ast.Variable (Name.invent Name.context "xa" (length args - 1));
val (xs1, xs2) = chop (find_index is_index args) xs;
@@ -263,10 +267,10 @@
val _ = (List.app check_pri pris; check_pri pri; check_blocks symbs');
val xprod' =
- if Lexicon.is_terminal lhs' then err_in_mfix ("Illegal lhs: " ^ lhs') mfix
+ if Lexicon.is_terminal lhs' then err ("Illegal lhs " ^ quote lhs')
else if const <> "" then xprod
else if length (filter is_argument symbs') <> 1 then
- err_in_mfix "Copy production must have exactly one argument" mfix
+ err "Copy production must have exactly one argument"
else if exists is_terminal symbs' then xprod
else XProd (lhs', map rem_pri symbs', "", chain_pri);
--- a/src/Pure/System/isabelle_process.scala Tue Mar 29 21:25:19 2016 +0200
+++ b/src/Pure/System/isabelle_process.scala Tue Mar 29 23:45:28 2016 +0200
@@ -13,6 +13,7 @@
options: Options,
logic: String = "",
args: List[String] = Nil,
+ dirs: List[Path] = Nil,
modes: List[String] = Nil,
receiver: Prover.Receiver = Console.println(_),
store: Sessions.Store = Sessions.store()): Isabelle_Process =
@@ -20,8 +21,8 @@
val channel = System_Channel()
val process =
try {
- ML_Process(options, logic = logic, args = args, modes = modes, store = store,
- channel = Some(channel))
+ ML_Process(options, logic = logic, args = args, dirs = dirs,
+ modes = modes, store = store, channel = Some(channel))
}
catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
process.stdin.close
--- a/src/Pure/Thy/thy_output.ML Tue Mar 29 21:25:19 2016 +0200
+++ b/src/Pure/Thy/thy_output.ML Tue Mar 29 23:45:28 2016 +0200
@@ -195,10 +195,19 @@
fun output_text state {markdown} source =
let
+ val is_reported =
+ (case try Toplevel.context_of state of
+ SOME ctxt => Context_Position.is_visible ctxt
+ | NONE => true);
+
val pos = Input.pos_of source;
- val _ = Position.report pos (Markup.language_document (Input.is_delimited source));
val syms = Input.source_explode source;
+ val _ =
+ if is_reported then
+ Position.report pos (Markup.language_document (Input.is_delimited source))
+ else ();
+
val output_antiquotes = map (eval_antiquote state) #> implode;
fun output_line line =
@@ -214,14 +223,16 @@
else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
then
let
- val ants = Antiquote.read' pos syms;
+ val ants = Antiquote.parse pos syms;
+ val reports = Antiquote.antiq_reports ants;
val blocks = Markdown.read_antiquotes ants;
- val _ = Position.reports (Markdown.reports blocks);
+ val _ = if is_reported then Position.reports (reports @ Markdown.reports blocks) else ();
in output_blocks blocks end
else
let
- val ants = Antiquote.read' pos (Symbol_Pos.trim_blanks syms);
- val _ = Position.reports (Markdown.text_reports ants);
+ val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms);
+ val reports = Antiquote.antiq_reports ants;
+ val _ = if is_reported then Position.reports (reports @ Markdown.text_reports ants) else ();
in output_antiquotes ants end
end;
--- a/src/Pure/Tools/ml_console.scala Tue Mar 29 21:25:19 2016 +0200
+++ b/src/Pure/Tools/ml_console.scala Tue Mar 29 23:45:28 2016 +0200
@@ -70,7 +70,7 @@
// process loop
val process =
- ML_Process(options, logic = logic, args = List("-i"),
+ ML_Process(options, logic = logic, args = List("-i"), dirs = dirs,
modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
raw_ml_system = raw_ml_system, store = Sessions.store(system_mode))
val process_output = Future.thread[Unit]("process_output") {
--- a/src/Pure/Tools/rail.ML Tue Mar 29 21:25:19 2016 +0200
+++ b/src/Pure/Tools/rail.ML Tue Mar 29 23:45:28 2016 +0200
@@ -5,7 +5,22 @@
Railroad diagrams in LaTeX.
*)
-structure Rail: sig end =
+signature RAIL =
+sig
+ datatype rails =
+ Cat of int * rail list
+ and rail =
+ Bar of rails list |
+ Plus of rails * rails |
+ Newline of int |
+ Nonterminal of string |
+ Terminal of bool * string |
+ Antiquote of bool * Antiquote.antiq
+ val read: Proof.context -> Input.source -> (string Antiquote.antiquote * rail) list
+ val output_rules: Toplevel.state -> (string Antiquote.antiquote * rail) list -> string
+end;
+
+structure Rail: RAIL =
struct
(** lexical syntax **)
@@ -313,6 +328,8 @@
| vertical_range (Newline _) y = (Newline (y + 2), y + 3)
| vertical_range atom y = (atom, y + 1);
+in
+
fun output_rules state rules =
let
val output_antiq = Thy_Output.eval_antiquote state o Antiquote.Antiq;
@@ -356,8 +373,6 @@
end;
in Latex.environment "railoutput" (implode (map output_rule rules)) end;
-in
-
val _ = Theory.setup
(Thy_Output.antiquotation @{binding rail} (Scan.lift Args.text_input)
(fn {state, context, ...} => output_rules state o read context));
@@ -365,4 +380,3 @@
end;
end;
-
--- a/src/Pure/pure_thy.ML Tue Mar 29 21:25:19 2016 +0200
+++ b/src/Pure/pure_thy.ML Tue Mar 29 23:45:28 2016 +0200
@@ -22,18 +22,24 @@
val qualify = Binding.qualify true Context.PureN;
+fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range);
+fun delimfix sy = Delimfix (Input.string sy, Position.no_range);
+fun infix_ (sy, p) = Infix (Input.string sy, p, Position.no_range);
+fun infixr_ (sy, p) = Infixr (Input.string sy, p, Position.no_range);
+fun binder (sy, p, q) = Binder (Input.string sy, p, q, Position.no_range);
+
(* application syntax variants *)
val appl_syntax =
- [("_appl", typ "('b => 'a) => args => logic", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000)),
- ("_appl", typ "('b => 'a) => args => aprop", Mixfix ("(1_/(1'(_')))", [1000, 0], 1000))];
+ [("_appl", typ "('b => 'a) => args => logic", mixfix ("(1_/(1'(_')))", [1000, 0], 1000)),
+ ("_appl", typ "('b => 'a) => args => aprop", mixfix ("(1_/(1'(_')))", [1000, 0], 1000))];
val applC_syntax =
- [("", typ "'a => cargs", Delimfix "_"),
- ("_cargs", typ "'a => cargs => cargs", Mixfix ("_/ _", [1000, 1000], 1000)),
- ("_applC", typ "('b => 'a) => cargs => logic", Mixfix ("(1_/ _)", [1000, 1000], 999)),
- ("_applC", typ "('b => 'a) => cargs => aprop", Mixfix ("(1_/ _)", [1000, 1000], 999))];
+ [("", typ "'a => cargs", delimfix "_"),
+ ("_cargs", typ "'a => cargs => cargs", mixfix ("_/ _", [1000, 1000], 1000)),
+ ("_applC", typ "('b => 'a) => cargs => logic", mixfix ("(1_/ _)", [1000, 1000], 999)),
+ ("_applC", typ "('b => 'a) => cargs => aprop", mixfix ("(1_/ _)", [1000, 1000], 999))];
structure Old_Appl_Syntax = Theory_Data
(
@@ -81,120 +87,120 @@
"class_name"]))
#> Sign.add_syntax Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers)
#> Sign.add_syntax Syntax.mode_default
- [("", typ "prop' => prop", Delimfix "_"),
- ("", typ "logic => any", Delimfix "_"),
- ("", typ "prop' => any", Delimfix "_"),
- ("", typ "logic => logic", Delimfix "'(_')"),
- ("", typ "prop' => prop'", Delimfix "'(_')"),
- ("_constrain", typ "logic => type => logic", Mixfix ("_::_", [4, 0], 3)),
- ("_constrain", typ "prop' => type => prop'", Mixfix ("_::_", [4, 0], 3)),
+ [("", typ "prop' => prop", delimfix "_"),
+ ("", typ "logic => any", delimfix "_"),
+ ("", typ "prop' => any", delimfix "_"),
+ ("", typ "logic => logic", delimfix "'(_')"),
+ ("", typ "prop' => prop'", delimfix "'(_')"),
+ ("_constrain", typ "logic => type => logic", mixfix ("_::_", [4, 0], 3)),
+ ("_constrain", typ "prop' => type => prop'", mixfix ("_::_", [4, 0], 3)),
("_ignore_type", typ "'a", NoSyn),
- ("", typ "tid_position => type", Delimfix "_"),
- ("", typ "tvar_position => type", Delimfix "_"),
- ("", typ "type_name => type", Delimfix "_"),
- ("_type_name", typ "id => type_name", Delimfix "_"),
- ("_type_name", typ "longid => type_name", Delimfix "_"),
- ("_ofsort", typ "tid_position => sort => type", Mixfix ("_::_", [1000, 0], 1000)),
- ("_ofsort", typ "tvar_position => sort => type", Mixfix ("_::_", [1000, 0], 1000)),
- ("_dummy_ofsort", typ "sort => type", Mixfix ("'_()::_", [0], 1000)),
- ("", typ "class_name => sort", Delimfix "_"),
- ("_class_name", typ "id => class_name", Delimfix "_"),
- ("_class_name", typ "longid => class_name", Delimfix "_"),
- ("_topsort", typ "sort", Delimfix "{}"),
- ("_sort", typ "classes => sort", Delimfix "{_}"),
- ("", typ "class_name => classes", Delimfix "_"),
- ("_classes", typ "class_name => classes => classes", Delimfix "_,_"),
- ("_tapp", typ "type => type_name => type", Mixfix ("_ _", [1000, 0], 1000)),
- ("_tappl", typ "type => types => type_name => type", Delimfix "((1'(_,/ _')) _)"),
- ("", typ "type => types", Delimfix "_"),
- ("_types", typ "type => types => types", Delimfix "_,/ _"),
- ("\<^type>fun", typ "type => type => type", Mixfix ("(_/ \<Rightarrow> _)", [1, 0], 0)),
- ("_bracket", typ "types => type => type", Mixfix ("([_]/ \<Rightarrow> _)", [0, 0], 0)),
- ("", typ "type => type", Delimfix "'(_')"),
- ("\<^type>dummy", typ "type", Delimfix "'_"),
+ ("", typ "tid_position => type", delimfix "_"),
+ ("", typ "tvar_position => type", delimfix "_"),
+ ("", typ "type_name => type", delimfix "_"),
+ ("_type_name", typ "id => type_name", delimfix "_"),
+ ("_type_name", typ "longid => type_name", delimfix "_"),
+ ("_ofsort", typ "tid_position => sort => type", mixfix ("_::_", [1000, 0], 1000)),
+ ("_ofsort", typ "tvar_position => sort => type", mixfix ("_::_", [1000, 0], 1000)),
+ ("_dummy_ofsort", typ "sort => type", mixfix ("'_()::_", [0], 1000)),
+ ("", typ "class_name => sort", delimfix "_"),
+ ("_class_name", typ "id => class_name", delimfix "_"),
+ ("_class_name", typ "longid => class_name", delimfix "_"),
+ ("_topsort", typ "sort", delimfix "{}"),
+ ("_sort", typ "classes => sort", delimfix "{_}"),
+ ("", typ "class_name => classes", delimfix "_"),
+ ("_classes", typ "class_name => classes => classes", delimfix "_,_"),
+ ("_tapp", typ "type => type_name => type", mixfix ("_ _", [1000, 0], 1000)),
+ ("_tappl", typ "type => types => type_name => type", delimfix "((1'(_,/ _')) _)"),
+ ("", typ "type => types", delimfix "_"),
+ ("_types", typ "type => types => types", delimfix "_,/ _"),
+ ("\<^type>fun", typ "type => type => type", mixfix ("(_/ \<Rightarrow> _)", [1, 0], 0)),
+ ("_bracket", typ "types => type => type", mixfix ("([_]/ \<Rightarrow> _)", [0, 0], 0)),
+ ("", typ "type => type", delimfix "'(_')"),
+ ("\<^type>dummy", typ "type", delimfix "'_"),
("_type_prop", typ "'a", NoSyn),
- ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\<lambda>_./ _)", [0, 3], 3)),
+ ("_lambda", typ "pttrns => 'a => logic", mixfix ("(3\<lambda>_./ _)", [0, 3], 3)),
("_abs", typ "'a", NoSyn),
- ("", typ "'a => args", Delimfix "_"),
- ("_args", typ "'a => args => args", Delimfix "_,/ _"),
- ("", typ "id_position => idt", Delimfix "_"),
- ("_idtdummy", typ "idt", Delimfix "'_"),
- ("_idtyp", typ "id_position => type => idt", Mixfix ("_::_", [], 0)),
- ("_idtypdummy", typ "type => idt", Mixfix ("'_()::_", [], 0)),
- ("", typ "idt => idt", Delimfix "'(_')"),
- ("", typ "idt => idts", Delimfix "_"),
- ("_idts", typ "idt => idts => idts", Mixfix ("_/ _", [1, 0], 0)),
- ("", typ "idt => pttrn", Delimfix "_"),
- ("", typ "pttrn => pttrns", Delimfix "_"),
- ("_pttrns", typ "pttrn => pttrns => pttrns", Mixfix ("_/ _", [1, 0], 0)),
- ("", typ "aprop => aprop", Delimfix "'(_')"),
- ("", typ "id_position => aprop", Delimfix "_"),
- ("", typ "longid_position => aprop", Delimfix "_"),
- ("", typ "var_position => aprop", Delimfix "_"),
- ("_DDDOT", typ "aprop", Delimfix "\<dots>"),
- ("_aprop", typ "aprop => prop", Delimfix "PROP _"),
- ("_asm", typ "prop => asms", Delimfix "_"),
- ("_asms", typ "prop => asms => asms", Delimfix "_;/ _"),
- ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\<lbrakk>_\<rbrakk>)/ \<Longrightarrow> _)", [0, 1], 1)),
- ("_ofclass", typ "type => logic => prop", Delimfix "(1OFCLASS/(1'(_,/ _')))"),
+ ("", typ "'a => args", delimfix "_"),
+ ("_args", typ "'a => args => args", delimfix "_,/ _"),
+ ("", typ "id_position => idt", delimfix "_"),
+ ("_idtdummy", typ "idt", delimfix "'_"),
+ ("_idtyp", typ "id_position => type => idt", mixfix ("_::_", [], 0)),
+ ("_idtypdummy", typ "type => idt", mixfix ("'_()::_", [], 0)),
+ ("", typ "idt => idt", delimfix "'(_')"),
+ ("", typ "idt => idts", delimfix "_"),
+ ("_idts", typ "idt => idts => idts", mixfix ("_/ _", [1, 0], 0)),
+ ("", typ "idt => pttrn", delimfix "_"),
+ ("", typ "pttrn => pttrns", delimfix "_"),
+ ("_pttrns", typ "pttrn => pttrns => pttrns", mixfix ("_/ _", [1, 0], 0)),
+ ("", typ "aprop => aprop", delimfix "'(_')"),
+ ("", typ "id_position => aprop", delimfix "_"),
+ ("", typ "longid_position => aprop", delimfix "_"),
+ ("", typ "var_position => aprop", delimfix "_"),
+ ("_DDDOT", typ "aprop", delimfix "\<dots>"),
+ ("_aprop", typ "aprop => prop", delimfix "PROP _"),
+ ("_asm", typ "prop => asms", delimfix "_"),
+ ("_asms", typ "prop => asms => asms", delimfix "_;/ _"),
+ ("_bigimpl", typ "asms => prop => prop", mixfix ("((1\<lbrakk>_\<rbrakk>)/ \<Longrightarrow> _)", [0, 1], 1)),
+ ("_ofclass", typ "type => logic => prop", delimfix "(1OFCLASS/(1'(_,/ _')))"),
("_mk_ofclass", typ "dummy", NoSyn),
- ("_TYPE", typ "type => logic", Delimfix "(1TYPE/(1'(_')))"),
- ("", typ "id_position => logic", Delimfix "_"),
- ("", typ "longid_position => logic", Delimfix "_"),
- ("", typ "var_position => logic", Delimfix "_"),
- ("_DDDOT", typ "logic", Delimfix "\<dots>"),
+ ("_TYPE", typ "type => logic", delimfix "(1TYPE/(1'(_')))"),
+ ("", typ "id_position => logic", delimfix "_"),
+ ("", typ "longid_position => logic", delimfix "_"),
+ ("", typ "var_position => logic", delimfix "_"),
+ ("_DDDOT", typ "logic", delimfix "\<dots>"),
("_strip_positions", typ "'a", NoSyn),
- ("_position", typ "num_token => num_position", Delimfix "_"),
- ("_position", typ "float_token => float_position", Delimfix "_"),
- ("_constify", typ "num_position => num_const", Delimfix "_"),
- ("_constify", typ "float_position => float_const", Delimfix "_"),
- ("_index", typ "logic => index", Delimfix "(00\<^bsub>_\<^esub>)"),
- ("_indexdefault", typ "index", Delimfix ""),
- ("_indexvar", typ "index", Delimfix "'\<index>"),
+ ("_position", typ "num_token => num_position", delimfix "_"),
+ ("_position", typ "float_token => float_position", delimfix "_"),
+ ("_constify", typ "num_position => num_const", delimfix "_"),
+ ("_constify", typ "float_position => float_const", delimfix "_"),
+ ("_index", typ "logic => index", delimfix "(00\<^bsub>_\<^esub>)"),
+ ("_indexdefault", typ "index", delimfix ""),
+ ("_indexvar", typ "index", delimfix "'\<index>"),
("_struct", typ "index => logic", NoSyn),
("_update_name", typ "idt", NoSyn),
("_constrainAbs", typ "'a", NoSyn),
- ("_position_sort", typ "tid => tid_position", Delimfix "_"),
- ("_position_sort", typ "tvar => tvar_position", Delimfix "_"),
- ("_position", typ "id => id_position", Delimfix "_"),
- ("_position", typ "longid => longid_position", Delimfix "_"),
- ("_position", typ "var => var_position", Delimfix "_"),
- ("_position", typ "str_token => str_position", Delimfix "_"),
- ("_position", typ "string_token => string_position", Delimfix "_"),
- ("_position", typ "cartouche => cartouche_position", Delimfix "_"),
+ ("_position_sort", typ "tid => tid_position", delimfix "_"),
+ ("_position_sort", typ "tvar => tvar_position", delimfix "_"),
+ ("_position", typ "id => id_position", delimfix "_"),
+ ("_position", typ "longid => longid_position", delimfix "_"),
+ ("_position", typ "var => var_position", delimfix "_"),
+ ("_position", typ "str_token => str_position", delimfix "_"),
+ ("_position", typ "string_token => string_position", delimfix "_"),
+ ("_position", typ "cartouche => cartouche_position", delimfix "_"),
("_type_constraint_", typ "'a", NoSyn),
- ("_context_const", typ "id_position => logic", Delimfix "CONST _"),
- ("_context_const", typ "id_position => aprop", Delimfix "CONST _"),
- ("_context_const", typ "longid_position => logic", Delimfix "CONST _"),
- ("_context_const", typ "longid_position => aprop", Delimfix "CONST _"),
- ("_context_xconst", typ "id_position => logic", Delimfix "XCONST _"),
- ("_context_xconst", typ "id_position => aprop", Delimfix "XCONST _"),
- ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"),
- ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"),
- (const "Pure.dummy_pattern", typ "aprop", Delimfix "'_"),
- ("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
- (const "Pure.term", typ "logic => prop", Delimfix "TERM _"),
- (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
+ ("_context_const", typ "id_position => logic", delimfix "CONST _"),
+ ("_context_const", typ "id_position => aprop", delimfix "CONST _"),
+ ("_context_const", typ "longid_position => logic", delimfix "CONST _"),
+ ("_context_const", typ "longid_position => aprop", delimfix "CONST _"),
+ ("_context_xconst", typ "id_position => logic", delimfix "XCONST _"),
+ ("_context_xconst", typ "id_position => aprop", delimfix "XCONST _"),
+ ("_context_xconst", typ "longid_position => logic", delimfix "XCONST _"),
+ ("_context_xconst", typ "longid_position => aprop", delimfix "XCONST _"),
+ (const "Pure.dummy_pattern", typ "aprop", delimfix "'_"),
+ ("_sort_constraint", typ "type => prop", delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
+ (const "Pure.term", typ "logic => prop", delimfix "TERM _"),
+ (const "Pure.conjunction", typ "prop => prop => prop", infixr_ ("&&&", 2))]
#> Sign.add_syntax Syntax.mode_default applC_syntax
#> Sign.add_syntax (Print_Mode.ASCII, true)
- [(tycon "fun", typ "type => type => type", Mixfix ("(_/ => _)", [1, 0], 0)),
- ("_bracket", typ "types => type => type", Mixfix ("([_]/ => _)", [0, 0], 0)),
- ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3%_./ _)", [0, 3], 3)),
- (const "Pure.eq", typ "'a => 'a => prop", Infix ("==", 2)),
- (const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3!!_./ _)", [0, 0], 0)),
- (const "Pure.imp", typ "prop => prop => prop", Infixr ("==>", 1)),
- ("_DDDOT", typ "aprop", Delimfix "..."),
- ("_bigimpl", typ "asms => prop => prop", Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
- ("_DDDOT", typ "logic", Delimfix "...")]
+ [(tycon "fun", typ "type => type => type", mixfix ("(_/ => _)", [1, 0], 0)),
+ ("_bracket", typ "types => type => type", mixfix ("([_]/ => _)", [0, 0], 0)),
+ ("_lambda", typ "pttrns => 'a => logic", mixfix ("(3%_./ _)", [0, 3], 3)),
+ (const "Pure.eq", typ "'a => 'a => prop", infix_ ("==", 2)),
+ (const "Pure.all_binder", typ "idts => prop => prop", mixfix ("(3!!_./ _)", [0, 0], 0)),
+ (const "Pure.imp", typ "prop => prop => prop", infixr_ ("==>", 1)),
+ ("_DDDOT", typ "aprop", delimfix "..."),
+ ("_bigimpl", typ "asms => prop => prop", mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
+ ("_DDDOT", typ "logic", delimfix "...")]
#> Sign.add_syntax ("", false)
- [(const "Pure.prop", typ "prop => prop", Mixfix ("_", [0], 0))]
+ [(const "Pure.prop", typ "prop => prop", mixfix ("_", [0], 0))]
#> Sign.add_consts
- [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", Infix ("\<equiv>", 2)),
- (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", Infixr ("\<Longrightarrow>", 1)),
- (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", Binder ("\<And>", 0, 0)),
+ [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", infix_ ("\<equiv>", 2)),
+ (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", infixr_ ("\<Longrightarrow>", 1)),
+ (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", binder ("\<And>", 0, 0)),
(qualify (Binding.make ("prop", @{here})), typ "prop => prop", NoSyn),
(qualify (Binding.make ("type", @{here})), typ "'a itself", NoSyn),
- (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", Delimfix "'_")]
+ (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", delimfix "'_")]
#> Theory.add_deps_global "Pure.eq" ((Defs.Const, "Pure.eq"), [typ "'a"]) []
#> Theory.add_deps_global "Pure.imp" ((Defs.Const, "Pure.imp"), []) []
#> Theory.add_deps_global "Pure.all" ((Defs.Const, "Pure.all"), [typ "'a"]) []
--- a/src/Tools/jEdit/src/isabelle_logic.scala Tue Mar 29 21:25:19 2016 +0200
+++ b/src/Tools/jEdit/src/isabelle_logic.scala Tue Mar 29 23:45:28 2016 +0200
@@ -75,8 +75,8 @@
(space_explode(',', PIDE.options.string("jedit_print_mode")) :::
space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse
PIDE.session.start(receiver =>
- Isabelle_Process(
- PIDE.options.value, logic = session_name(), modes = modes, receiver = receiver,
+ Isabelle_Process(PIDE.options.value, logic = session_name(), dirs = session_dirs(),
+ modes = modes, receiver = receiver,
store = Sessions.store(session_build_mode() == "system")))
}