--- a/NEWS Tue Aug 02 13:13:15 2016 +0200
+++ b/NEWS Tue Aug 02 18:58:49 2016 +0200
@@ -111,6 +111,12 @@
* Completion templates for commands involving "begin ... end" blocks,
e.g. 'context', 'notepad'.
+* Additional abbreviations for syntactic completion may be specified
+within the theory header as 'abbrevs', in addition to global
+$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs as
+before. The theory syntax for 'keywords' has been simplified
+accordingly: optional abbrevs need to go into the new 'abbrevs' section.
+
*** Isar ***
--- a/etc/abbrevs Tue Aug 02 13:13:15 2016 +0200
+++ b/etc/abbrevs Tue Aug 02 18:58:49 2016 +0200
@@ -4,7 +4,3 @@
"===>" = "===>"
"--->" = "\<midarrow>\<rightarrow>"
-
-(*HOL-NSA*)
-"--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
-"--->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S"
--- a/src/Doc/Isar_Ref/Spec.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Tue Aug 02 18:58:49 2016 +0200
@@ -58,14 +58,14 @@
such a global @{command (global) "end"}.
@{rail \<open>
- @@{command theory} @{syntax name} imports? keywords? \<newline> @'begin'
- ;
- imports: @'imports' (@{syntax name} +)
+ @@{command theory} @{syntax name} @'imports' (@{syntax name} +) \<newline>
+ keywords? abbrevs? @'begin'
;
keywords: @'keywords' (keyword_decls + @'and')
;
- keyword_decls: (@{syntax string} +)
- ('::' @{syntax name} @{syntax tags})? ('==' @{syntax name})?
+ keyword_decls: (@{syntax string} +) ('::' @{syntax name} @{syntax tags})?
+ ;
+ abbrevs: @'abbrevs' ((text '=' text) +)
;
@@{command thy_deps} (thy_bounds thy_bounds?)?
;
@@ -85,7 +85,7 @@
based on Isabelle. Regular user theories usually refer to some more complex
entry point, such as theory @{theory Main} in Isabelle/HOL.
- The optional @{keyword_def "keywords"} specification declares outer syntax
+ The @{keyword_def "keywords"} specification declares outer syntax
(\chref{ch:outer-syntax}) that is introduced in this theory later on (rare
in end-user applications). Both minor keywords and major keywords of the
Isar command language need to be specified, in order to make parsing of
@@ -97,8 +97,10 @@
@{syntax tags} provide defaults for document preparation
(\secref{sec:tags}).
- It is possible to specify an alternative completion via \<^verbatim>\<open>==\<close>~\<open>text\<close>, while
- the default is the corresponding keyword name.
+ The @{keyword_def "abbrevs"} specification declares additional abbreviations
+ for syntactic completion. The default for a new keyword is just its name,
+ but completion may be avoided by defining @{keyword "abbrevs"} with empty
+ text.
\<^descr> @{command (global) "end"} concludes the current theory definition. Note
that some other commands, e.g.\ local theory targets \<^theory_text>\<open>locale\<close> or \<^theory_text>\<open>class\<close>
--- a/src/HOL/Isar_Examples/Basic_Logic.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Basic_Logic.thy Tue Aug 02 18:58:49 2016 +0200
@@ -7,7 +7,7 @@
section \<open>Basic logical reasoning\<close>
theory Basic_Logic
-imports Main
+ imports Main
begin
--- a/src/HOL/Isar_Examples/Cantor.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Cantor.thy Tue Aug 02 18:58:49 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Cantor's Theorem\<close>
theory Cantor
-imports Main
+ imports Main
begin
subsection \<open>Mathematical statement and proof\<close>
--- a/src/HOL/Isar_Examples/Drinker.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Drinker.thy Tue Aug 02 18:58:49 2016 +0200
@@ -5,7 +5,7 @@
section \<open>The Drinker's Principle\<close>
theory Drinker
-imports Main
+ imports Main
begin
text \<open>
--- a/src/HOL/Isar_Examples/Expr_Compiler.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Expr_Compiler.thy Tue Aug 02 18:58:49 2016 +0200
@@ -7,7 +7,7 @@
section \<open>Correctness of a simple expression compiler\<close>
theory Expr_Compiler
-imports Main
+ imports Main
begin
text \<open>
@@ -46,10 +46,10 @@
\<close>
primrec eval :: "('adr, 'val) expr \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val"
-where
- "eval (Variable x) env = env x"
-| "eval (Constant c) env = c"
-| "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)"
+ where
+ "eval (Variable x) env = env x"
+ | "eval (Constant c) env = c"
+ | "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)"
subsection \<open>Machine\<close>
@@ -69,14 +69,13 @@
\<close>
primrec exec :: "(('adr, 'val) instr) list \<Rightarrow> 'val list \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val list"
-where
- "exec [] stack env = stack"
-| "exec (instr # instrs) stack env =
- (case instr of
- Const c \<Rightarrow> exec instrs (c # stack) env
- | Load x \<Rightarrow> exec instrs (env x # stack) env
- | Apply f \<Rightarrow> exec instrs (f (hd stack) (hd (tl stack))
- # (tl (tl stack))) env)"
+ where
+ "exec [] stack env = stack"
+ | "exec (instr # instrs) stack env =
+ (case instr of
+ Const c \<Rightarrow> exec instrs (c # stack) env
+ | Load x \<Rightarrow> exec instrs (env x # stack) env
+ | Apply f \<Rightarrow> exec instrs (f (hd stack) (hd (tl stack)) # (tl (tl stack))) env)"
definition execute :: "(('adr, 'val) instr) list \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val"
where "execute instrs env = hd (exec instrs [] env)"
@@ -90,10 +89,10 @@
\<close>
primrec compile :: "('adr, 'val) expr \<Rightarrow> (('adr, 'val) instr) list"
-where
- "compile (Variable x) = [Load x]"
-| "compile (Constant c) = [Const c]"
-| "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"
+ where
+ "compile (Variable x) = [Load x]"
+ | "compile (Constant c) = [Const c]"
+ | "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"
text \<open>
--- a/src/HOL/Isar_Examples/Fibonacci.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Fibonacci.thy Tue Aug 02 18:58:49 2016 +0200
@@ -15,7 +15,7 @@
section \<open>Fib and Gcd commute\<close>
theory Fibonacci
-imports "../Number_Theory/Primes"
+ imports "../Number_Theory/Primes"
begin
text_raw \<open>\<^footnote>\<open>Isar version by Gertrud Bauer. Original tactic script by Larry
@@ -28,10 +28,10 @@
subsection \<open>Fibonacci numbers\<close>
fun fib :: "nat \<Rightarrow> nat"
-where
- "fib 0 = 0"
-| "fib (Suc 0) = 1"
-| "fib (Suc (Suc x)) = fib x + fib (Suc x)"
+ where
+ "fib 0 = 0"
+ | "fib (Suc 0) = 1"
+ | "fib (Suc (Suc x)) = fib x + fib (Suc x)"
lemma [simp]: "fib (Suc n) > 0"
by (induct n rule: fib.induct) simp_all
--- a/src/HOL/Isar_Examples/First_Order_Logic.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/First_Order_Logic.thy Tue Aug 02 18:58:49 2016 +0200
@@ -10,7 +10,7 @@
\<close>
theory First_Order_Logic
-imports Pure
+ imports Pure
begin
subsection \<open>Abstract syntax\<close>
--- a/src/HOL/Isar_Examples/Group.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Group.thy Tue Aug 02 18:58:49 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Basic group theory\<close>
theory Group
-imports Main
+ imports Main
begin
subsection \<open>Groups and calculational reasoning\<close>
--- a/src/HOL/Isar_Examples/Group_Context.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Group_Context.thy Tue Aug 02 18:58:49 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Some algebraic identities derived from group axioms -- theory context version\<close>
theory Group_Context
-imports Main
+ imports Main
begin
text \<open>hypothetical group axiomatization\<close>
--- a/src/HOL/Isar_Examples/Group_Notepad.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Group_Notepad.thy Tue Aug 02 18:58:49 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Some algebraic identities derived from group axioms -- proof notepad version\<close>
theory Group_Notepad
-imports Main
+ imports Main
begin
notepad
--- a/src/HOL/Isar_Examples/Higher_Order_Logic.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Higher_Order_Logic.thy Tue Aug 02 18:58:49 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Foundations of HOL\<close>
theory Higher_Order_Logic
-imports Pure
+ imports Pure
begin
text \<open>
@@ -76,7 +76,8 @@
subsubsection \<open>Derived connectives\<close>
-definition false :: o ("\<bottom>") where "\<bottom> \<equiv> \<forall>A. A"
+definition false :: o ("\<bottom>")
+ where "\<bottom> \<equiv> \<forall>A. A"
theorem falseE [elim]:
assumes "\<bottom>"
@@ -87,7 +88,8 @@
qed
-definition true :: o ("\<top>") where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
+definition true :: o ("\<top>")
+ where "\<top> \<equiv> \<bottom> \<longrightarrow> \<bottom>"
theorem trueI [intro]: \<top>
unfolding true_def ..
--- a/src/HOL/Isar_Examples/Hoare.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Hoare.thy Tue Aug 02 18:58:49 2016 +0200
@@ -7,7 +7,7 @@
section \<open>Hoare Logic\<close>
theory Hoare
-imports Main
+ imports Main
begin
subsection \<open>Abstract syntax and semantics\<close>
@@ -34,28 +34,24 @@
type_synonym 'a sem = "'a \<Rightarrow> 'a \<Rightarrow> bool"
primrec iter :: "nat \<Rightarrow> 'a bexp \<Rightarrow> 'a sem \<Rightarrow> 'a sem"
-where
- "iter 0 b S s s' \<longleftrightarrow> s \<notin> b \<and> s = s'"
-| "iter (Suc n) b S s s' \<longleftrightarrow> s \<in> b \<and> (\<exists>s''. S s s'' \<and> iter n b S s'' s')"
+ where
+ "iter 0 b S s s' \<longleftrightarrow> s \<notin> b \<and> s = s'"
+ | "iter (Suc n) b S s s' \<longleftrightarrow> s \<in> b \<and> (\<exists>s''. S s s'' \<and> iter n b S s'' s')"
primrec Sem :: "'a com \<Rightarrow> 'a sem"
-where
- "Sem (Basic f) s s' \<longleftrightarrow> s' = f s"
-| "Sem (c1; c2) s s' \<longleftrightarrow> (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')"
-| "Sem (Cond b c1 c2) s s' \<longleftrightarrow>
- (if s \<in> b then Sem c1 s s' else Sem c2 s s')"
-| "Sem (While b x c) s s' \<longleftrightarrow> (\<exists>n. iter n b (Sem c) s s')"
+ where
+ "Sem (Basic f) s s' \<longleftrightarrow> s' = f s"
+ | "Sem (c1; c2) s s' \<longleftrightarrow> (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')"
+ | "Sem (Cond b c1 c2) s s' \<longleftrightarrow> (if s \<in> b then Sem c1 s s' else Sem c2 s s')"
+ | "Sem (While b x c) s s' \<longleftrightarrow> (\<exists>n. iter n b (Sem c) s s')"
-definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
- ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
+definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" ("(3\<turnstile> _/ (2_)/ _)" [100, 55, 100] 50)
where "\<turnstile> P c Q \<longleftrightarrow> (\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> P \<longrightarrow> s' \<in> Q)"
-lemma ValidI [intro?]:
- "(\<And>s s'. Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q) \<Longrightarrow> \<turnstile> P c Q"
+lemma ValidI [intro?]: "(\<And>s s'. Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q) \<Longrightarrow> \<turnstile> P c Q"
by (simp add: Valid_def)
-lemma ValidD [dest?]:
- "\<turnstile> P c Q \<Longrightarrow> Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q"
+lemma ValidD [dest?]: "\<turnstile> P c Q \<Longrightarrow> Sem c s s' \<Longrightarrow> s \<in> P \<Longrightarrow> s' \<in> Q"
by (simp add: Valid_def)
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy Tue Aug 02 18:58:49 2016 +0200
@@ -1,7 +1,7 @@
section \<open>Using Hoare Logic\<close>
theory Hoare_Ex
-imports Hoare
+ imports Hoare
begin
subsection \<open>State spaces\<close>
@@ -276,11 +276,11 @@
type_synonym 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>"
primrec timeit :: "'a time com \<Rightarrow> 'a time com"
-where
- "timeit (Basic f) = (Basic f; Basic(\<lambda>s. s\<lparr>time := Suc (time s)\<rparr>))"
-| "timeit (c1; c2) = (timeit c1; timeit c2)"
-| "timeit (Cond b c1 c2) = Cond b (timeit c1) (timeit c2)"
-| "timeit (While b iv c) = While b iv (timeit c)"
+ where
+ "timeit (Basic f) = (Basic f; Basic(\<lambda>s. s\<lparr>time := Suc (time s)\<rparr>))"
+ | "timeit (c1; c2) = (timeit c1; timeit c2)"
+ | "timeit (Cond b c1 c2) = Cond b (timeit c1) (timeit c2)"
+ | "timeit (While b iv c) = While b iv (timeit c)"
record tvars = tstate +
I :: nat
--- a/src/HOL/Isar_Examples/Knaster_Tarski.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Knaster_Tarski.thy Tue Aug 02 18:58:49 2016 +0200
@@ -7,7 +7,7 @@
section \<open>Textbook-style reasoning: the Knaster-Tarski Theorem\<close>
theory Knaster_Tarski
-imports Main "~~/src/HOL/Library/Lattice_Syntax"
+ imports Main "~~/src/HOL/Library/Lattice_Syntax"
begin
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Tue Aug 02 18:58:49 2016 +0200
@@ -6,7 +6,7 @@
section \<open>The Mutilated Checker Board Problem\<close>
theory Mutilated_Checkerboard
-imports Main
+ imports Main
begin
text \<open>
@@ -16,11 +16,10 @@
subsection \<open>Tilings\<close>
-inductive_set tiling :: "'a set set \<Rightarrow> 'a set set"
- for A :: "'a set set"
-where
- empty: "{} \<in> tiling A"
-| Un: "a \<union> t \<in> tiling A" if "a \<in> A" and "t \<in> tiling A" and "a \<subseteq> - t"
+inductive_set tiling :: "'a set set \<Rightarrow> 'a set set" for A :: "'a set set"
+ where
+ empty: "{} \<in> tiling A"
+ | Un: "a \<union> t \<in> tiling A" if "a \<in> A" and "t \<in> tiling A" and "a \<subseteq> - t"
text \<open>The union of two disjoint tilings is a tiling.\<close>
@@ -114,9 +113,9 @@
subsection \<open>Dominoes\<close>
inductive_set domino :: "(nat \<times> nat) set set"
-where
- horiz: "{(i, j), (i, j + 1)} \<in> domino"
-| vertl: "{(i, j), (i + 1, j)} \<in> domino"
+ where
+ horiz: "{(i, j), (i, j + 1)} \<in> domino"
+ | vertl: "{(i, j), (i + 1, j)} \<in> domino"
lemma dominoes_tile_row:
"{i} \<times> below (2 * n) \<in> tiling domino"
@@ -242,10 +241,8 @@
subsection \<open>Main theorem\<close>
definition mutilated_board :: "nat \<Rightarrow> nat \<Rightarrow> (nat \<times> nat) set"
- where
- "mutilated_board m n =
- below (2 * (m + 1)) \<times> below (2 * (n + 1))
- - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"
+ where "mutilated_board m n =
+ below (2 * (m + 1)) \<times> below (2 * (n + 1)) - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"
theorem mutil_not_tiling: "mutilated_board m n \<notin> tiling domino"
proof (unfold mutilated_board_def)
--- a/src/HOL/Isar_Examples/Peirce.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Peirce.thy Tue Aug 02 18:58:49 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Peirce's Law\<close>
theory Peirce
-imports Main
+ imports Main
begin
text \<open>
--- a/src/HOL/Isar_Examples/Puzzle.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Puzzle.thy Tue Aug 02 18:58:49 2016 +0200
@@ -1,7 +1,7 @@
section \<open>An old chestnut\<close>
theory Puzzle
-imports Main
+ imports Main
begin
text_raw \<open>\<^footnote>\<open>A question from ``Bundeswettbewerb Mathematik''. Original
--- a/src/HOL/Isar_Examples/Schroeder_Bernstein.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Schroeder_Bernstein.thy Tue Aug 02 18:58:49 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Schröder-Bernstein Theorem\<close>
theory Schroeder_Bernstein
-imports Main
+ imports Main
begin
text \<open>
--- a/src/HOL/Isar_Examples/Structured_Statements.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Structured_Statements.thy Tue Aug 02 18:58:49 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Structured statements within Isar proofs\<close>
theory Structured_Statements
-imports Main
+ imports Main
begin
subsection \<open>Introduction steps\<close>
--- a/src/HOL/Isar_Examples/Summation.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Isar_Examples/Summation.thy Tue Aug 02 18:58:49 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Summing natural numbers\<close>
theory Summation
-imports Main
+ imports Main
begin
text \<open>
--- a/src/HOL/Library/Simps_Case_Conv.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Library/Simps_Case_Conv.thy Tue Aug 02 18:58:49 2016 +0200
@@ -5,8 +5,10 @@
theory Simps_Case_Conv
imports Main
keywords
- "simps_of_case" :: thy_decl == "" and
- "case_of_simps" :: thy_decl
+ "simps_of_case" "case_of_simps" :: thy_decl
+abbrevs
+ "simps_of_case" = ""
+ "case_of_simps" = ""
begin
ML_file "simps_case_conv.ML"
--- a/src/HOL/Nonstandard_Analysis/HLim.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/HLim.thy Tue Aug 02 18:58:49 2016 +0200
@@ -6,7 +6,8 @@
section\<open>Limits and Continuity (Nonstandard)\<close>
theory HLim
-imports Star
+ imports Star
+ abbrevs "--->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S"
begin
text\<open>Nonstandard Definitions\<close>
--- a/src/HOL/Nonstandard_Analysis/HSEQ.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/HSEQ.thy Tue Aug 02 18:58:49 2016 +0200
@@ -11,7 +11,8 @@
section \<open>Sequences and Convergence (Nonstandard)\<close>
theory HSEQ
-imports Limits NatStar
+ imports Limits NatStar
+ abbrevs "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
begin
definition
--- a/src/Pure/General/completion.scala Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/General/completion.scala Tue Aug 02 18:58:49 2016 +0200
@@ -330,7 +330,7 @@
private val caret_indicator = '\u0007'
private val antiquote = "@{"
- private val default_abbrs =
+ private val default_abbrevs =
List("@{" -> "@{\u0007}",
"`" -> "\\<close>",
"`" -> "\\<open>",
@@ -340,11 +340,11 @@
"\"" -> "\\<open>\u0007\\<close>")
private def default_frequency(name: String): Option[Int] =
- default_abbrs.iterator.map(_._2).zipWithIndex.find(_._1 == name).map(_._2)
+ default_abbrevs.iterator.map(_._2).zipWithIndex.find(_._1 == name).map(_._2)
}
final class Completion private(
- protected val keywords: Map[String, Boolean] = Map.empty,
+ protected val keywords: Set[String] = Set.empty,
protected val words_lex: Scan.Lexicon = Scan.Lexicon.empty,
protected val words_map: Multi_Map[String, String] = Multi_Map.empty,
protected val abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
@@ -363,8 +363,7 @@
if (this eq other) this
else if (is_empty) other
else {
- val keywords1 =
- (keywords /: other.keywords) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
+ val keywords1 = (keywords /: other.keywords) { case (ks, k) => if (ks(k)) ks else ks + k }
val words_lex1 = words_lex ++ other.words_lex
val words_map1 = words_map ++ other.words_map
val abbrevs_lex1 = abbrevs_lex ++ other.abbrevs_lex
@@ -376,48 +375,52 @@
/* keywords */
private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name)
- private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords.isDefinedAt(name)
+ private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords(name)
private def is_keyword_template(name: String, template: Boolean): Boolean =
- is_keyword(name) && keywords(name) == template
+ is_keyword(name) && (words_map.getOrElse(name, name) != name) == template
- def + (keyword: String, template: String): Completion =
- new Completion(
- keywords + (keyword -> (keyword != template)),
- words_lex + keyword,
- words_map + (keyword -> template),
- abbrevs_lex,
- abbrevs_map)
-
- def + (keyword: String): Completion = this + (keyword, keyword)
+ def add_keyword(keyword: String): Completion =
+ new Completion(keywords + keyword, words_lex, words_map, abbrevs_lex, abbrevs_map)
- /* load symbols and abbrevs */
+ /* symbols and abbrevs */
- private def load(): Completion =
+ def add_symbols(): Completion =
{
- val abbrevs = Completion.load_abbrevs()
-
val words =
(for ((sym, _) <- Symbol.names.toList) yield (sym, sym)) :::
- (for ((sym, name) <- Symbol.names.toList) yield ("\\" + name, sym)) :::
- (for ((abbr, text) <- abbrevs if Completion.Word_Parsers.is_word(abbr)) yield (abbr, text))
-
- val non_word_abbrs =
- (for ((abbr, text) <- abbrevs if !Completion.Word_Parsers.is_word(abbr))
- yield (abbr, text)).toList
-
- val abbrs =
- for ((abbr, text) <- non_word_abbrs ::: Completion.default_abbrs)
- yield (abbr.reverse, (abbr, text))
+ (for ((sym, name) <- Symbol.names.toList) yield ("\\" + name, sym))
new Completion(
keywords,
words_lex ++ words.map(_._1),
words_map ++ words,
- abbrevs_lex ++ abbrs.map(_._1),
- abbrevs_map ++ abbrs)
+ abbrevs_lex,
+ abbrevs_map)
}
+ def add_abbrevs(abbrevs: List[(String, String)]): Completion =
+ if (abbrevs.isEmpty) this
+ else {
+ val words =
+ for ((abbr, text) <- abbrevs if text != "" && Completion.Word_Parsers.is_word(abbr))
+ yield (abbr, text)
+ val abbrs =
+ for ((abbr, text) <- abbrevs if text != "" && !Completion.Word_Parsers.is_word(abbr))
+ yield (abbr.reverse, (abbr, text))
+ val remove = (for ((abbr, "") <- abbrevs.iterator) yield abbr).toSet
+
+ new Completion(
+ keywords,
+ words_lex ++ words.map(_._1) -- remove,
+ words_map ++ words -- remove,
+ abbrevs_lex ++ abbrs.map(_._1) -- remove,
+ abbrevs_map ++ abbrs -- remove)
+ }
+
+ private def load(): Completion =
+ add_symbols().add_abbrevs(Completion.load_abbrevs() ::: Completion.default_abbrevs)
+
/* complete */
@@ -444,7 +447,7 @@
case (abbr, _) :: _ =>
val ok =
if (abbr == Completion.antiquote) language_context.antiquotes
- else language_context.symbols || Completion.default_abbrs.exists(_._1 == abbr)
+ else language_context.symbols || Completion.default_abbrevs.exists(_._1 == abbr)
if (ok) Some((abbr, abbrevs))
else None
}
--- a/src/Pure/General/multi_map.scala Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/General/multi_map.scala Tue Aug 02 18:58:49 2016 +0200
@@ -8,6 +8,7 @@
package isabelle
+import scala.collection.GenTraversableOnce
import scala.collection.generic.{ImmutableMapFactory, CanBuildFrom}
@@ -75,6 +76,9 @@
def + [B1 >: B](p: (A, B1)): Multi_Map[A, B1] = insert(p._1, p._2)
+ override def ++ [B1 >: B](entries: GenTraversableOnce[(A, B1)]): Multi_Map[A, B1] =
+ (this.asInstanceOf[Multi_Map[A, B1]] /: entries)(_ + _)
+
def - (a: A): Multi_Map[A, B] =
if (rep.isDefinedAt(a)) new Multi_Map(rep - a) else this
}
--- a/src/Pure/General/scan.scala Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/General/scan.scala Tue Aug 02 18:58:49 2016 +0200
@@ -8,7 +8,7 @@
import scala.annotation.tailrec
-import scala.collection.{IndexedSeq, TraversableOnce}
+import scala.collection.{IndexedSeq, Traversable, TraversableOnce}
import scala.collection.immutable.PagedSeq
import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
import scala.util.parsing.combinator.RegexParsers
@@ -393,6 +393,11 @@
else if (is_empty) other
else this ++ other.raw_iterator
+ def -- (remove: Traversable[String]): Lexicon =
+ if (remove.exists(contains(_)))
+ Lexicon.empty ++ iterator.filterNot(a => remove.exists(b => a == b))
+ else this
+
/* scan */
--- a/src/Pure/Isar/keyword.scala Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/Isar/keyword.scala Tue Aug 02 18:58:49 2016 +0200
@@ -163,7 +163,7 @@
def add_keywords(header: Thy_Header.Keywords): Keywords =
(this /: header) {
- case (keywords, (name, ((kind, exts), _), _)) =>
+ case (keywords, (name, ((kind, exts), _))) =>
if (kind == "") keywords + Symbol.decode(name) + Symbol.encode(name)
else keywords + (Symbol.decode(name), kind, exts) + (Symbol.encode(name), kind, exts)
}
--- a/src/Pure/Isar/outer_syntax.scala Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Tue Aug 02 18:58:49 2016 +0200
@@ -76,7 +76,7 @@
val keywords: Keyword.Keywords = Keyword.Keywords.empty,
val completion: Completion = Completion.empty,
val language_context: Completion.Language_Context = Completion.Language_Context.outer,
- val has_tokens: Boolean = true) extends Prover.Syntax
+ val has_tokens: Boolean = true)
{
/** syntax content **/
@@ -85,30 +85,41 @@
/* add keywords */
- def + (name: String, kind: String = "", tags: List[String] = Nil, replace: Option[String] = None)
- : Outer_Syntax =
+ def + (name: String, kind: String = "", tags: List[String] = Nil): Outer_Syntax =
{
val keywords1 = keywords + (name, kind, tags)
val completion1 =
- if (replace == Some("")) completion
- else if (replace.isEmpty && Keyword.theory_block.contains(kind))
- completion + (name, name + "\nbegin\n\u0007\nend") + (name, name)
- else completion + (name, replace getOrElse name)
+ completion.add_keyword(name).add_abbrevs(
+ if (Keyword.theory_block.contains(kind))
+ List((name, name + "\nbegin\n\u0007\nend"), (name, name))
+ else List((name, name)))
new Outer_Syntax(keywords1, completion1, language_context, true)
}
def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
(this /: keywords) {
- case (syntax, (name, ((kind, tags), _), replace)) =>
- syntax +
- (Symbol.decode(name), kind, tags, replace) +
- (Symbol.encode(name), kind, tags, replace)
+ case (syntax, (name, ((kind, tags), _))) =>
+ syntax + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags)
+ }
+
+ def add_abbrevs(abbrevs: Thy_Header.Abbrevs): Outer_Syntax =
+ if (abbrevs.isEmpty) this
+ else {
+ val completion1 =
+ completion.add_abbrevs(
+ (for ((a, b) <- abbrevs) yield {
+ val a1 = Symbol.decode(a)
+ val a2 = Symbol.encode(a)
+ val b1 = Symbol.decode(b)
+ List((a1, b1), (a2, b1))
+ }).flatten)
+ new Outer_Syntax(keywords, completion1, language_context, has_tokens)
}
/* merge */
- def ++ (other: Prover.Syntax): Prover.Syntax =
+ def ++ (other: Outer_Syntax): Outer_Syntax =
if (this eq other) this
else {
val keywords1 = keywords ++ other.asInstanceOf[Outer_Syntax].keywords
--- a/src/Pure/PIDE/command.scala Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/PIDE/command.scala Tue Aug 02 18:58:49 2016 +0200
@@ -326,7 +326,7 @@
}
else None
- def span_files(syntax: Prover.Syntax, span: Command_Span.Span): (List[String], Int) =
+ def span_files(syntax: Outer_Syntax, span: Command_Span.Span): (List[String], Int) =
syntax.load_command(span.name) match {
case Some(exts) =>
find_file(clean_tokens(span.content)) match {
@@ -340,7 +340,7 @@
def blobs_info(
resources: Resources,
- syntax: Prover.Syntax,
+ syntax: Outer_Syntax,
get_blob: Document.Node.Name => Option[Document.Blob],
can_import: Document.Node.Name => Boolean,
node_name: Document.Node.Name,
--- a/src/Pure/PIDE/document.scala Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/PIDE/document.scala Tue Aug 02 18:58:49 2016 +0200
@@ -83,6 +83,7 @@
sealed case class Header(
imports: List[(Name, Position.T)] = Nil,
keywords: Thy_Header.Keywords = Nil,
+ abbrevs: Thy_Header.Abbrevs = Nil,
errors: List[String] = Nil)
{
def error(msg: String): Header = copy(errors = errors ::: List(msg))
@@ -244,7 +245,7 @@
final class Node private(
val get_blob: Option[Document.Blob] = None,
val header: Node.Header = Node.no_header,
- val syntax: Option[Prover.Syntax] = None,
+ val syntax: Option[Outer_Syntax] = None,
val text_perspective: Text.Perspective = Text.Perspective.empty,
val perspective: Node.Perspective_Command = Node.no_perspective_command,
_commands: Node.Commands = Node.Commands.empty)
@@ -268,7 +269,7 @@
def update_header(new_header: Node.Header): Node =
new Node(get_blob, new_header, syntax, text_perspective, perspective, _commands)
- def update_syntax(new_syntax: Option[Prover.Syntax]): Node =
+ def update_syntax(new_syntax: Option[Outer_Syntax]): Node =
new Node(get_blob, header, new_syntax, text_perspective, perspective, _commands)
def update_perspective(
--- a/src/Pure/PIDE/protocol.scala Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/PIDE/protocol.scala Tue Aug 02 18:58:49 2016 +0200
@@ -374,13 +374,12 @@
val master_dir = File.standard_url(name.master_dir)
val theory = Long_Name.base_name(name.theory)
val imports = header.imports.map({ case (a, _) => a.node })
- val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
(Nil,
pair(Encode.string, pair(Encode.string, pair(list(Encode.string),
pair(list(pair(Encode.string,
pair(pair(Encode.string, list(Encode.string)), list(Encode.string)))),
list(Encode.string)))))(
- (master_dir, (theory, (imports, (keywords, header.errors)))))) },
+ (master_dir, (theory, (imports, (header.keywords, header.errors)))))) },
{ case Document.Node.Perspective(a, b, c) =>
(bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
list(pair(id, pair(Encode.string, list(Encode.string))))(c.dest)) }))
--- a/src/Pure/PIDE/prover.scala Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/PIDE/prover.scala Tue Aug 02 18:58:49 2016 +0200
@@ -13,18 +13,6 @@
object Prover
{
- /* syntax */
-
- trait Syntax
- {
- def ++ (other: Syntax): Syntax
- def add_keywords(keywords: Thy_Header.Keywords): Syntax
- def parse_spans(input: CharSequence): List[Command_Span.Span]
- def load_command(name: String): Option[List[String]]
- def load_commands_in(text: String): Boolean
- }
-
-
/* underlying system process */
trait System_Process
--- a/src/Pure/PIDE/resources.scala Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/PIDE/resources.scala Tue Aug 02 18:58:49 2016 +0200
@@ -23,7 +23,7 @@
class Resources(
val loaded_theories: Set[String],
val known_theories: Map[String, Document.Node.Name],
- val base_syntax: Prover.Syntax)
+ val base_syntax: Outer_Syntax)
{
/* document node names */
@@ -55,7 +55,7 @@
/* theory files */
- def loaded_files(syntax: Prover.Syntax, text: String): List[String] =
+ def loaded_files(syntax: Outer_Syntax, text: String): List[String] =
if (syntax.load_commands_in(text)) {
val spans = syntax.parse_spans(text)
spans.iterator.map(Command.span_files(syntax, _)._1).flatten.toList
@@ -103,7 +103,7 @@
val imports =
header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) })
- Document.Node.Header(imports, header.keywords)
+ Document.Node.Header(imports, header.keywords, header.abbrevs)
}
catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
}
--- a/src/Pure/PIDE/session.scala Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/PIDE/session.scala Tue Aug 02 18:58:49 2016 +0200
@@ -237,7 +237,7 @@
private val global_state = Synchronized(Document.State.init)
def current_state(): Document.State = global_state.value
- def recent_syntax(name: Document.Node.Name): Prover.Syntax =
+ def recent_syntax(name: Document.Node.Name): Outer_Syntax =
global_state.value.recent_finished.version.get_finished.nodes(name).syntax getOrElse
resources.base_syntax
--- a/src/Pure/Pure.thy Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/Pure.thy Tue Aug 02 18:58:49 2016 +0200
@@ -6,7 +6,7 @@
theory Pure
keywords
- "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
+ "!!" "!" "+" "--" ":" ";" "<" "<=" "==" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
"\<subseteq>" "]" "attach" "binder" "for" "if" "in" "infix" "infixl" "infixr" "is"
"open" "output" "overloaded" "pervasive" "premises" "structure" "unchecked" "when"
and "private" "qualified" :: before_command
@@ -14,7 +14,7 @@
"obtains" "shows" "where" "|" :: quasi_command
and "text" "txt" :: document_body
and "text_raw" :: document_raw
- and "default_sort" :: thy_decl == ""
+ and "default_sort" :: thy_decl
and "typedecl" "type_synonym" "nonterminal" "judgment"
"consts" "syntax" "no_syntax" "translations" "no_translations"
"definition" "abbreviation" "type_notation" "no_type_notation" "notation"
@@ -25,7 +25,7 @@
and "SML_import" "SML_export" :: thy_decl % "ML"
and "ML_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *)
and "ML_val" "ML_command" :: diag % "ML"
- and "simproc_setup" :: thy_decl % "ML" == ""
+ and "simproc_setup" :: thy_decl % "ML"
and "setup" "local_setup" "attribute_setup" "method_setup"
"declaration" "syntax_declaration"
"parse_ast_translation" "parse_translation" "print_translation"
@@ -47,9 +47,9 @@
and "schematic_goal" :: thy_goal
and "notepad" :: thy_decl_block
and "have" :: prf_goal % "proof"
- and "hence" :: prf_goal % "proof" == "then have"
+ and "hence" :: prf_goal % "proof"
and "show" :: prf_asm_goal % "proof"
- and "thus" :: prf_asm_goal % "proof" == "then show"
+ and "thus" :: prf_asm_goal % "proof"
and "then" "from" "with" :: prf_chain % "proof"
and "note" :: prf_decl % "proof"
and "supply" :: prf_script % "proof"
@@ -68,7 +68,7 @@
and "done" :: "qed_script" % "proof"
and "oops" :: qed_global % "proof"
and "defer" "prefer" "apply" :: prf_script % "proof"
- and "apply_end" :: prf_script % "proof" == ""
+ and "apply_end" :: prf_script % "proof"
and "subgoal" :: prf_script_goal % "proof"
and "proof" :: prf_block % "proof"
and "also" "moreover" :: prf_decl % "proof"
@@ -86,11 +86,19 @@
and "display_drafts" "print_state" :: diag
and "welcome" :: diag
and "end" :: thy_end % "theory"
- and "realizers" :: thy_decl == ""
- and "realizability" :: thy_decl == ""
+ and "realizers" :: thy_decl
+ and "realizability" :: thy_decl
and "extract_type" "extract" :: thy_decl
and "find_theorems" "find_consts" :: diag
and "named_theorems" :: thy_decl
+abbrevs
+ "default_sort" = ""
+ "simproc_setup" = ""
+ "hence" = "then have"
+ "thus" = "then show"
+ "apply_end" = ""
+ "realizers" = ""
+ "realizability" = ""
begin
section \<open>Isar commands\<close>
--- a/src/Pure/Thy/thy_header.ML Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/Thy/thy_header.ML Tue Aug 02 18:58:49 2016 +0200
@@ -58,6 +58,7 @@
val theoryN = "theory";
val importsN = "imports";
val keywordsN = "keywords";
+val abbrevsN = "abbrevs";
val beginN = "begin";
val bootstrap_keywords =
@@ -68,11 +69,12 @@
((")", @{here}), Keyword.no_spec),
((",", @{here}), Keyword.no_spec),
(("::", @{here}), Keyword.no_spec),
- (("==", @{here}), Keyword.no_spec),
+ (("=", @{here}), Keyword.no_spec),
(("and", @{here}), Keyword.no_spec),
((beginN, @{here}), Keyword.quasi_command_spec),
((importsN, @{here}), Keyword.quasi_command_spec),
((keywordsN, @{here}), Keyword.quasi_command_spec),
+ ((abbrevsN, @{here}), Keyword.quasi_command_spec),
((chapterN, @{here}), ((Keyword.document_heading, []), [])),
((sectionN, @{here}), ((Keyword.document_heading, []), [])),
((subsectionN, @{here}), ((Keyword.document_heading, []), [])),
@@ -128,14 +130,12 @@
Parse.group (fn () => "outer syntax keyword specification")
(Parse.name -- opt_files -- Parse.tags);
-val keyword_compl =
- Parse.group (fn () => "outer syntax keyword completion") Parse.name;
-
val keyword_decl =
Scan.repeat1 (Parse.position Parse.string) --
- Scan.optional (Parse.$$$ "::" |-- Parse.!!! keyword_spec) Keyword.no_spec --
- Scan.option (Parse.$$$ "==" |-- Parse.!!! keyword_compl)
- >> (fn ((names, spec), _) => map (rpair spec) names);
+ Scan.optional (Parse.$$$ "::" |-- Parse.!!! keyword_spec) Keyword.no_spec
+ >> (fn (names, spec) => map (rpair spec) names);
+
+val abbrevs = Scan.repeat1 (Parse.text -- (Parse.$$$ "=" |-- Parse.!!! Parse.text));
val keyword_decls = Parse.and_list1 keyword_decl >> flat;
@@ -145,7 +145,8 @@
Parse.position Parse.theory_name :|-- (fn (name, pos) =>
imports name --
Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --|
- Parse.$$$ beginN >> (fn (imports, keywords) => make (name, pos) imports keywords));
+ (Scan.optional (Parse.$$$ abbrevsN |-- Parse.!!! abbrevs) [] -- Parse.$$$ beginN)
+ >> (fn (imports, keywords) => make (name, pos) imports keywords));
end;
--- a/src/Pure/Thy/thy_header.scala Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/Thy/thy_header.scala Tue Aug 02 18:58:49 2016 +0200
@@ -17,7 +17,8 @@
{
/* bootstrap keywords */
- type Keywords = List[(String, Keyword.Spec, Option[String])]
+ type Keywords = List[(String, Keyword.Spec)]
+ type Abbrevs = List[(String, String)]
val CHAPTER = "chapter"
val SECTION = "section"
@@ -32,32 +33,34 @@
val THEORY = "theory"
val IMPORTS = "imports"
val KEYWORDS = "keywords"
+ val ABBREVS = "abbrevs"
val AND = "and"
val BEGIN = "begin"
private val bootstrap_header: Keywords =
List(
- ("%", Keyword.no_spec, None),
- ("(", Keyword.no_spec, None),
- (")", Keyword.no_spec, None),
- (",", Keyword.no_spec, None),
- ("::", Keyword.no_spec, None),
- ("==", Keyword.no_spec, None),
- (AND, Keyword.no_spec, None),
- (BEGIN, Keyword.quasi_command_spec, None),
- (IMPORTS, Keyword.quasi_command_spec, None),
- (KEYWORDS, Keyword.quasi_command_spec, None),
- (CHAPTER, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
- (SECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
- (SUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
- (SUBSUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
- (PARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
- (SUBPARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
- (TEXT, (((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
- (TXT, (((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
- (TEXT_RAW, (((Keyword.DOCUMENT_RAW, Nil), Nil)), None),
- (THEORY, ((Keyword.THY_BEGIN, Nil), List("theory")), None),
- ("ML", ((Keyword.THY_DECL, Nil), List("ML")), None))
+ ("%", Keyword.no_spec),
+ ("(", Keyword.no_spec),
+ (")", Keyword.no_spec),
+ (",", Keyword.no_spec),
+ ("::", Keyword.no_spec),
+ ("=", Keyword.no_spec),
+ (AND, Keyword.no_spec),
+ (BEGIN, Keyword.quasi_command_spec),
+ (IMPORTS, Keyword.quasi_command_spec),
+ (KEYWORDS, Keyword.quasi_command_spec),
+ (ABBREVS, Keyword.quasi_command_spec),
+ (CHAPTER, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
+ (SECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
+ (SUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
+ (SUBSUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
+ (PARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
+ (SUBPARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
+ (TEXT, (((Keyword.DOCUMENT_BODY, Nil), Nil))),
+ (TXT, (((Keyword.DOCUMENT_BODY, Nil), Nil))),
+ (TEXT_RAW, (((Keyword.DOCUMENT_RAW, Nil), Nil))),
+ (THEORY, ((Keyword.THY_BEGIN, Nil), List("theory"))),
+ ("ML", ((Keyword.THY_DECL, Nil), List("ML"))))
private val bootstrap_keywords =
Keyword.Keywords.empty.add_keywords(bootstrap_header)
@@ -106,22 +109,26 @@
val keyword_decl =
rep1(string) ~
- opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
- opt($$$("==") ~! name ^^ { case _ ~ x => x }) ^^
- { case xs ~ y ~ z => xs.map((_, y.getOrElse(Keyword.no_spec), z)) }
+ opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^
+ { case xs ~ y => xs.map((_, y.getOrElse(Keyword.no_spec))) }
val keyword_decls =
keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
{ case xs ~ yss => (xs :: yss).flatten }
+ val abbrevs =
+ rep1(text ~ ($$$("=") ~! text) ^^ { case a ~ (_ ~ b) => (a, b) })
+
val args =
position(theory_name) ~
(opt($$$(IMPORTS) ~! rep1(position(theory_name))) ^^
{ case None => Nil case Some(_ ~ xs) => xs }) ~
(opt($$$(KEYWORDS) ~! keyword_decls) ^^
{ case None => Nil case Some(_ ~ xs) => xs }) ~
+ (opt($$$(ABBREVS) ~! abbrevs) ^^
+ { case None => Nil case Some(_ ~ xs) => xs }) ~
$$$(BEGIN) ^^
- { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
+ { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) }
val heading =
(command(CHAPTER) |
@@ -171,13 +178,15 @@
sealed case class Thy_Header(
name: (String, Position.T),
imports: List[(String, Position.T)],
- keywords: Thy_Header.Keywords)
+ keywords: Thy_Header.Keywords,
+ abbrevs: Thy_Header.Abbrevs)
{
def decode_symbols: Thy_Header =
{
val f = Symbol.decode _
- Thy_Header((f(name._1), name._2), imports.map({ case (a, b) => (f(a), b) }),
- keywords.map({ case (a, ((x, y), z), c) =>
- (f(a), ((f(x), y.map(f)), z.map(f)), c.map(f)) }))
+ Thy_Header((f(name._1), name._2),
+ imports.map({ case (a, b) => (f(a), b) }),
+ keywords.map({ case (a, ((b, c), d)) => (f(a), ((f(b), c.map(f)), d.map(f))) }),
+ abbrevs.map({ case (a, b) => (f(a), f(b)) }))
}
}
--- a/src/Pure/Thy/thy_info.scala Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/Thy/thy_info.scala Tue Aug 02 18:58:49 2016 +0200
@@ -38,24 +38,26 @@
object Dependencies
{
- val empty = new Dependencies(Nil, Nil, Set.empty, Multi_Map.empty, Multi_Map.empty)
+ val empty = new Dependencies(Nil, Nil, Nil, Set.empty, Multi_Map.empty, Multi_Map.empty)
}
final class Dependencies private(
rev_deps: List[Thy_Info.Dep],
val keywords: Thy_Header.Keywords,
+ val abbrevs: Thy_Header.Abbrevs,
val seen: Set[Document.Node.Name],
val seen_names: Multi_Map[String, Document.Node.Name],
val seen_positions: Multi_Map[String, Position.T])
{
def :: (dep: Thy_Info.Dep): Dependencies =
- new Dependencies(dep :: rev_deps, dep.header.keywords ::: keywords,
+ new Dependencies(
+ dep :: rev_deps, dep.header.keywords ::: keywords, dep.header.abbrevs ::: abbrevs,
seen, seen_names, seen_positions)
def + (thy: (Document.Node.Name, Position.T)): Dependencies =
{
val (name, pos) = thy
- new Dependencies(rev_deps, keywords,
+ new Dependencies(rev_deps, keywords, abbrevs,
seen + name,
seen_names + (name.theory -> name),
seen_positions + (name.theory -> pos))
@@ -80,7 +82,8 @@
header_errors ::: import_errors
}
- lazy val syntax: Prover.Syntax = resources.base_syntax.add_keywords(keywords)
+ lazy val syntax: Outer_Syntax =
+ resources.base_syntax.add_keywords(keywords).add_abbrevs(abbrevs)
def loaded_theories: Set[String] =
(resources.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
--- a/src/Pure/Thy/thy_syntax.scala Tue Aug 02 13:13:15 2016 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Tue Aug 02 18:58:49 2016 +0200
@@ -84,6 +84,7 @@
val node1 = node.update_header(header)
if (node.header.imports.map(_._1) != node1.header.imports.map(_._1) ||
node.header.keywords != node1.header.keywords ||
+ node.header.abbrevs != node1.header.abbrevs ||
node.header.errors != node1.header.errors) syntax_changed0 += name
nodes += (name -> node1)
doc_edits += (name -> Document.Node.Deps(header))
@@ -100,7 +101,8 @@
else {
val header = node.header
val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
- Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(header.keywords))
+ Some((resources.base_syntax /: imports_syntax)(_ ++ _)
+ .add_keywords(header.keywords).add_abbrevs(header.abbrevs))
}
nodes += (name -> node.update_syntax(syntax))
}
@@ -156,7 +158,7 @@
private def reparse_spans(
resources: Resources,
- syntax: Prover.Syntax,
+ syntax: Outer_Syntax,
get_blob: Document.Node.Name => Option[Document.Blob],
can_import: Document.Node.Name => Boolean,
node_name: Document.Node.Name,
@@ -202,7 +204,7 @@
private def text_edit(
resources: Resources,
- syntax: Prover.Syntax,
+ syntax: Outer_Syntax,
get_blob: Document.Node.Name => Option[Document.Blob],
can_import: Document.Node.Name => Boolean,
reparse_limit: Int,