From 067e33104e2775fd20ce5e63c48e7be659fd8bde Mon Sep 17 00:00:00 2001 From: Patrick Massot Date: Mon, 4 Dec 2023 09:48:19 -0500 Subject: [PATCH] =?UTF-8?q?Update=20lun.=2004=20d=C3=A9c.=202023=2009:48:1?= =?UTF-8?q?9=20EST?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .buildinfo | 2 +- C01_Introduction.html | 22 +- C02_Basics.html | 40 +- C03_Logic.html | 49 +- C04_Sets_and_Functions.html | 64 +- C05_Elementary_Number_Theory.html | 30 +- C06_Structures.html | 30 +- C07_Hierarchies.html | 36 +- C08_Groups_and_Rings.html | 234 +++--- C09_Topology.html | 78 +- C10_Differential_Calculus.html | 46 +- C11_Integration_and_Measure_Theory.html | 28 +- .../_sphinx_javascript_frameworks_compat.js | 134 --- _static/basic.css | 40 +- _static/doctools.js | 450 +++++----- _static/documentation_options.js | 6 +- _static/{jquery-3.6.0.js => jquery-3.5.1.js} | 227 +++-- _static/jquery.js | 4 +- _static/language_data.js | 100 ++- _static/searchtools.js | 788 +++++++++--------- genindex.html | 1 - index.html | 10 +- mathematics_in_lean.pdf | Bin 977586 -> 976534 bytes search.html | 1 - searchindex.js | 2 +- 25 files changed, 1181 insertions(+), 1241 deletions(-) delete mode 100644 _static/_sphinx_javascript_frameworks_compat.js rename _static/{jquery-3.6.0.js => jquery-3.5.1.js} (98%) diff --git a/.buildinfo b/.buildinfo index 7a6f75aa..d1d64cb6 100644 --- a/.buildinfo +++ b/.buildinfo @@ -1,4 +1,4 @@ # Sphinx build info version 1 # This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done. -config: 9821478498fa33697c987b601aae688f +config: 803b947a09f3db5a52c6c529e3761a53 tags: 645f666f9bcd5a90fca523b33c5a78b7 diff --git a/C01_Introduction.html b/C01_Introduction.html index 6a393cbb..0012d9b2 100644 --- a/C01_Introduction.html +++ b/C01_Introduction.html @@ -1,8 +1,7 @@ - - + 1. Introduction — Mathematics in Lean 0.1 documentation @@ -16,7 +15,6 @@ - @@ -85,10 +83,10 @@
-
-

1. Introduction

-
-

1.1. Getting Started

+
+

1. Introduction

+
+

1.1. Getting Started

The goal of this book is to teach you to formalize mathematics using the Lean 4 interactive proof assistant. It assumes that you know some mathematics, but it does not require much. @@ -173,9 +171,9 @@

1.1. Getting Startedsolutions folder associated with each section.

-

-
-

1.2. Overview

+
+
+

1.2. Overview

Put simply, Lean is a tool for building complex expressions in a formal language known as dependent type theory.

Every expression has a type, and you can use the #check command to @@ -347,8 +345,8 @@

1.2. Overview - - +

+
diff --git a/C02_Basics.html b/C02_Basics.html index bd18f2d8..88f4e16e 100644 --- a/C02_Basics.html +++ b/C02_Basics.html @@ -1,8 +1,7 @@ - - + 2. Basics — Mathematics in Lean 0.1 documentation @@ -16,7 +15,6 @@ - @@ -89,14 +87,14 @@
-
-

2. Basics

+
+

2. Basics

This chapter is designed to introduce you to the nuts and bolts of mathematical reasoning in Lean: calculating, applying lemmas and theorems, and reasoning about generic structures.

-
-

2.1. Calculating

+
+

2.1. Calculating

We generally learn to carry out mathematical calculations without thinking of them as proofs. But when we justify each step in a calculation, @@ -385,9 +383,9 @@

2.1. Calculatingrw [add_mul]

-
-
-

2.2. Proving Identities in Algebraic Structures

+
+
+

2.2. Proving Identities in Algebraic Structures

Mathematically, a ring consists of a collection of objects, \(R\), operations \(+\) \(\times\), and constants \(0\) and \(1\), and an operation \(x \mapsto -x\) such that:

@@ -705,9 +703,9 @@

2.1. Calculatingnoncomm_ring and ring. This is partly for historical reasons, but also for the convenience of using a shorter name for the tactic that deals with commutative rings, since it is used more often.

- -
-

2.3. Using Theorems and Lemmas

+

+
+

2.3. Using Theorems and Lemmas

Rewriting is great for proving equations, but what about other sorts of theorems? For example, how can we prove an inequality, @@ -974,9 +972,9 @@

2.1. Calculating

If you managed to solve this, congratulations! You are well on your way to becoming a master formalizer.

- -
-

2.4. More examples using apply and rw

+

+
+

2.4. More examples using apply and rw

The min function on the real numbers is uniquely characterized by the following three facts:

#check (min_le_left a b : min a b ≤ a)
@@ -1176,9 +1174,9 @@ 
2.1. Calculating_root_.dvd_antisymm to specify the generic one;
 either one will work.

-
-

-
2.5. Proving Facts about Algebraic Structures

+
+
+

2.5. Proving Facts about Algebraic Structures

In Section 2.2, we saw that many common identities governing the real numbers hold in more general classes of algebraic structures, @@ -1391,8 +1389,8 @@

2.1. Calculating

We recommend making use of the theorem nonneg_of_mul_nonneg_left. As you may have guessed, this theorem is called dist_nonneg in Mathlib.

- - +

+
diff --git a/C03_Logic.html b/C03_Logic.html index b2b46d08..3b48b932 100644 --- a/C03_Logic.html +++ b/C03_Logic.html @@ -1,8 +1,7 @@ - - + 3. Logic — Mathematics in Lean 0.1 documentation @@ -16,7 +15,6 @@ - @@ -90,8 +88,8 @@
-
-

3. Logic

+
+

3. Logic

In the last chapter, we dealt with equations, inequalities, and basic mathematical statements like “\(x\) divides \(y\).” @@ -101,8 +99,8 @@ “if … then,” “every,” and “some.” In this chapter, we show you how to work with statements that are built up in this way.

-
-

3.1. Implication and the Universal Quantifier

+
+

3.1. Implication and the Universal Quantifier

Consider the statement after the #check:

#check ∀ x : ℝ, 0 ≤ x → |x| = x
@@ -490,9 +488,9 @@ sorry
-
-
-

3.2. The Existential Quantifier

+
+
+

3.2. The Existential Quantifier

The existential quantifier, which can be entered as \ex in VS Code, is used to represent the phrase “there exists.” The formal expression ∃ x : ℝ, 2 < x ∧ x < 3 in Lean says @@ -811,9 +809,9 @@ sorry

- -
-

3.3. Negation

+
+
+

3.3. Negation

The symbol ¬ is meant to express negation, so ¬ x < y says that x is not less than y, ¬ x = y (or, equivalently, x ≠ y) says that @@ -1076,9 +1074,9 @@ by finding a contradiction in the hypotheses, such as a pair of the form h : P and h' : ¬ P. Of course, in this example, linarith also works.

- -
-

3.4. Conjunction and Iff

+
+
+

3.4. Conjunction and Iff

You have already seen that the conjunction symbol, ∧, is used to express “and.” The constructor tactic allows you to prove a statement of @@ -1131,8 +1129,7 @@ fun ⟨h₀, h₁⟩ h' ↦ h₁ (le_antisymm h₀ h')

-

In analogy to the obtain tactic, which we used with the existential -quantifier, there is also a pattern-matching have:

+

In analogy to the obtain tactic, there is also a pattern-matching have:

example {x y : ℝ} (h : x ≤ y ∧ x ≠ y) : ¬y ≤ x := by
   have ⟨h₀, h₁⟩ := h
   contrapose! h₁
@@ -1336,9 +1333,9 @@
   sorry
- -
-

3.5. Disjunction

+ +
+

3.5. Disjunction

The canonical way to prove a disjunction A ∨ B is to prove A or to prove B. The left tactic chooses A, @@ -1579,9 +1576,9 @@ sorry

-
-
-

3.6. Sequences and Convergence

+ +
+

3.6. Sequences and Convergence

We now have enough skills at our disposal to do some real mathematics. In Lean, we can represent a sequence \(s_0, s_1, s_2, \ldots\) of real numbers as a function s : ℕ → ℝ. @@ -1816,8 +1813,8 @@ not only abstracting away particular features of the domain and codomain, but also abstracting over different types of convergence.

-
- + + diff --git a/C04_Sets_and_Functions.html b/C04_Sets_and_Functions.html index f7b03497..23d59b03 100644 --- a/C04_Sets_and_Functions.html +++ b/C04_Sets_and_Functions.html @@ -1,8 +1,7 @@ - - + 4. Sets and Functions — Mathematics in Lean 0.1 documentation @@ -16,7 +15,6 @@ - @@ -87,8 +85,8 @@
-
-

4. Sets and Functions

+
+

4. Sets and Functions

The vocabulary of sets, relations, and functions provides a uniform language for carrying out constructions in all the branches of mathematics. @@ -120,8 +118,8 @@ from real numbers to real numbers. The distinction between types and sets takes some getting used to, but this chapter will take you through the essentials.

-
-

4.1. Sets

+
+

4.1. Sets

If α is any type, the type Set α consists of sets of elements of α. This type supports the usual set-theoretic operations and relations. @@ -557,9 +555,9 @@

In the library, these identities are called sUnion_eq_biUnion and sInter_eq_biInter.

-
-
-

4.2. Functions

+
+
+

4.2. Functions

If f : α → β is a function and p is a set of elements of type β, the library defines preimage f p, written f ⁻¹' p, @@ -689,39 +687,19 @@ 

variable {I : Type*} (A : I → Set α) (B : I → Set β)
 
 example : (f '' ⋃ i, A i) = ⋃ i, f '' A i := by
-  ext y; simp
-  constructor
-  · rintro ⟨x, ⟨i, xAi⟩, fxeq⟩
-    use i, x
-  rintro ⟨i, x, xAi, fxeq⟩
-  exact ⟨x, ⟨i, xAi⟩, fxeq⟩
+  sorry
 
 example : (f '' ⋂ i, A i) ⊆ ⋂ i, f '' A i := by
-  intro y; simp
-  intro x h fxeq i
-  use x
-  exact ⟨h i, fxeq⟩
+  sorry
 
 example (i : I) (injf : Injective f) : (⋂ i, f '' A i) ⊆ f '' ⋂ i, A i := by
-  intro y; simp
-  intro h
-  rcases h i with ⟨x, xAi, fxeq⟩
-  use x; constructor
-  · intro i'
-    rcases h i' with ⟨x', x'Ai, fx'eq⟩
-    have : f x = f x' := by rw [fxeq, fx'eq]
-    have : x = x' := injf this
-    rw [this]
-    exact x'Ai
-  exact fxeq
+  sorry
 
 example : (f ⁻¹' ⋃ i, B i) = ⋃ i, f ⁻¹' B i := by
-  ext x
-  simp
+  sorry
 
 example : (f ⁻¹' ⋂ i, B i) = ⋂ i, f ⁻¹' B i := by
-  ext x
-  simp
+  sorry

The library defines a predicate InjOn f s to say that @@ -824,7 +802,7 @@ exact Classical.choose_spec h

-

The lines noncomputable theory and open Classical +

The lines noncomputable section and open Classical are needed because we are using classical logic in an essential way. On input y, the function inverse f returns some value of x satisfying f x = y if there is one, @@ -883,9 +861,9 @@ contradiction

- -
-

4.3. The Schröder-Bernstein Theorem

+ +
+

4.3. The Schröder-Bernstein Theorem

We close this chapter with an elementary but nontrivial theorem of set theory. Let \(\alpha\) and \(\beta\) be sets. (In our formalization, they will actually be types.) @@ -1017,11 +995,11 @@ As a result, for every \(x\) in the complement of \(A\), there is a \(y\) such that \(g(y) = x\). (By the injectivity of \(g\), this \(y\) is unique, -but next theorem says only that inv_fun g x returns some y +but next theorem says only that invFun g x returns some y such that g y = x.)

Step through the proof below, make sure you understand what is going on, and fill in the remaining parts. -You will need to use inv_fun_eq at the end. +You will need to use invFun_eq at the end. Notice that rewriting with sb_aux here replaces sb_aux f g 0 with the right-hand side of the corresponding defining equation.

theorem sb_right_inv {x : α} (hx : x ∉ sbSet f g) : g (invFun g x) = x := by
@@ -1144,8 +1122,8 @@
   ⟨sbFun f g, sb_injective f g hf hg, sb_surjective f g hf hg⟩
-
- + + diff --git a/C05_Elementary_Number_Theory.html b/C05_Elementary_Number_Theory.html index 021b81c6..3d267132 100644 --- a/C05_Elementary_Number_Theory.html +++ b/C05_Elementary_Number_Theory.html @@ -1,8 +1,7 @@ - - + 5. Elementary Number Theory — Mathematics in Lean 0.1 documentation @@ -16,7 +15,6 @@ - @@ -87,16 +85,16 @@
-
-

5. Elementary Number Theory

+
+

5. Elementary Number Theory

In this chapter, we show you how to formalize some elementary results in number theory. As we deal with more substantive mathematical content, the proofs will get longer and more involved, building on the skills you have already mastered.

-
-

5.1. Irrational Roots

-

Let’s start with a fact known to the ancient greeks, namely, +

+

5.1. Irrational Roots

+

Let’s start with a fact known to the ancient Greeks, namely, that the square root of 2 is irrational. If we suppose otherwise, we can write \(\sqrt{2} = a / b\) as a fraction @@ -394,9 +392,9 @@ which adds the value infinity to the natural numbers. In the next chapter, we will begin to develop the means to appreciate the way that Lean supports this sort of generality.

-
-
-

5.2. Induction and Recursion

+
+
+

5.2. Induction and Recursion

The set of natural numbers \(\mathbb{N} = \{ 0, 1, 2, \ldots \}\) is not only fundamentally important in its own right, but also a plays a central role in the construction of new mathematical objects. @@ -699,9 +697,9 @@ end MyNat

- -
-

5.3. Infinitely Many Primes

+
+
+

5.3. Infinitely Many Primes

Let us continue our exploration of induction and recursion with another mathematical standard: a proof that there are infinitely many primes. One way to formulate this is as the statement that @@ -1137,8 +1135,8 @@

If you managed to complete the proof, congratulations! This has been a serious feat of formalization.

- - + + diff --git a/C06_Structures.html b/C06_Structures.html index 15fadffc..666b451a 100644 --- a/C06_Structures.html +++ b/C06_Structures.html @@ -1,8 +1,7 @@ - - + 6. Structures — Mathematics in Lean 0.1 documentation @@ -16,7 +15,6 @@ - @@ -87,8 +85,8 @@
-
-

6. Structures

+
+

6. Structures

Modern mathematics makes essential use of algebraic structures, which encapsulate patterns that can be instantiated in @@ -107,8 +105,8 @@ algebraic structures on your own.

For more technical detail, you can consult Theorem Proving in Lean, and a paper by Anne Baanen, Use and abuse of instance parameters in the Lean mathematical library.

-
-

6.1. Defining structures

+
+

6.1. Defining structures

In the broadest sense of the term, a structure is a specification of a collection of data, possibly with constraints that the data is required to satisfy. @@ -467,9 +465,9 @@ Moreover, as we are about to see, Lean provides support for weaving structures together into a rich, interconnected hierarchy, and for managing the interactions between them.

-
-
-

6.2. Algebraic Structures

+
+
+

6.2. Algebraic Structures

To clarify what we mean by the phrase algebraic structure, it will help to consider some examples.

    @@ -1016,9 +1014,9 @@ the expressions we type. When used wisely, however, class inference is a powerful tool. It is what makes algebraic reasoning possible in Lean.

    -
-
-

6.3. Building the Gaussian Integers

+
+
+

6.3. Building the Gaussian Integers

We will now illustrate the use of the algebraic hierarchy in Lean by building an important mathematical object, the Gaussian integers, and showing that it is a Euclidean domain. In other words, according to @@ -1044,7 +1042,7 @@

\[\begin{split}(a + bi) (c + di) & = ac + bci + adi + bd i^2 \\ & = (ac - bd) + (bc + ad)i.\end{split}\]
-

This explains the definition of hasMul below.

+

This explains the definition of Mul below.

instance : Zero gaussInt :=
   ⟨⟨0, 0⟩⟩
 
@@ -1512,8 +1510,8 @@
   PrincipalIdealRing.irreducible_iff_prime
- - +
+
diff --git a/C07_Hierarchies.html b/C07_Hierarchies.html index d137a428..28f260b0 100644 --- a/C07_Hierarchies.html +++ b/C07_Hierarchies.html @@ -1,8 +1,7 @@ - - + 7. Hierarchies — Mathematics in Lean 0.1 documentation @@ -16,7 +15,6 @@ - @@ -86,8 +84,8 @@
-
-

7. Hierarchies

+
+

7. Hierarchies

We have seen in Chapter 6 how to define the class of groups and build instances of this class, and then how to build an instance of the commutative ring class. But of course there is a hierarchy here: a @@ -103,8 +101,8 @@ so we will used indices to distinguish our version. For instance we will have Ring₁ as our version of Ring. Since we will gradually explain more powerful ways of formalizing structures, those indices will sometimes grow beyond one.

-
-

7.1. Basics

+
+

7.1. Basics

At the very bottom of all hierarchies in Lean, we find data-carrying classes. The following class records that the given type α is endowed with a distinguished element called one. At this stage, it has no property at all.

@@ -320,9 +318,9 @@ attribute. Structures and classes are defined in both additive and multiplicative notation with an attribute to_additive linking them. In case of multiple inheritance like for semi-groups, the auto-generated “symmetry-restoring” instances need also to be marked. -This is a bit technical you don’t need to understand details. The important point is that +This is a bit technical; you don’t need to understand details. The important point is that lemmas are then only stated in multiplicative notation and marked with the attribute to_additive -to generate the additive version as left_inv_eq_right_inv' with it’s auto-generated additive +to generate the additive version as left_inv_eq_right_inv' with its auto-generated additive version left_neg_eq_right_neg'. In order to check the name of this additive version we used the whatsnew in command on top of left_inv_eq_right_inv'.

class AddSemigroup₃ (α : Type) extends Add α where
@@ -385,7 +383,7 @@
   sorry
-

Note that to_additive can be ask to tag a lemma with simp and propagate that attribute +

Note that to_additive can be asked to tag a lemma with simp and propagate that attribute to the additive version as follows.

@[to_additive (attr := simp)]
 lemma Group₃.mul_inv {G : Type} [Group₃ G] {a : G} : a * a⁻¹ = 1 := by
@@ -408,7 +406,7 @@
 
We are now ready for rings. For demonstration purposes we won’t assume that addition is
 commutative, and then immediately provide an instance of AddCommGroup₃. Mathlib does not
 play this game, first because in practice this does not make any ring instance easier and
-also because Mathlib’s algebraic hierarchy goes through semi-rings which are like rings but without
+also because Mathlib’s algebraic hierarchy goes through semirings which are like rings but without
 opposites so that the proof below does not work for them. What we gain here, besides a nice exercise
 if you have never seen it, is an example of building an instance using the syntax that allows
 to provide a parent structure and some extra fields.

@@ -629,9 +627,9 @@
 that every preorder comes with a <₁ which has a default value built from ≤₁ and a
 Prop-valued field asserting the natural relation between those two comparison operators.
 -/

-
-
-

7.2. Morphisms

+
+
+

7.2. Morphisms

So far in this chapter, we discussed how to create a hierarchy of mathematical structures. But defining structures is not really completed until we have morphisms. There are two main approaches here. The most obvious one is to define a predicate on functions.

@@ -833,9 +831,9 @@ := sorry
- -
-

7.3. Sub-objects

+
+
+

7.3. Sub-objects

After defining some algebraic structure and its morphisms, the next step is to consider sets that inherit this algebraic structure, for instance subgroups or subrings. This largely overlaps our previous topic. Indeed a set in X is implemented as a function from @@ -971,8 +969,8 @@ sorry

- - + + diff --git a/C08_Groups_and_Rings.html b/C08_Groups_and_Rings.html index 23206f12..1b7aaf93 100644 --- a/C08_Groups_and_Rings.html +++ b/C08_Groups_and_Rings.html @@ -1,8 +1,7 @@ - - + 8. Groups and Rings — Mathematics in Lean 0.1 documentation @@ -16,7 +15,6 @@ - @@ -99,8 +97,8 @@
-
-

8. Groups and Rings

+
+

8. Groups and Rings

We saw in Section 2.2 how to reason about operations in groups and rings. Later, in Section 6.2, we saw how to define abstract algebraic structures, such as group structures, as well as concrete instances @@ -114,10 +112,10 @@ decisions behind the way the topics are treated. So making sense of some of the examples may require reviewing the background from Chapter 7.

-
-

8.1. Monoids and Groups

-
-

8.1.1. Monoids and their morphisms

+
+

8.1. Monoids and Groups

+
+

8.1.1. Monoids and their morphisms

Courses in abstract algebra often start with groups and then progress to rings, fields, and vector spaces. This involves some contortions when discussing multiplication on rings since the multiplication operation does not come from a group structure @@ -126,7 +124,7 @@ is to leave those proofs as exercises. A less efficient but safer and more formalization-friendly way of proceeding is to use monoids. A monoid structure on a type M is an internal composition law that is associative and has a neutral element. -Monoids are used primarily to accommodate both groups and the multiplicative structure +Monoids are used primarily to accommodate both groups and the multiplicative structure of rings. But there are also a number of natural examples; for instance, the set of natural numbers equipped with addition forms a monoid.

From a practical point of view, you can mostly ignore monoids when using Mathlib. But you need @@ -139,7 +137,7 @@ By default, Monoid uses multiplicative notation for the operation; for additive notation use AddMonoid instead. The commutative versions of these structures add the prefix Comm before Monoid.

-
example {M : Type*} [Monoid M] (x : M) : x*1 = x := mul_one x
+
example {M : Type*} [Monoid M] (x : M) : x * 1 = x := mul_one x
 
 example {M : Type*} [AddCommMonoid M] (x y : M) : x + y = y + x := add_comm x y
 

@@ -151,10 +149,10 @@
 we apply it to elements of M. The additive version is called AddMonoidHom and written
 M →+ N.

 
example {M N : Type*} [Monoid M] [Monoid N] (x y : M) (f : M →* N) : f (x * y) = f x * f y :=
-f.map_mul x y
+  f.map_mul x y
 
 example {M N : Type*} [AddMonoid M] [AddMonoid N] (f : M →+ N) : f 0 = 0 :=
-f.map_zero
+  f.map_zero
 

 

 
These morphisms are bundled maps, i.e. they package together a map and some of its properties.
@@ -162,12 +160,12 @@
 here we simply note the slightly unfortunate consequence that we cannot use ordinary function
 composition to compose maps. Instead, we need to use MonoidHom.comp and AddMonoidHom.comp.

 
example {M N P : Type*} [AddMonoid M] [AddMonoid N] [AddMonoid P]
-  (f : M →+ N) (g : N →+ P) : M →+ P := g.comp f
+    (f : M →+ N) (g : N →+ P) : M →+ P := g.comp f
 

 

-
-
-

8.1.2. Groups and their morphisms

+
+
+

8.1.2. Groups and their morphisms

We will have much more to say about groups, which are monoids with the extra property that every element has an inverse.

example {G : Type*} [Group G] (x : G) : x * x⁻¹ = 1 := mul_inv_self x
@@ -176,7 +174,7 @@ 
8.1.2. Groups and their morphismsSimilar to the ring tactic that we saw earlier, there is a group tactic that proves
 any identity that holds in any group. (Equivalently, it proves the identities that hold in
 free groups.)

-
example {G : Type*} [Group G] (x y z : G) : x * (y * z) * (x*z)⁻¹ * (x * y * x⁻¹)⁻¹ = 1 := by
+
example {G : Type*} [Group G] (x y z : G) : x * (y * z) * (x * z)⁻¹ * (x * y * x⁻¹)⁻¹ = 1 := by
   group
 

 

@@ -189,12 +187,12 @@ 
8.1.2. Groups and their morphismsMonoid with Group.

 
example {G H : Type*} [Group G] [Group H] (x y : G) (f : G →* H) : f (x * y) = f x * f y :=
-f.map_mul x y
+  f.map_mul x y
 

 

 
Of course we do get some new properties, such as this one:

 
example {G H : Type*} [Group G] [Group H] (x : G) (f : G →* H) : f (x⁻¹) = (f x)⁻¹ :=
-f.map_inv x
+  f.map_inv x
 

 

 
You may be worried that constructing group morphisms will require us to do unnecessary work since
@@ -203,8 +201,8 @@ 
8.1.2. Groups and their morphisms
 
example {G H : Type*} [Group G] [Group H] (f : G → H) (h : ∀ x y, f (x * y) = f x * f y) :
-  G →* H :=
-MonoidHom.mk' f h
+    G →* H :=
+  MonoidHom.mk' f h
 

 

 
There is also a type MulEquiv of group (or monoid) isomorphisms denoted by ≃* (and
@@ -216,30 +214,30 @@ 
8.1.2. Groups and their morphismsf.trans g respectively.
 Elements of this type are automatically coerced to morphisms and functions when necessary.

 
example {G H : Type*} [Group G] [Group H] (f : G ≃* H) :
-  f.trans f.symm = MulEquiv.refl G :=
-f.self_trans_symm
+    f.trans f.symm = MulEquiv.refl G :=
+  f.self_trans_symm
 

 

 
One can use MulEquiv.ofBijective to build an isomorphism from a bijective morphism.
 Doing so makes the inverse function noncomputable.

 
noncomputable example {G H : Type*} [Group G] [Group H]
-      (f : G →* H) (h : Function.Bijective f) :
+    (f : G →* H) (h : Function.Bijective f) :
     G ≃* H :=
   MulEquiv.ofBijective f h
 

 

-
-
-

8.1.3. Subgroups

+
+
+

8.1.3. Subgroups

Just as group morphisms are bundled, a subgroup of G is also a bundled structure consisting of a set in G with the relevant closure properties.

example {G : Type*} [Group G] (H : Subgroup G) {x y : G} (hx : x ∈ H) (hy : y ∈ H) :
-  x * y ∈ H :=
-H.mul_mem hx hy
+    x * y ∈ H :=
+  H.mul_mem hx hy
 
 example {G : Type*} [Group G] (H : Subgroup G) {x : G} (hx : x ∈ H) :
-  x⁻¹ ∈ H :=
-H.inv_mem hx
+    x⁻¹ ∈ H :=
+  H.inv_mem hx

In the example above, it is important to understand that Subgroup G is the type of subgroups @@ -281,18 +279,18 @@

8.1.3. SubgroupsIsSubgroup : Set G → Prop is that one can easily endow Subgroup G with additional structure. Importantly, it has the structure of a complete lattice structure with respect to inclusion. For instance, instead of having a lemma stating that an intersection of -two subgroups of G if again a subgroup, we -have use the lattice operation ⊓ to construct the intersection. We can then apply arbitrary +two subgroups of G is again a subgroup, we +have used the lattice operation ⊓ to construct the intersection. We can then apply arbitrary lemmas about lattices to the construction.

Let us check that the set underlying the infimum of two subgroups is indeed, by definition, their intersection.

example {G : Type*} [Group G] (H H' : Subgroup G) :
-  ((H ⊓ H' : Subgroup G) : Set G) = (H : Set G) ∩ (H' : Set G) := rfl
+    ((H ⊓ H' : Subgroup G) : Set G) = (H : Set G) ∩ (H' : Set G) := rfl

It may look strange to have a different notation for what amounts to the intersection of the underlying sets, but the correspondence does not carry over to the supremum operation and set -union, since a union of subgroup is not a subgroup. +union, since a union of subgroups is not, in general, a subgroup. Instead one needs to use the subgroup generated by the union, which is done using Subgroup.closure.

example {G : Type*} [Group G] (H H' : Subgroup G) :
@@ -331,7 +329,7 @@ 
8.1.3. Subgroupsmap
 and comap.
 These are not the common mathematical terms, but they have the advantage of being
-shorter than “pushforward” and  “direct image.””

+shorter than “pushforward” and “direct image.”

 
example {G H : Type*} [Group G] [Group H] (G' : Subgroup G) (f : G →* H) : Subgroup H :=
   Subgroup.map f G'
 
@@ -361,23 +359,23 @@ 
8.1.3. Subgroupsopen Subgroup
 
-example (φ : G →* H) (S T : Subgroup H) (hST : S ≤ T) : comap φ S ≤ comap φ T :=by
+example (φ : G →* H) (S T : Subgroup H) (hST : S ≤ T) : comap φ S ≤ comap φ T := by
   sorry
 
-example (φ : G →* H) (S T : Subgroup G) (hST : S ≤ T) : map φ S ≤ map φ T :=by
+example (φ : G →* H) (S T : Subgroup G) (hST : S ≤ T) : map φ S ≤ map φ T := by
   sorry
 
 variable {K : Type*} [Group K]
 
 -- Remember you can use the `ext` tactic to prove an equality of subgroups.
 example (φ : G →* H) (ψ : H →* K) (U : Subgroup K) :
-  comap (ψ.comp φ) U = comap φ (comap ψ U) := by
+    comap (ψ.comp φ) U = comap φ (comap ψ U) := by
   sorry
 
 -- Pushing a subgroup along one homomorphism and then another is equal to
---  pushing it forward along the composite of the homomorphisms.
+-- pushing it forward along the composite of the homomorphisms.
 example (φ : G →* H) (ψ : H →* K) (S : Subgroup G) :
-  map (ψ.comp φ) S = map ψ (S.map φ) := by
+    map (ψ.comp φ) S = map ψ (S.map φ) := by
   sorry
 
 end exercises
@@ -386,9 +384,9 @@ 
8.1.3. SubgroupsLet us finish this introduction to subgroups in Mathlib with two very classical results.
 Lagrange theorem states the cardinality of a subgroup of a finite group divides the cardinality of
 the group. Sylow’s first theorem is a famous partial converse to Lagrange’s theorem.

-
Since this corner of Mathlib is partly set up to allow computation, we need to tell
-Lean to use nonconstructive logic, using the following attribute command.

-
attribute [local instance 10] setFintype Classical.propDecidable
+
While this corner of Mathlib is partly set up to allow computation, we can tell
+Lean to use nonconstructive logic anyway using the following open scoped command.

+
open scoped Classical
 
 open Fintype
 
@@ -403,7 +401,7 @@ 
8.1.3. Subgroups

 

 
The next two exercises derive a corollary of Lagrange’s lemma. (This is also already in Mathlib,
-so do not use exact? too quickly.)

+so do not use exact? too quickly.)

 
lemma eq_bot_iff_card {G : Type*} [Group G] {H : Subgroup G} [Fintype H] :
     H = ⊥ ↔ card H = 1 := by
   suffices (∀ x ∈ H, x = 1) ↔ ∃ x ∈ H, ∀ a ∈ H, a = x by
@@ -413,13 +411,13 @@ 
8.1.3. Subgroups#check card_dvd_of_le
 
 lemma inf_bot_of_coprime {G : Type*} [Group G] (H K : Subgroup G) [Fintype H] [Fintype K]
-    (h : (card H).Coprime (card K))  : H ⊓ K = ⊥ := by
-    sorry
+    (h : (card H).Coprime (card K)) : H ⊓ K = ⊥ := by
+  sorry
 

 

-
-

-
8.1.4. Concrete groups

+

+

+
8.1.4. Concrete groups

 
One can also manipulate concrete groups in Mathlib, although this is typically more complicated
 than working with the abstract theory.
 For instance, given any type X, the group of permutations of X is Equiv.Perm X.
@@ -429,7 +427,7 @@ 
8.1.4. Concrete groups
open Equiv
 
 example {X : Type*} [Finite X] : Subgroup.closure {σ : Perm X | Perm.IsCycle σ} = ⊤ :=
-Perm.closure_isCycle
+  Perm.closure_isCycle
 

 

 
One can be fully concrete and compute actual products of cycles. Below we use the #simp command,
@@ -493,9 +491,9 @@ 
8.1.4. Concrete groupsend FreeGroup
 

 

-
-

-
8.1.5. Group actions

+
+
+

8.1.5. Group actions

One important way that group theory interacts with the rest of mathematics is through the use of group actions. An action of a group G on some type X is nothing more than a morphism from G to @@ -510,28 +508,28 @@

8.1.5. Group actions
noncomputable section GroupActions
 
 example {G X : Type*} [Group G] [MulAction G X] (g g': G) (x : X) :
-  g • (g' • x) = (g * g') • x :=
-(mul_smul g g' x).symm
+    g • (g' • x) = (g * g') • x :=
+  (mul_smul g g' x).symm

There is also a version for additive group called AddAction, where the action is denoted by +ᵥ. This is used for instance in the definition of affine spaces.

example {G X : Type*} [AddGroup G] [AddAction G X] (g g' : G) (x : X) :
-  g +ᵥ (g' +ᵥ x) = (g + g') +ᵥ x :=
-(add_vadd g g' x).symm
+    g +ᵥ (g' +ᵥ x) = (g + g') +ᵥ x :=
+  (add_vadd g g' x).symm

The underlying group morphism is called MulAction.toPermHom.

open MulAction
 
 example {G X : Type*} [Group G] [MulAction G X] : G →* Equiv.Perm X :=
-toPermHom G X
+  toPermHom G X

As an illustration let us see how to define the Cayley isomorphism embedding of any group G into a permutation group, namely Perm G.

def CayleyIsoMorphism (G : Type*) [Group G] : G ≃* (toPermHom G G).range :=
-Equiv.Perm.subgroupOfMulAction G G
+  Equiv.Perm.subgroupOfMulAction G G

Note that nothing before the above definition required having a group rather than a monoid (or any @@ -579,7 +577,7 @@

8.1.5. Group actions
variable {G : Type*} [Group G]
 
 lemma conjugate_one (H : Subgroup G) : conjugate 1 H = H := by
-    sorry
+  sorry
 
 instance : MulAction G (Subgroup G) where
   smul := conjugate
@@ -591,33 +589,33 @@ 
8.1.5. Group actionsend GroupActions

- -
-

8.1.6. Quotient groups

+

+
+

8.1.6. Quotient groups

In the above discussion of subgroups acting on groups, we saw the quotient G ⧸ H appear. In general this is only a type. It can be endowed with a group structure such that the quotient map is a group morphism if and only if H is a normal subgroup (and this group structure is then unique).

-

The normality assumption is a type class Subgroup.Normal so that type class inference can use to -derive the group structure on the quotient.

+

The normality assumption is a type class Subgroup.Normal so that type class inference can use it +to derive the group structure on the quotient.

noncomputable section QuotientGroup
 
 example {G : Type*} [Group G] (H : Subgroup G) [H.Normal] : Group (G ⧸ H) := inferInstance
 
 example {G : Type*} [Group G] (H : Subgroup G) [H.Normal] : G →* G ⧸ H :=
-QuotientGroup.mk' H
+  QuotientGroup.mk' H

The universal property of quotient groups is accessed through QuotientGroup.lift: a group morphism φ descends to G ⧸ N as soon as its kernel contains N.

example {G : Type*} [Group G] (N : Subgroup G) [N.Normal] {M : Type*}
-  [Group M] (φ : G →* M) (h : N ≤ MonoidHom.ker φ) : G ⧸ N →* M :=
-QuotientGroup.lift N φ h
+    [Group M] (φ : G →* M) (h : N ≤ MonoidHom.ker φ) : G ⧸ N →* M :=
+  QuotientGroup.lift N φ h

The fact that the target group is called M is the above snippet is a clue that having a monoid structure on M would be enough.

-

An important special case is when N = ker φ In that case the descended morphism is +

An important special case is when N = ker φ. In that case the descended morphism is injective and we get a group isomorphism onto its image. This result is often called the first isomorphism theorem.

example {G : Type*} [Group G] {M : Type*} [Group M] (φ : G →* M) :
@@ -643,7 +641,7 @@ 
8.1.5. Group actions
example {G : Type*} [Group G] {M N : Subgroup G} [M.Normal]
-  [N.Normal] (h : M = N) : G ⧸ M ≃* G ⧸ N := QuotientGroup.quotientMulEquivOfEq  h
+    [N.Normal] (h : M = N) : G ⧸ M ≃* G ⧸ N := QuotientGroup.quotientMulEquivOfEq h

As a final series of exercises for this section, we will prove that if H and K are disjoint @@ -653,7 +651,7 @@

8.1.5. Group actions
section
-variable  {G : Type*} [Group G] {H K : Subgroup G}
+variable {G : Type*} [Group G] {H K : Subgroup G}
 
 open MonoidHom
 
@@ -662,7 +660,7 @@ 
8.1.5. Group actions#check Subgroup.index_mul_card
 #check Nat.eq_of_mul_eq_mul_right
 
-lemma aux_card_eq [Fintype G] (h' : card G = card H * card K) : card (G⧸H) = card K := by
+lemma aux_card_eq [Fintype G] (h' : card G = card H * card K) : card (G ⧸ H) = card K := by
   sorry

@@ -675,14 +673,14 @@

8.1.5. Group actions#check restrict #check ker_restrict -def iso₁ [Fintype G] (h : Disjoint H K) (h' : card G = card H * card K) : K ≃* G⧸H := by +def iso₁ [Fintype G] (h : Disjoint H K) (h' : card G = card H * card K) : K ≃* G ⧸ H := by sorry

Now we can define our second building block. We will need MonoidHom.prod, which builds a morphism from G₀ to G₁ × G₂ out of morphisms from G₀ to G₁ and G₂.

-
def iso₂ : G ≃* (G⧸K) × (G⧸H) := by
+
def iso₂ : G ≃* (G ⧸ K) × (G ⧸ H) := by
   sorry
 

 

@@ -693,32 +691,32 @@ 
8.1.5. Group actionssorry
- - -
-

8.2. Rings

-
-

8.2.1. Rings, their units, morphisms and subrings

+ + +
+

8.2. Rings

+
+

8.2.1. Rings, their units, morphisms and subrings

The type of ring structures on a type R is Ring R. The variant where multiplication is assumed to be commutative is CommRing R. We have already seen that the ring tactic will prove any equality that follows from the axioms of a commutative ring.

-
example {R : Type*} [CommRing R] (x y : R) : (x + y)^2 = x^2 + y^2 + 2*x*y := by ring
+
example {R : Type*} [CommRing R] (x y : R) : (x + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y := by ring
 

 

-
More exotic variants do not require that the addition on R  forms a group but only an additive
+
More exotic variants do not require that the addition on R forms a group but only an additive
 monoid. The corresponding type classes are Semiring R and CommSemiring R.
 The type of natural numbers is an important instance of CommSemiring R, as is any type
 of functions taking values in the natural numbers.
 Another important example is the type of ideals in a ring, which will be discussed below.
 The name of the ring tactic is doubly misleading, since it assumes commutativity but works
 in semirings as well. In other words, it applies to any CommSemiring.

-
example (x y : ℕ) : (x + y)^2 = x^2 + y^2 + 2*x*y := by ring
+
example (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y := by ring
 

 

 
There are also versions of the ring and semiring classes that do not assume the existence of a
 multiplicative unit or
 the associativity of multiplication. We will not discuss those here.

-
Some concepts that are traditionally taught in an introduction to  ring theory are actually about
+
Some concepts that are traditionally taught in an introduction to ring theory are actually about
 the underlying multiplicative monoid.
 A prominent example is the definition of the units of a ring. Every (multiplicative) monoid M
 has a predicate IsUnit : M → Prop asserting existence of a two-sided inverse, a
@@ -731,7 +729,7 @@ 
8.1.5. Group actionsx seen as unit.

 
example (x : ℤˣ) : x = 1 ∨ x = -1 := Int.units_eq_one_or x
 
-example {M : Type*} [Monoid M] (x : Mˣ) : (x : M)*x⁻¹ = 1 := Units.mul_inv x
+example {M : Type*} [Monoid M] (x : Mˣ) : (x : M) * x⁻¹ = 1 := Units.mul_inv x
 
 example {M : Type*} [Monoid M] : Group Mˣ := inferInstance
 

@@ -745,7 +743,7 @@ 
8.1.5. Group actionsUnits.map f
 

 

-
The isormophism variant is RingEquiv, with notation ≃+*.

+
The isomorphism variant is RingEquiv, with notation ≃+*.

 
As with submonoids and subgroups, there is a Subring R type for subrings of a ring R,
 but this type is a lot less useful than the type of subgroups since one cannot quotient a ring by
 a subring.

@@ -753,9 +751,9 @@ 
8.1.5. Group actionsRingHom.range produces a subring.

-
-
-

8.2.2. Ideals and quotients

+ +
+

8.2.2. Ideals and quotients

For historical reasons, Mathlib only has a theory of ideals for commutative rings. (The ring library was originally developed to make quick progress toward the foundations of modern algebraic geometry.) So in this section we will work with commutative (semi)rings. @@ -765,7 +763,7 @@

8.2.2. Ideals and quotientsIdeal.Quotient.mk I by I.Quotient.mk in the snippet below because the parser immediately replaces Ideal R with Submodule R R.

-
example {R : Type*} [CommRing R] (I : Ideal R) : R →+* R⧸I :=
+
example {R : Type*} [CommRing R] (I : Ideal R) : R →+* R ⧸ I :=
   Ideal.Quotient.mk I
 
 example {R : Type*} [CommRing R] {a : R} {I : Ideal R} :
@@ -827,7 +825,7 @@ 
8.2.2. Ideals and quotientsIdeal.quotientInfRingEquivPiQuotient f hf
 

 

-
The elementary version of the Chinese remainder theorem, a statement about Zmod, can be easily
+
The elementary version of the Chinese remainder theorem, a statement about ZMod, can be easily
 deduced from the previous one:

 
open BigOperators PiNotation
 
@@ -881,7 +879,7 @@ 
8.2.2. Ideals and quotientsFinset. Relevant lemmas on Finset are given
 below.
-Remember that the ring tactic work for semirings and that the ideals of a ring form a semiring.

+Remember that the ring tactic works for semirings and that the ideals of a ring form a semiring.

 
#check Finset.mem_insert_of_mem
 #check Finset.mem_insert_self
 
@@ -896,10 +894,10 @@ 
8.2.2. Ideals and quotientsrw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
       set K := ⨅ j ∈ s, J j
       calc
-        1 = I + K            := sorry
-        _ = I + K*(I + J i)  := sorry
-        _ = (1+K)*I + K*J i  := sorry
-        _ ≤ I + K ⊓ J i      := sorry
+        1 = I + K                  := sorry
+        _ = I + K * (I + J i)      := sorry
+        _ = (1 + K) * I + K * J i  := sorry
+        _ ≤ I + K ⊓ J i            := sorry
 

 

 
We can now prove surjectivity of the map appearing in the Chinese remainder theorem.

@@ -914,25 +912,25 @@ 
8.2.2. Ideals and quotientssorry
     sorry
   choose e he using key
-  use mk _ (∑ i, f i*e i)
+  use mk _ (∑ i, f i * e i)
   sorry
 

 

 
Now all the pieces come together in the following:

 
noncomputable def chineseIso [Fintype ι] (f : ι → Ideal R)
-    (hf : ∀ i j, i ≠ j → IsCoprime (f i) (f j)) : (R ⧸ ⨅ i, f i) ≃+* ∀ i, R ⧸ f i :=
+    (hf : ∀ i j, i ≠ j → IsCoprime (f i) (f j)) : (R ⧸ ⨅ i, f i) ≃+* Π i, R ⧸ f i :=
   { Equiv.ofBijective _ ⟨chineseMap_inj f, chineseMap_surj hf⟩,
     chineseMap f with }
 

 

-

-
-

8.2.3. Algebras and polynomials

-

Given a commutative (semi)ring R, an algebra over ``R`` is a semiring A equipped + +

+

8.2.3. Algebras and polynomials

+

Given a commutative (semi)ring R, an algebra over R is a semiring A equipped with a ring morphism whose image commutes with every element of A. This is encoded as a type class Algebra R A. The morphism from R to A is called the structure map and is denoted -algebraMap R A : R →*+ A in Lean. +algebraMap R A : R →+* A in Lean. Multiplication of a : A by algebraMap R A r for some r : R is called the scalar multiplication of a by r and denoted by r • a. Note that this notion of algebra is sometimes called an associative unital algebra to emphasize the @@ -973,15 +971,15 @@

8.2.3. Algebras and polynomialsBecause C is a ring morphism from R to R[X], we can use all ring morphisms lemmas such as map_zero, map_one, map_mul, and map_pow before computing in the ring R[X]. For example:

-
example {R : Type*} [CommRing R] (r : R) : (X + C r) * (X - C r) = X^2 - C (r ^ 2) := by
+
example {R : Type*} [CommRing R] (r : R) : (X + C r) * (X - C r) = X ^ 2 - C (r ^ 2) := by
   rw [C.map_pow]
   ring
 

 

 
You can access coefficients using Polynomial.coeff

-
example {R : Type*} [CommRing R](r:R) : (C r).coeff 0 = r := by simp
+
example {R : Type*} [CommRing R] (r:R) : (C r).coeff 0 = r := by simp
 
-example {R : Type*} [CommRing R] : (X^2 + 2*X + C 3 : R[X]).coeff 1 = 2 := by simp
+example {R : Type*} [CommRing R] : (X ^ 2 + 2 * X + C 3 : R[X]).coeff 1 = 2 := by simp
 

 

 
Defining the degree of a polynomial is always tricky because of the special case of the zero
@@ -1020,7 +1018,7 @@ 
8.2.3. Algebras and polynomialsexample {R : Type*} [CommRing R] (r : R) : (X - C r).eval r = 0 := by simp
 

 

-
In particular, there is a predicate, IsRoot, that hold of elements r in R where a
+
In particular, there is a predicate, IsRoot, that holds for elements r in R where a
 polynomial vanishes.

 
example {R : Type*} [CommRing R] (P : R[X]) (r : R) : IsRoot P r ↔ P.eval r = 0 := Iff.rfl
 

@@ -1036,19 +1034,19 @@ 
8.2.3. Algebras and polynomialsroots_X_sub_C r
 
 example {R : Type*} [CommRing R] [IsDomain R] (r : R) (n : ℕ):
-    ((X - C r)^n).roots = n • {r} :=
+    ((X - C r) ^ n).roots = n • {r} :=
   by simp
-

Both Polynomial.eval and Polynomial.roots consider only the coefficients ring. They do not -allow us to say that X^2 - 2 : ℚ[X] has a root in ℝ or that X^2 + 1 : ℝ[X] has a root in +

Both Polynomial.eval and Polynomial.roots consider only the coefficients ring. They do not +allow us to say that X ^ 2 - 2 : ℚ[X] has a root in ℝ or that X ^ 2 + 1 : ℝ[X] has a root in ℂ. For this, we need Polynomial.aeval, which will evaluate P : R[X] in any R-algebra. More precisely, given a semiring A and an instance of Algebra R A, Polynomial.aeval sends every element of a along the R-algebra morphism of evaluation at a. Since AlgHom has a coercion to functions, one can apply it to a polynomial. But aeval does not have a polynomial as an argument, so one cannot use dot notation like in P.eval above.

-
example : aeval Complex.I (X^2 + 1 : ℝ[X]) = 0 := by simp
+
example : aeval Complex.I (X ^ 2 + 1 : ℝ[X]) = 0 := by simp
 

 

 
The function corresponding to roots in this context is aroots which takes a polynomial
@@ -1056,7 +1054,7 @@ 
8.2.3. Algebras and polynomialsroots).

 
open Complex Polynomial
 
-example : aroots (X^2 + 1 : ℝ[X]) ℂ = {Complex.I, -I} := by
+example : aroots (X ^ 2 + 1 : ℝ[X]) ℂ = {Complex.I, -I} := by
   suffices roots (X ^ 2 + 1 : ℂ[X]) = {I, -I} by simpa [aroots_def]
   have factored : (X ^ 2 + 1 : ℂ[X]) = (X - C I) * (X - C (-I)) := by
     rw [C_neg]
@@ -1078,7 +1076,7 @@ 
8.2.3. Algebras and polynomials
 
#check (Complex.ofReal : ℝ →+* ℂ)
 
-example : (X^2 + 1 : ℝ[X]).eval₂ Complex.ofReal Complex.I = 0 := by simp
+example : (X ^ 2 + 1 : ℝ[X]).eval₂ Complex.ofReal Complex.I = 0 := by simp
 

 

 
Let us end by mentioning multivariate polynomials briefly. Given a commutative semiring R,
@@ -1101,9 +1099,9 @@ 
8.2.3. Algebras and polynomials
example : MvPolynomial.eval ![0, 1] circleEquation = 0 := by simp [circleEquation]
 

 

-

-
- + + + diff --git a/C09_Topology.html b/C09_Topology.html index 172fd93a..6e3d40dd 100644 --- a/C09_Topology.html +++ b/C09_Topology.html @@ -1,8 +1,7 @@ - - + 9. Topology — Mathematics in Lean 0.1 documentation @@ -16,7 +15,6 @@ - @@ -99,8 +97,8 @@
-
-

9. Topology

+
+

9. Topology

Calculus is based on the concept of a function, which is used to model quantities that depend on one another. For example, it is common to study quantities that change over time. @@ -167,8 +165,8 @@ Formalizing mathematics requires making the relevant notion of “sameness” fully explicit, and that is exactly what Bourbaki’s theory of filters manages to do.

-
-

9.1. Filters

+
+

9.1. Filters

A filter on a type X is a collection of sets of X that satisfies three conditions that we will spell out below. The notion supports two related ideas:

@@ -410,7 +408,7 @@

There is also a nice basis for the filter atTop. The lemma -Filter.has_basis.tendsto_iff allows +Filter.HasBasis.tendsto_iff allows us to reformulate a statement of the form Tendsto f F G given bases for F and G. Putting these pieces together gives us essentially the notion of convergence @@ -520,9 +518,9 @@ sorry

- -
-

9.2. Metric spaces

+ +
+

9.2. Metric spaces

Examples in the previous section focus on sequences of real numbers. In this section we will go up a bit in generality and focus on metric spaces. A metric space is a type X equipped with a distance function dist : X → X → ℝ which is a generalization of the function fun x y ↦ |x - y| from the case where X = ℝ.

@@ -540,8 +538,8 @@ They are called EMetricSpace, PseudoMetricSpace and PseudoEMetricSpace respectively (here “e” stands for “extended”).

Note that our journey from ℝ to metric spaces jumped over the special case of normed spaces that also require linear algebra and will be explained as part of the calculus chapter.

-
-

9.2.1. Convergence and continuity

+
+

9.2.1. Convergence and continuity

Using distance functions, we can already define convergent sequences and continuous functions between metric spaces. They are actually defined in a more general setting covered in the next section, but we have lemmas recasting the definition is terms of distances.

@@ -628,9 +626,9 @@

9.2.1. Convergence and continuityMetric.continuousAt_iff

-
-
-

9.2.2. Balls, open sets and closed sets

+ +
+

9.2.2. Balls, open sets and closed sets

Once we have a distance function, the most important geometric definitions are (open) balls and closed balls.

variable (r : ℝ)
 
@@ -685,9 +683,9 @@ 
9.2.2. Balls, open sets and closed sets<
   Metric.nhds_basis_closedBall.mem_iff
-
-
-

9.2.3. Compactness

+ +
+

9.2.3. Compactness

Compactness is an important topological notion. It distinguishes subsets of a metric space that enjoy the same kind of properties as segments in reals compared to other intervals:

    @@ -728,9 +726,9 @@

    9.2.3. Compactness

In a compact metric space any closed set is compact, this is IsClosed.isCompact.

-
-
-

9.2.4. Uniformly continuous functions

+ +
+

9.2.4. Uniformly continuous functions

We now turn to uniformity notions on metric spaces : uniformly continuous functions, Cauchy sequences and completeness. Again those are defined in a more general context but we have lemmas in the metric name space to access their elementary definitions. We start with uniform continuity.

@@ -759,9 +757,9 @@

9.2.4. Uniformly continuous functionssorry

-
-
-

9.2.5. Completeness

+ +
+

9.2.5. Completeness

A Cauchy sequence in a metric space is a sequence whose terms get closer and closer to each other. There are a couple of equivalent ways to state that idea. In particular converging sequences are Cauchy. The converse is true only in so-called complete @@ -850,12 +848,12 @@

9.2.5. Completenesssorry

-
- -
-

9.3. Topological spaces

-
-

9.3.1. Fundamentals

+ + +
+

9.3. Topological spaces

+
+

9.3.1. Fundamentals

We now go up in generality and introduce topological spaces. We will review the two main ways to define topological spaces and then explain how the category of topological spaces is much better behaved than the category of metric spaces. Note that we won’t be using Mathlib category theory here, only having @@ -1043,9 +1041,9 @@

9.3.1. Fundamentals

This ends our tour of how Mathlib thinks that topological spaces fix defects of the theory of metric spaces by being a more functorial theory and having a complete lattice structure for any fixed type.

-

-
-

9.3.2. Separation and countability

+ +
+

9.3.2. Separation and countability

We saw that the category of topological spaces have very nice properties. The price to pay for this is existence of rather pathological topological spaces. There are a number of assumptions you can make on a topological space to ensure its behavior @@ -1132,9 +1130,9 @@

9.3.2. Separation and countabilitymem_closure_iff_seq_limit

-
-
-

9.3.3. Compactness

+ +
+

9.3.3. Compactness

Let us now discuss how compactness is defined for topological spaces. As usual there are several ways to think about it and Mathlib goes for the filter version.

We first need to define cluster points of filters. Given a filter F on a topological space X, @@ -1190,9 +1188,9 @@

9.3.3. Compactnesshs.elim_finite_subcover U hUo hsU

-
-
- + + + diff --git a/C10_Differential_Calculus.html b/C10_Differential_Calculus.html index f0a3bbf9..d3a981be 100644 --- a/C10_Differential_Calculus.html +++ b/C10_Differential_Calculus.html @@ -1,8 +1,7 @@ - - + 10. Differential Calculus — Mathematics in Lean 0.1 documentation @@ -16,7 +15,6 @@ - @@ -92,8 +90,8 @@
-
-

10. Differential Calculus

+
+

10. Differential Calculus

We now consider the formalization of notions from analysis, starting with differentiation in this chapter and turning integration and measure theory in the next. @@ -102,8 +100,8 @@ which is familiar from any introductory calculus class. In Section 10.2, we then consider the notion of a derivative in a much broader setting.

-
-

10.1. Elementary Differential Calculus

+
+

10.1. Elementary Differential Calculus

Let f be a function from the reals to the reals. There is a difference between talking about the derivative of f at a single point and talking about the derivative function. @@ -176,11 +174,11 @@ example : deriv sin π = -1 := by simp

-
-
-

10.2. Differential Calculus in Normed Spaces

-
-

10.2.1. Normed spaces

+
+
+

10.2. Differential Calculus in Normed Spaces

+
+

10.2.1. Normed spaces

Differentiation can be generalized beyond ℝ using the notion of a normed vector space, which encapsulates both direction and distance. We start with the notion of a normed group, which as an additive commutative @@ -243,9 +241,9 @@

10.2.1. Normed spacesFiniteDimensional.complete 𝕜 E

- -
-

10.2.2. Continuous linear maps

+
+
+

10.2.2. Continuous linear maps

We now turn to the morphisms in the category of normed spaces, namely, continuous linear maps. In Mathlib, the type of 𝕜-linear continuous maps between normed spaces @@ -325,9 +323,9 @@

10.2.2. Continuous linear mapssorry

- -
-

10.2.3. Asymptotic comparisons

+ +
+

10.2.3. Asymptotic comparisons

Defining differentiability also requires asymptotic comparisons. Mathlib has an extensive library covering the big O and little o relations, whose definitions are shown below. @@ -353,9 +351,9 @@

10.2.3. Asymptotic comparisonsIff.rfl

-
-
-

10.2.4. Differentiability

+ +
+

10.2.4. Differentiability

We are now ready to discuss differentiable functions between normed spaces. In analogy the elementary one-dimensional, Mathlib defines a predicate HasFDerivAt and a function fderiv. @@ -438,9 +436,9 @@

10.2.4. DifferentiabilityHasFDerivWithinAt or the even more general HasFDerivAtFilter.

-

- - + + + diff --git a/C11_Integration_and_Measure_Theory.html b/C11_Integration_and_Measure_Theory.html index 5c0d8de1..9a3f29b4 100644 --- a/C11_Integration_and_Measure_Theory.html +++ b/C11_Integration_and_Measure_Theory.html @@ -1,8 +1,7 @@ - - + 11. Integration and Measure Theory — Mathematics in Lean 0.1 documentation @@ -16,7 +15,6 @@ - @@ -87,10 +85,10 @@
-
-

11. Integration and Measure Theory

-
-

11.1. Elementary Integration

+
+

11. Integration and Measure Theory

+
+

11.1. Elementary Integration

We first focus on integration of functions on finite intervals in ℝ. We can integrate elementary functions.

open MeasureTheory intervalIntegral
@@ -127,9 +125,9 @@
   rfl
-
-
-

11.2. Measure Theory

+
+
+

11.2. Measure Theory

The general context for integration in Mathlib is measure theory. Even the elementary integrals of the previous section are in fact Bochner integrals. Bochner integration is a generalization of Lebesgue integration where the target space can be any Banach space, @@ -204,9 +202,9 @@ Iff.rfl

- -
-

11.3. Integration

+ +
+

11.3. Integration

Now that we have measurable spaces and measures we can consider integrals. As explained above, Mathlib uses a very general notion of integration that allows any Banach space as the target. @@ -281,8 +279,8 @@ integral_image_eq_integral_abs_det_fderiv_smul μ hs hf h_inj g

-
- + + diff --git a/_static/_sphinx_javascript_frameworks_compat.js b/_static/_sphinx_javascript_frameworks_compat.js deleted file mode 100644 index 8549469d..00000000 --- a/_static/_sphinx_javascript_frameworks_compat.js +++ /dev/null @@ -1,134 +0,0 @@ -/* - * _sphinx_javascript_frameworks_compat.js - * ~~~~~~~~~~ - * - * Compatability shim for jQuery and underscores.js. - * - * WILL BE REMOVED IN Sphinx 6.0 - * xref RemovedInSphinx60Warning - * - */ - -/** - * select a different prefix for underscore - */ -$u = _.noConflict(); - - -/** - * small helper function to urldecode strings - * - * See https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/decodeURIComponent#Decoding_query_parameters_from_a_URL - */ -jQuery.urldecode = function(x) { - if (!x) { - return x - } - return decodeURIComponent(x.replace(/\+/g, ' ')); -}; - -/** - * small helper function to urlencode strings - */ -jQuery.urlencode = encodeURIComponent; - -/** - * This function returns the parsed url parameters of the - * current request. Multiple values per key are supported, - * it will always return arrays of strings for the value parts. - */ -jQuery.getQueryParameters = function(s) { - if (typeof s === 'undefined') - s = document.location.search; - var parts = s.substr(s.indexOf('?') + 1).split('&'); - var result = {}; - for (var i = 0; i < parts.length; i++) { - var tmp = parts[i].split('=', 2); - var key = jQuery.urldecode(tmp[0]); - var value = jQuery.urldecode(tmp[1]); - if (key in result) - result[key].push(value); - else - result[key] = [value]; - } - return result; -}; - -/** - * highlight a given string on a jquery object by wrapping it in - * span elements with the given class name. - */ -jQuery.fn.highlightText = function(text, className) { - function highlight(node, addItems) { - if (node.nodeType === 3) { - var val = node.nodeValue; - var pos = val.toLowerCase().indexOf(text); - if (pos >= 0 && - !jQuery(node.parentNode).hasClass(className) && - !jQuery(node.parentNode).hasClass("nohighlight")) { - var span; - var isInSVG = jQuery(node).closest("body, svg, foreignObject").is("svg"); - if (isInSVG) { - span = document.createElementNS("http://www.w3.org/2000/svg", "tspan"); - } else { - span = document.createElement("span"); - span.className = className; - } - span.appendChild(document.createTextNode(val.substr(pos, text.length))); - node.parentNode.insertBefore(span, node.parentNode.insertBefore( - document.createTextNode(val.substr(pos + text.length)), - node.nextSibling)); - node.nodeValue = val.substr(0, pos); - if (isInSVG) { - var rect = document.createElementNS("http://www.w3.org/2000/svg", "rect"); - var bbox = node.parentElement.getBBox(); - rect.x.baseVal.value = bbox.x; - rect.y.baseVal.value = bbox.y; - rect.width.baseVal.value = bbox.width; - rect.height.baseVal.value = bbox.height; - rect.setAttribute('class', className); - addItems.push({ - "parent": node.parentNode, - "target": rect}); - } - } - } - else if (!jQuery(node).is("button, select, textarea")) { - jQuery.each(node.childNodes, function() { - highlight(this, addItems); - }); - } - } - var addItems = []; - var result = this.each(function() { - highlight(this, addItems); - }); - for (var i = 0; i < addItems.length; ++i) { - jQuery(addItems[i].parent).before(addItems[i].target); - } - return result; -}; - -/* - * backward compatibility for jQuery.browser - * This will be supported until firefox bug is fixed. - */ -if (!jQuery.browser) { - jQuery.uaMatch = function(ua) { - ua = ua.toLowerCase(); - - var match = /(chrome)[ \/]([\w.]+)/.exec(ua) || - /(webkit)[ \/]([\w.]+)/.exec(ua) || - /(opera)(?:.*version|)[ \/]([\w.]+)/.exec(ua) || - /(msie) ([\w.]+)/.exec(ua) || - ua.indexOf("compatible") < 0 && /(mozilla)(?:.*? rv:([\w.]+)|)/.exec(ua) || - []; - - return { - browser: match[ 1 ] || "", - version: match[ 2 ] || "0" - }; - }; - jQuery.browser = {}; - jQuery.browser[jQuery.uaMatch(navigator.userAgent).browser] = true; -} diff --git a/_static/basic.css b/_static/basic.css index 9039e027..bf18350b 100644 --- a/_static/basic.css +++ b/_static/basic.css @@ -222,7 +222,7 @@ table.modindextable td { /* -- general body styles --------------------------------------------------- */ div.body { - min-width: 360px; + min-width: 450px; max-width: 800px; } @@ -335,13 +335,13 @@ p.sidebar-title { font-weight: bold; } -div.admonition, div.topic, aside.topic, blockquote { +div.admonition, div.topic, blockquote { clear: left; } /* -- topics ---------------------------------------------------------------- */ -div.topic, aside.topic { +div.topic { border: 1px solid #ccc; padding: 7px; margin: 10px 0 10px 0; @@ -380,7 +380,6 @@ div.body p.centered { div.sidebar > :last-child, aside.sidebar > :last-child, div.topic > :last-child, -aside.topic > :last-child, div.admonition > :last-child { margin-bottom: 0; } @@ -388,7 +387,6 @@ div.admonition > :last-child { div.sidebar::after, aside.sidebar::after, div.topic::after, -aside.topic::after, div.admonition::after, blockquote::after { display: block; @@ -430,6 +428,10 @@ table.docutils td, table.docutils th { border-bottom: 1px solid #aaa; } +table.footnote td, table.footnote th { + border: 0 !important; +} + th { text-align: left; padding-right: 5px; @@ -613,7 +615,6 @@ ul.simple p { margin-bottom: 0; } -/* Docutils 0.17 and older (footnotes & citations) */ dl.footnote > dt, dl.citation > dt { float: left; @@ -631,33 +632,6 @@ dl.citation > dd:after { clear: both; } -/* Docutils 0.18+ (footnotes & citations) */ -aside.footnote > span, -div.citation > span { - float: left; -} -aside.footnote > span:last-of-type, -div.citation > span:last-of-type { - padding-right: 0.5em; -} -aside.footnote > p { - margin-left: 2em; -} -div.citation > p { - margin-left: 4em; -} -aside.footnote > p:last-of-type, -div.citation > p:last-of-type { - margin-bottom: 0em; -} -aside.footnote > p:last-of-type:after, -div.citation > p:last-of-type:after { - content: ""; - clear: both; -} - -/* Footnotes & citations ends */ - dl.field-list { display: grid; grid-template-columns: fit-content(30%) auto; diff --git a/_static/doctools.js b/_static/doctools.js index c3db08d1..e509e483 100644 --- a/_static/doctools.js +++ b/_static/doctools.js @@ -2,263 +2,325 @@ * doctools.js * ~~~~~~~~~~~ * - * Base JavaScript utilities for all Sphinx HTML documentation. + * Sphinx JavaScript utilities for all documentation. * * :copyright: Copyright 2007-2022 by the Sphinx team, see AUTHORS. * :license: BSD, see LICENSE for details. * */ -"use strict"; -const _ready = (callback) => { - if (document.readyState !== "loading") { - callback(); - } else { - document.addEventListener("DOMContentLoaded", callback); +/** + * select a different prefix for underscore + */ +$u = _.noConflict(); + +/** + * make the code below compatible with browsers without + * an installed firebug like debugger +if (!window.console || !console.firebug) { + var names = ["log", "debug", "info", "warn", "error", "assert", "dir", + "dirxml", "group", "groupEnd", "time", "timeEnd", "count", "trace", + "profile", "profileEnd"]; + window.console = {}; + for (var i = 0; i < names.length; ++i) + window.console[names[i]] = function() {}; +} + */ + +/** + * small helper function to urldecode strings + * + * See https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/decodeURIComponent#Decoding_query_parameters_from_a_URL + */ +jQuery.urldecode = function(x) { + if (!x) { + return x } + return decodeURIComponent(x.replace(/\+/g, ' ')); }; /** - * highlight a given string on a node by wrapping it in - * span elements with the given class name. + * small helper function to urlencode strings */ -const _highlight = (node, addItems, text, className) => { - if (node.nodeType === Node.TEXT_NODE) { - const val = node.nodeValue; - const parent = node.parentNode; - const pos = val.toLowerCase().indexOf(text); - if ( - pos >= 0 && - !parent.classList.contains(className) && - !parent.classList.contains("nohighlight") - ) { - let span; +jQuery.urlencode = encodeURIComponent; - const closestNode = parent.closest("body, svg, foreignObject"); - const isInSVG = closestNode && closestNode.matches("svg"); - if (isInSVG) { - span = document.createElementNS("http://www.w3.org/2000/svg", "tspan"); - } else { - span = document.createElement("span"); - span.classList.add(className); - } +/** + * This function returns the parsed url parameters of the + * current request. Multiple values per key are supported, + * it will always return arrays of strings for the value parts. + */ +jQuery.getQueryParameters = function(s) { + if (typeof s === 'undefined') + s = document.location.search; + var parts = s.substr(s.indexOf('?') + 1).split('&'); + var result = {}; + for (var i = 0; i < parts.length; i++) { + var tmp = parts[i].split('=', 2); + var key = jQuery.urldecode(tmp[0]); + var value = jQuery.urldecode(tmp[1]); + if (key in result) + result[key].push(value); + else + result[key] = [value]; + } + return result; +}; - span.appendChild(document.createTextNode(val.substr(pos, text.length))); - parent.insertBefore( - span, - parent.insertBefore( +/** + * highlight a given string on a jquery object by wrapping it in + * span elements with the given class name. + */ +jQuery.fn.highlightText = function(text, className) { + function highlight(node, addItems) { + if (node.nodeType === 3) { + var val = node.nodeValue; + var pos = val.toLowerCase().indexOf(text); + if (pos >= 0 && + !jQuery(node.parentNode).hasClass(className) && + !jQuery(node.parentNode).hasClass("nohighlight")) { + var span; + var isInSVG = jQuery(node).closest("body, svg, foreignObject").is("svg"); + if (isInSVG) { + span = document.createElementNS("http://www.w3.org/2000/svg", "tspan"); + } else { + span = document.createElement("span"); + span.className = className; + } + span.appendChild(document.createTextNode(val.substr(pos, text.length))); + node.parentNode.insertBefore(span, node.parentNode.insertBefore( document.createTextNode(val.substr(pos + text.length)), - node.nextSibling - ) - ); - node.nodeValue = val.substr(0, pos); - - if (isInSVG) { - const rect = document.createElementNS( - "http://www.w3.org/2000/svg", - "rect" - ); - const bbox = parent.getBBox(); - rect.x.baseVal.value = bbox.x; - rect.y.baseVal.value = bbox.y; - rect.width.baseVal.value = bbox.width; - rect.height.baseVal.value = bbox.height; - rect.setAttribute("class", className); - addItems.push({ parent: parent, target: rect }); + node.nextSibling)); + node.nodeValue = val.substr(0, pos); + if (isInSVG) { + var rect = document.createElementNS("http://www.w3.org/2000/svg", "rect"); + var bbox = node.parentElement.getBBox(); + rect.x.baseVal.value = bbox.x; + rect.y.baseVal.value = bbox.y; + rect.width.baseVal.value = bbox.width; + rect.height.baseVal.value = bbox.height; + rect.setAttribute('class', className); + addItems.push({ + "parent": node.parentNode, + "target": rect}); + } } } - } else if (node.matches && !node.matches("button, select, textarea")) { - node.childNodes.forEach((el) => _highlight(el, addItems, text, className)); + else if (!jQuery(node).is("button, select, textarea")) { + jQuery.each(node.childNodes, function() { + highlight(this, addItems); + }); + } } -}; -const _highlightText = (thisNode, text, className) => { - let addItems = []; - _highlight(thisNode, addItems, text, className); - addItems.forEach((obj) => - obj.parent.insertAdjacentElement("beforebegin", obj.target) - ); + var addItems = []; + var result = this.each(function() { + highlight(this, addItems); + }); + for (var i = 0; i < addItems.length; ++i) { + jQuery(addItems[i].parent).before(addItems[i].target); + } + return result; }; +/* + * backward compatibility for jQuery.browser + * This will be supported until firefox bug is fixed. + */ +if (!jQuery.browser) { + jQuery.uaMatch = function(ua) { + ua = ua.toLowerCase(); + + var match = /(chrome)[ \/]([\w.]+)/.exec(ua) || + /(webkit)[ \/]([\w.]+)/.exec(ua) || + /(opera)(?:.*version|)[ \/]([\w.]+)/.exec(ua) || + /(msie) ([\w.]+)/.exec(ua) || + ua.indexOf("compatible") < 0 && /(mozilla)(?:.*? rv:([\w.]+)|)/.exec(ua) || + []; + + return { + browser: match[ 1 ] || "", + version: match[ 2 ] || "0" + }; + }; + jQuery.browser = {}; + jQuery.browser[jQuery.uaMatch(navigator.userAgent).browser] = true; +} + /** * Small JavaScript module for the documentation. */ -const Documentation = { - init: () => { - Documentation.highlightSearchWords(); - Documentation.initDomainIndexTable(); - Documentation.initOnKeyListeners(); +var Documentation = { + + init : function() { + this.fixFirefoxAnchorBug(); + this.highlightSearchWords(); + this.initIndexTable(); + if (DOCUMENTATION_OPTIONS.NAVIGATION_WITH_KEYS) { + this.initOnKeyListeners(); + } }, /** * i18n support */ - TRANSLATIONS: {}, - PLURAL_EXPR: (n) => (n === 1 ? 0 : 1), - LOCALE: "unknown", + TRANSLATIONS : {}, + PLURAL_EXPR : function(n) { return n === 1 ? 0 : 1; }, + LOCALE : 'unknown', // gettext and ngettext don't access this so that the functions // can safely bound to a different name (_ = Documentation.gettext) - gettext: (string) => { - const translated = Documentation.TRANSLATIONS[string]; - switch (typeof translated) { - case "undefined": - return string; // no translation - case "string": - return translated; // translation exists - default: - return translated[0]; // (singular, plural) translation tuple exists - } + gettext : function(string) { + var translated = Documentation.TRANSLATIONS[string]; + if (typeof translated === 'undefined') + return string; + return (typeof translated === 'string') ? translated : translated[0]; }, - ngettext: (singular, plural, n) => { - const translated = Documentation.TRANSLATIONS[singular]; - if (typeof translated !== "undefined") - return translated[Documentation.PLURAL_EXPR(n)]; - return n === 1 ? singular : plural; + ngettext : function(singular, plural, n) { + var translated = Documentation.TRANSLATIONS[singular]; + if (typeof translated === 'undefined') + return (n == 1) ? singular : plural; + return translated[Documentation.PLURALEXPR(n)]; }, - addTranslations: (catalog) => { - Object.assign(Documentation.TRANSLATIONS, catalog.messages); - Documentation.PLURAL_EXPR = new Function( - "n", - `return (${catalog.plural_expr})` - ); - Documentation.LOCALE = catalog.locale; + addTranslations : function(catalog) { + for (var key in catalog.messages) + this.TRANSLATIONS[key] = catalog.messages[key]; + this.PLURAL_EXPR = new Function('n', 'return +(' + catalog.plural_expr + ')'); + this.LOCALE = catalog.locale; }, /** - * highlight the search words provided in the url in the text + * add context elements like header anchor links */ - highlightSearchWords: () => { - const highlight = - new URLSearchParams(window.location.search).get("highlight") || ""; - const terms = highlight.toLowerCase().split(/\s+/).filter(x => x); - if (terms.length === 0) return; // nothing to do - - // There should never be more than one element matching "div.body" - const divBody = document.querySelectorAll("div.body"); - const body = divBody.length ? divBody[0] : document.querySelector("body"); - window.setTimeout(() => { - terms.forEach((term) => _highlightText(body, term, "highlighted")); - }, 10); - - const searchBox = document.getElementById("searchbox"); - if (searchBox === null) return; - searchBox.appendChild( - document - .createRange() - .createContextualFragment( - '

' + - '' + - Documentation.gettext("Hide Search Matches") + - "

" - ) - ); + addContextElements : function() { + $('div[id] > :header:first').each(function() { + $('\u00B6'). + attr('href', '#' + this.id). + attr('title', _('Permalink to this headline')). + appendTo(this); + }); + $('dt[id]').each(function() { + $('\u00B6'). + attr('href', '#' + this.id). + attr('title', _('Permalink to this definition')). + appendTo(this); + }); }, /** - * helper function to hide the search marks again + * workaround a firefox stupidity + * see: https://bugzilla.mozilla.org/show_bug.cgi?id=645075 */ - hideSearchWords: () => { - document - .querySelectorAll("#searchbox .highlight-link") - .forEach((el) => el.remove()); - document - .querySelectorAll("span.highlighted") - .forEach((el) => el.classList.remove("highlighted")); - const url = new URL(window.location); - url.searchParams.delete("highlight"); - window.history.replaceState({}, "", url); + fixFirefoxAnchorBug : function() { + if (document.location.hash && $.browser.mozilla) + window.setTimeout(function() { + document.location.href += ''; + }, 10); }, /** - * helper function to focus on search bar + * highlight the search words provided in the url in the text */ - focusSearchBar: () => { - document.querySelectorAll("input[name=q]")[0]?.focus(); + highlightSearchWords : function() { + var params = $.getQueryParameters(); + var terms = (params.highlight) ? params.highlight[0].split(/\s+/) : []; + if (terms.length) { + var body = $('div.body'); + if (!body.length) { + body = $('body'); + } + window.setTimeout(function() { + $.each(terms, function() { + body.highlightText(this.toLowerCase(), 'highlighted'); + }); + }, 10); + $('

' + _('Hide Search Matches') + '

') + .appendTo($('#searchbox')); + } }, /** - * Initialise the domain index toggle buttons + * init the domain index toggle buttons */ - initDomainIndexTable: () => { - const toggler = (el) => { - const idNumber = el.id.substr(7); - const toggledRows = document.querySelectorAll(`tr.cg-${idNumber}`); - if (el.src.substr(-9) === "minus.png") { - el.src = `${el.src.substr(0, el.src.length - 9)}plus.png`; - toggledRows.forEach((el) => (el.style.display = "none")); - } else { - el.src = `${el.src.substr(0, el.src.length - 8)}minus.png`; - toggledRows.forEach((el) => (el.style.display = "")); - } - }; - - const togglerElements = document.querySelectorAll("img.toggler"); - togglerElements.forEach((el) => - el.addEventListener("click", (event) => toggler(event.currentTarget)) - ); - togglerElements.forEach((el) => (el.style.display = "")); - if (DOCUMENTATION_OPTIONS.COLLAPSE_INDEX) togglerElements.forEach(toggler); + initIndexTable : function() { + var togglers = $('img.toggler').click(function() { + var src = $(this).attr('src'); + var idnum = $(this).attr('id').substr(7); + $('tr.cg-' + idnum).toggle(); + if (src.substr(-9) === 'minus.png') + $(this).attr('src', src.substr(0, src.length-9) + 'plus.png'); + else + $(this).attr('src', src.substr(0, src.length-8) + 'minus.png'); + }).css('display', ''); + if (DOCUMENTATION_OPTIONS.COLLAPSE_INDEX) { + togglers.click(); + } }, - initOnKeyListeners: () => { - // only install a listener if it is really needed - if ( - !DOCUMENTATION_OPTIONS.NAVIGATION_WITH_KEYS && - !DOCUMENTATION_OPTIONS.ENABLE_SEARCH_SHORTCUTS - ) - return; + /** + * helper function to hide the search marks again + */ + hideSearchWords : function() { + $('#searchbox .highlight-link').fadeOut(300); + $('span.highlighted').removeClass('highlighted'); + var url = new URL(window.location); + url.searchParams.delete('highlight'); + window.history.replaceState({}, '', url); + }, - const blacklistedElements = new Set([ - "TEXTAREA", - "INPUT", - "SELECT", - "BUTTON", - ]); - document.addEventListener("keydown", (event) => { - if (blacklistedElements.has(document.activeElement.tagName)) return; // bail for input elements - if (event.altKey || event.ctrlKey || event.metaKey) return; // bail with special keys + /** + * make the url absolute + */ + makeURL : function(relativeURL) { + return DOCUMENTATION_OPTIONS.URL_ROOT + '/' + relativeURL; + }, - if (!event.shiftKey) { - switch (event.key) { - case "ArrowLeft": - if (!DOCUMENTATION_OPTIONS.NAVIGATION_WITH_KEYS) break; + /** + * get the current relative url + */ + getCurrentURL : function() { + var path = document.location.pathname; + var parts = path.split(/\//); + $.each(DOCUMENTATION_OPTIONS.URL_ROOT.split(/\//), function() { + if (this === '..') + parts.pop(); + }); + var url = parts.join('/'); + return path.substring(url.lastIndexOf('/') + 1, path.length - 1); + }, - const prevLink = document.querySelector('link[rel="prev"]'); - if (prevLink && prevLink.href) { - window.location.href = prevLink.href; - event.preventDefault(); + initOnKeyListeners: function() { + $(document).keydown(function(event) { + var activeElementType = document.activeElement.tagName; + // don't navigate when in search box, textarea, dropdown or button + if (activeElementType !== 'TEXTAREA' && activeElementType !== 'INPUT' && activeElementType !== 'SELECT' + && activeElementType !== 'BUTTON' && !event.altKey && !event.ctrlKey && !event.metaKey + && !event.shiftKey) { + switch (event.keyCode) { + case 37: // left + var prevHref = $('link[rel="prev"]').prop('href'); + if (prevHref) { + window.location.href = prevHref; + return false; } break; - case "ArrowRight": - if (!DOCUMENTATION_OPTIONS.NAVIGATION_WITH_KEYS) break; - - const nextLink = document.querySelector('link[rel="next"]'); - if (nextLink && nextLink.href) { - window.location.href = nextLink.href; - event.preventDefault(); + case 39: // right + var nextHref = $('link[rel="next"]').prop('href'); + if (nextHref) { + window.location.href = nextHref; + return false; } break; - case "Escape": - if (!DOCUMENTATION_OPTIONS.ENABLE_SEARCH_SHORTCUTS) break; - Documentation.hideSearchWords(); - event.preventDefault(); } } - - // some keyboard layouts may need Shift to get / - switch (event.key) { - case "/": - if (!DOCUMENTATION_OPTIONS.ENABLE_SEARCH_SHORTCUTS) break; - Documentation.focusSearchBar(); - event.preventDefault(); - } }); - }, + } }; // quick alias for translations -const _ = Documentation.gettext; +_ = Documentation.gettext; -_ready(Documentation.init); +$(document).ready(function() { + Documentation.init(); +}); diff --git a/_static/documentation_options.js b/_static/documentation_options.js index ca5f05e1..8839ac8c 100644 --- a/_static/documentation_options.js +++ b/_static/documentation_options.js @@ -1,14 +1,12 @@ var DOCUMENTATION_OPTIONS = { URL_ROOT: document.getElementById("documentation_options").getAttribute('data-url_root'), VERSION: '0.1', - LANGUAGE: 'en', + LANGUAGE: 'None', COLLAPSE_INDEX: false, BUILDER: 'html', FILE_SUFFIX: '.html', LINK_SUFFIX: '.html', HAS_SOURCE: true, SOURCELINK_SUFFIX: '.txt', - NAVIGATION_WITH_KEYS: false, - SHOW_SEARCH_SUMMARY: true, - ENABLE_SEARCH_SHORTCUTS: false, + NAVIGATION_WITH_KEYS: false }; \ No newline at end of file diff --git a/_static/jquery-3.6.0.js b/_static/jquery-3.5.1.js similarity index 98% rename from _static/jquery-3.6.0.js rename to _static/jquery-3.5.1.js index fc6c299b..50937333 100644 --- a/_static/jquery-3.6.0.js +++ b/_static/jquery-3.5.1.js @@ -1,15 +1,15 @@ /*! - * jQuery JavaScript Library v3.6.0 + * jQuery JavaScript Library v3.5.1 * https://jquery.com/ * * Includes Sizzle.js * https://sizzlejs.com/ * - * Copyright OpenJS Foundation and other contributors + * Copyright JS Foundation and other contributors * Released under the MIT license * https://jquery.org/license * - * Date: 2021-03-02T17:08Z + * Date: 2020-05-04T22:49Z */ ( function( global, factory ) { @@ -76,16 +76,12 @@ var support = {}; var isFunction = function isFunction( obj ) { - // Support: Chrome <=57, Firefox <=52 - // In some browsers, typeof returns "function" for HTML elements - // (i.e., `typeof document.createElement( "object" ) === "function"`). - // We don't want to classify *any* DOM node as a function. - // Support: QtWeb <=3.8.5, WebKit <=534.34, wkhtmltopdf tool <=0.12.5 - // Plus for old WebKit, typeof returns "function" for HTML collections - // (e.g., `typeof document.getElementsByTagName("div") === "function"`). (gh-4756) - return typeof obj === "function" && typeof obj.nodeType !== "number" && - typeof obj.item !== "function"; - }; + // Support: Chrome <=57, Firefox <=52 + // In some browsers, typeof returns "function" for HTML elements + // (i.e., `typeof document.createElement( "object" ) === "function"`). + // We don't want to classify *any* DOM node as a function. + return typeof obj === "function" && typeof obj.nodeType !== "number"; + }; var isWindow = function isWindow( obj ) { @@ -151,7 +147,7 @@ function toType( obj ) { var - version = "3.6.0", + version = "3.5.1", // Define a local copy of jQuery jQuery = function( selector, context ) { @@ -405,7 +401,7 @@ jQuery.extend( { if ( isArrayLike( Object( arr ) ) ) { jQuery.merge( ret, typeof arr === "string" ? - [ arr ] : arr + [ arr ] : arr ); } else { push.call( ret, arr ); @@ -500,9 +496,9 @@ if ( typeof Symbol === "function" ) { // Populate the class2type map jQuery.each( "Boolean Number String Function Array Date RegExp Object Error Symbol".split( " " ), - function( _i, name ) { - class2type[ "[object " + name + "]" ] = name.toLowerCase(); - } ); +function( _i, name ) { + class2type[ "[object " + name + "]" ] = name.toLowerCase(); +} ); function isArrayLike( obj ) { @@ -522,14 +518,14 @@ function isArrayLike( obj ) { } var Sizzle = /*! - * Sizzle CSS Selector Engine v2.3.6 + * Sizzle CSS Selector Engine v2.3.5 * https://sizzlejs.com/ * * Copyright JS Foundation and other contributors * Released under the MIT license * https://js.foundation/ * - * Date: 2021-02-16 + * Date: 2020-03-14 */ ( function( window ) { var i, @@ -1112,8 +1108,8 @@ support = Sizzle.support = {}; * @returns {Boolean} True iff elem is a non-HTML XML node */ isXML = Sizzle.isXML = function( elem ) { - var namespace = elem && elem.namespaceURI, - docElem = elem && ( elem.ownerDocument || elem ).documentElement; + var namespace = elem.namespaceURI, + docElem = ( elem.ownerDocument || elem ).documentElement; // Support: IE <=8 // Assume HTML when documentElement doesn't yet exist, such as inside loading iframes @@ -3028,9 +3024,9 @@ var rneedsContext = jQuery.expr.match.needsContext; function nodeName( elem, name ) { - return elem.nodeName && elem.nodeName.toLowerCase() === name.toLowerCase(); + return elem.nodeName && elem.nodeName.toLowerCase() === name.toLowerCase(); -} +}; var rsingleTag = ( /^<([a-z][^\/\0>:\x20\t\r\n\f]*)[\x20\t\r\n\f]*\/?>(?:<\/\1>|)$/i ); @@ -4001,8 +3997,8 @@ jQuery.extend( { resolveContexts = Array( i ), resolveValues = slice.call( arguments ), - // the primary Deferred - primary = jQuery.Deferred(), + // the master Deferred + master = jQuery.Deferred(), // subordinate callback factory updateFunc = function( i ) { @@ -4010,30 +4006,30 @@ jQuery.extend( { resolveContexts[ i ] = this; resolveValues[ i ] = arguments.length > 1 ? slice.call( arguments ) : value; if ( !( --remaining ) ) { - primary.resolveWith( resolveContexts, resolveValues ); + master.resolveWith( resolveContexts, resolveValues ); } }; }; // Single- and empty arguments are adopted like Promise.resolve if ( remaining <= 1 ) { - adoptValue( singleValue, primary.done( updateFunc( i ) ).resolve, primary.reject, + adoptValue( singleValue, master.done( updateFunc( i ) ).resolve, master.reject, !remaining ); // Use .then() to unwrap secondary thenables (cf. gh-3000) - if ( primary.state() === "pending" || + if ( master.state() === "pending" || isFunction( resolveValues[ i ] && resolveValues[ i ].then ) ) { - return primary.then(); + return master.then(); } } // Multiple arguments are aggregated like Promise.all array elements while ( i-- ) { - adoptValue( resolveValues[ i ], updateFunc( i ), primary.reject ); + adoptValue( resolveValues[ i ], updateFunc( i ), master.reject ); } - return primary.promise(); + return master.promise(); } } ); @@ -4184,8 +4180,8 @@ var access = function( elems, fn, key, value, chainable, emptyGet, raw ) { for ( ; i < len; i++ ) { fn( elems[ i ], key, raw ? - value : - value.call( elems[ i ], i, fn( elems[ i ], key ) ) + value : + value.call( elems[ i ], i, fn( elems[ i ], key ) ) ); } } @@ -5093,7 +5089,10 @@ function buildFragment( elems, context, scripts, selection, ignored ) { } -var rtypenamespace = /^([^.]*)(?:\.(.+)|)/; +var + rkeyEvent = /^key/, + rmouseEvent = /^(?:mouse|pointer|contextmenu|drag|drop)|click/, + rtypenamespace = /^([^.]*)(?:\.(.+)|)/; function returnTrue() { return true; @@ -5388,8 +5387,8 @@ jQuery.event = { event = jQuery.event.fix( nativeEvent ), handlers = ( - dataPriv.get( this, "events" ) || Object.create( null ) - )[ event.type ] || [], + dataPriv.get( this, "events" ) || Object.create( null ) + )[ event.type ] || [], special = jQuery.event.special[ event.type ] || {}; // Use the fix-ed jQuery.Event rather than the (read-only) native event @@ -5513,12 +5512,12 @@ jQuery.event = { get: isFunction( hook ) ? function() { if ( this.originalEvent ) { - return hook( this.originalEvent ); + return hook( this.originalEvent ); } } : function() { if ( this.originalEvent ) { - return this.originalEvent[ name ]; + return this.originalEvent[ name ]; } }, @@ -5657,13 +5656,7 @@ function leverageNative( el, type, expectSync ) { // Cancel the outer synthetic event event.stopImmediatePropagation(); event.preventDefault(); - - // Support: Chrome 86+ - // In Chrome, if an element having a focusout handler is blurred by - // clicking outside of it, it invokes the handler synchronously. If - // that handler calls `.remove()` on the element, the data is cleared, - // leaving `result` undefined. We need to guard against this. - return result && result.value; + return result.value; } // If this is an inner synthetic event for an event with a bubbling surrogate @@ -5828,7 +5821,34 @@ jQuery.each( { targetTouches: true, toElement: true, touches: true, - which: true + + which: function( event ) { + var button = event.button; + + // Add which for key events + if ( event.which == null && rkeyEvent.test( event.type ) ) { + return event.charCode != null ? event.charCode : event.keyCode; + } + + // Add which for click: 1 === left; 2 === middle; 3 === right + if ( !event.which && button !== undefined && rmouseEvent.test( event.type ) ) { + if ( button & 1 ) { + return 1; + } + + if ( button & 2 ) { + return 3; + } + + if ( button & 4 ) { + return 2; + } + + return 0; + } + + return event.which; + } }, jQuery.event.addProp ); jQuery.each( { focus: "focusin", blur: "focusout" }, function( type, delegateType ) { @@ -5854,12 +5874,6 @@ jQuery.each( { focus: "focusin", blur: "focusout" }, function( type, delegateTyp return true; }, - // Suppress native focus or blur as it's already being fired - // in leverageNative. - _default: function() { - return true; - }, - delegateType: delegateType }; } ); @@ -6527,10 +6541,6 @@ var rboxStyle = new RegExp( cssExpand.join( "|" ), "i" ); // set in CSS while `offset*` properties report correct values. // Behavior in IE 9 is more subtle than in newer versions & it passes // some versions of this test; make sure not to make it pass there! - // - // Support: Firefox 70+ - // Only Firefox includes border widths - // in computed dimensions. (gh-4529) reliableTrDimensions: function() { var table, tr, trChild, trStyle; if ( reliableTrDimensionsVal == null ) { @@ -6538,32 +6548,17 @@ var rboxStyle = new RegExp( cssExpand.join( "|" ), "i" ); tr = document.createElement( "tr" ); trChild = document.createElement( "div" ); - table.style.cssText = "position:absolute;left:-11111px;border-collapse:separate"; - tr.style.cssText = "border:1px solid"; - - // Support: Chrome 86+ - // Height set through cssText does not get applied. - // Computed height then comes back as 0. + table.style.cssText = "position:absolute;left:-11111px"; tr.style.height = "1px"; trChild.style.height = "9px"; - // Support: Android 8 Chrome 86+ - // In our bodyBackground.html iframe, - // display for all div elements is set to "inline", - // which causes a problem only in Android 8 Chrome 86. - // Ensuring the div is display: block - // gets around this issue. - trChild.style.display = "block"; - documentElement .appendChild( table ) .appendChild( tr ) .appendChild( trChild ); trStyle = window.getComputedStyle( tr ); - reliableTrDimensionsVal = ( parseInt( trStyle.height, 10 ) + - parseInt( trStyle.borderTopWidth, 10 ) + - parseInt( trStyle.borderBottomWidth, 10 ) ) === tr.offsetHeight; + reliableTrDimensionsVal = parseInt( trStyle.height ) > 3; documentElement.removeChild( table ); } @@ -7027,10 +7022,10 @@ jQuery.each( [ "height", "width" ], function( _i, dimension ) { // Running getBoundingClientRect on a disconnected node // in IE throws an error. ( !elem.getClientRects().length || !elem.getBoundingClientRect().width ) ? - swap( elem, cssShow, function() { - return getWidthOrHeight( elem, dimension, extra ); - } ) : - getWidthOrHeight( elem, dimension, extra ); + swap( elem, cssShow, function() { + return getWidthOrHeight( elem, dimension, extra ); + } ) : + getWidthOrHeight( elem, dimension, extra ); } }, @@ -7089,7 +7084,7 @@ jQuery.cssHooks.marginLeft = addGetHookIf( support.reliableMarginLeft, swap( elem, { marginLeft: 0 }, function() { return elem.getBoundingClientRect().left; } ) - ) + "px"; + ) + "px"; } } ); @@ -7228,7 +7223,7 @@ Tween.propHooks = { if ( jQuery.fx.step[ tween.prop ] ) { jQuery.fx.step[ tween.prop ]( tween ); } else if ( tween.elem.nodeType === 1 && ( - jQuery.cssHooks[ tween.prop ] || + jQuery.cssHooks[ tween.prop ] || tween.elem.style[ finalPropName( tween.prop ) ] != null ) ) { jQuery.style( tween.elem, tween.prop, tween.now + tween.unit ); } else { @@ -7473,7 +7468,7 @@ function defaultPrefilter( elem, props, opts ) { anim.done( function() { - /* eslint-enable no-loop-func */ + /* eslint-enable no-loop-func */ // The final step of a "hide" animation is actually hiding the element if ( !hidden ) { @@ -7593,7 +7588,7 @@ function Animation( elem, properties, options ) { tweens: [], createTween: function( prop, end ) { var tween = jQuery.Tween( elem, animation.opts, prop, end, - animation.opts.specialEasing[ prop ] || animation.opts.easing ); + animation.opts.specialEasing[ prop ] || animation.opts.easing ); animation.tweens.push( tween ); return tween; }, @@ -7766,8 +7761,7 @@ jQuery.fn.extend( { anim.stop( true ); } }; - - doAnimation.finish = doAnimation; + doAnimation.finish = doAnimation; return empty || optall.queue === false ? this.each( doAnimation ) : @@ -8407,8 +8401,8 @@ jQuery.fn.extend( { if ( this.setAttribute ) { this.setAttribute( "class", className || value === false ? - "" : - dataPriv.get( this, "__className__" ) || "" + "" : + dataPriv.get( this, "__className__" ) || "" ); } } @@ -8423,7 +8417,7 @@ jQuery.fn.extend( { while ( ( elem = this[ i++ ] ) ) { if ( elem.nodeType === 1 && ( " " + stripAndCollapse( getClass( elem ) ) + " " ).indexOf( className ) > -1 ) { - return true; + return true; } } @@ -8713,7 +8707,9 @@ jQuery.extend( jQuery.event, { special.bindType || type; // jQuery handler - handle = ( dataPriv.get( cur, "events" ) || Object.create( null ) )[ event.type ] && + handle = ( + dataPriv.get( cur, "events" ) || Object.create( null ) + )[ event.type ] && dataPriv.get( cur, "handle" ); if ( handle ) { handle.apply( cur, data ); @@ -8860,7 +8856,7 @@ var rquery = ( /\?/ ); // Cross-browser xml parsing jQuery.parseXML = function( data ) { - var xml, parserErrorElem; + var xml; if ( !data || typeof data !== "string" ) { return null; } @@ -8869,17 +8865,12 @@ jQuery.parseXML = function( data ) { // IE throws on parseFromString with invalid input. try { xml = ( new window.DOMParser() ).parseFromString( data, "text/xml" ); - } catch ( e ) {} + } catch ( e ) { + xml = undefined; + } - parserErrorElem = xml && xml.getElementsByTagName( "parsererror" )[ 0 ]; - if ( !xml || parserErrorElem ) { - jQuery.error( "Invalid XML: " + ( - parserErrorElem ? - jQuery.map( parserErrorElem.childNodes, function( el ) { - return el.textContent; - } ).join( "\n" ) : - data - ) ); + if ( !xml || xml.getElementsByTagName( "parsererror" ).length ) { + jQuery.error( "Invalid XML: " + data ); } return xml; }; @@ -8980,14 +8971,16 @@ jQuery.fn.extend( { // Can add propHook for "elements" to filter or add form elements var elements = jQuery.prop( this, "elements" ); return elements ? jQuery.makeArray( elements ) : this; - } ).filter( function() { + } ) + .filter( function() { var type = this.type; // Use .is( ":disabled" ) so that fieldset[disabled] works return this.name && !jQuery( this ).is( ":disabled" ) && rsubmittable.test( this.nodeName ) && !rsubmitterTypes.test( type ) && ( this.checked || !rcheckableType.test( type ) ); - } ).map( function( _i, elem ) { + } ) + .map( function( _i, elem ) { var val = jQuery( this ).val(); if ( val == null ) { @@ -9040,8 +9033,7 @@ var // Anchor tag for parsing the document origin originAnchor = document.createElement( "a" ); - -originAnchor.href = location.href; + originAnchor.href = location.href; // Base "constructor" for jQuery.ajaxPrefilter and jQuery.ajaxTransport function addToPrefiltersOrTransports( structure ) { @@ -9422,8 +9414,8 @@ jQuery.extend( { // Context for global events is callbackContext if it is a DOM node or jQuery collection globalEventContext = s.context && ( callbackContext.nodeType || callbackContext.jquery ) ? - jQuery( callbackContext ) : - jQuery.event, + jQuery( callbackContext ) : + jQuery.event, // Deferreds deferred = jQuery.Deferred(), @@ -9735,10 +9727,8 @@ jQuery.extend( { response = ajaxHandleResponses( s, jqXHR, responses ); } - // Use a noop converter for missing script but not if jsonp - if ( !isSuccess && - jQuery.inArray( "script", s.dataTypes ) > -1 && - jQuery.inArray( "json", s.dataTypes ) < 0 ) { + // Use a noop converter for missing script + if ( !isSuccess && jQuery.inArray( "script", s.dataTypes ) > -1 ) { s.converters[ "text script" ] = function() {}; } @@ -10476,6 +10466,12 @@ jQuery.offset = { options.using.call( elem, props ); } else { + if ( typeof props.top === "number" ) { + props.top += "px"; + } + if ( typeof props.left === "number" ) { + props.left += "px"; + } curElem.css( props ); } } @@ -10644,11 +10640,8 @@ jQuery.each( [ "top", "left" ], function( _i, prop ) { // Create innerHeight, innerWidth, height, width, outerHeight and outerWidth methods jQuery.each( { Height: "height", Width: "width" }, function( name, type ) { - jQuery.each( { - padding: "inner" + name, - content: type, - "": "outer" + name - }, function( defaultExtra, funcName ) { + jQuery.each( { padding: "inner" + name, content: type, "": "outer" + name }, + function( defaultExtra, funcName ) { // Margin is only for outerHeight, outerWidth jQuery.fn[ funcName ] = function( margin, value ) { @@ -10733,8 +10726,7 @@ jQuery.fn.extend( { } } ); -jQuery.each( - ( "blur focus focusin focusout resize scroll click dblclick " + +jQuery.each( ( "blur focus focusin focusout resize scroll click dblclick " + "mousedown mouseup mousemove mouseover mouseout mouseenter mouseleave " + "change select submit keydown keypress keyup contextmenu" ).split( " " ), function( _i, name ) { @@ -10745,8 +10737,7 @@ jQuery.each( this.on( name, null, data, fn ) : this.trigger( name ); }; - } -); + } ); diff --git a/_static/jquery.js b/_static/jquery.js index c4c6022f..b0614034 100644 --- a/_static/jquery.js +++ b/_static/jquery.js @@ -1,2 +1,2 @@ -/*! jQuery v3.6.0 | (c) OpenJS Foundation and other contributors | jquery.org/license */ -!function(e,t){"use strict";"object"==typeof module&&"object"==typeof module.exports?module.exports=e.document?t(e,!0):function(e){if(!e.document)throw new Error("jQuery requires a window with a document");return t(e)}:t(e)}("undefined"!=typeof window?window:this,function(C,e){"use strict";var t=[],r=Object.getPrototypeOf,s=t.slice,g=t.flat?function(e){return t.flat.call(e)}:function(e){return t.concat.apply([],e)},u=t.push,i=t.indexOf,n={},o=n.toString,v=n.hasOwnProperty,a=v.toString,l=a.call(Object),y={},m=function(e){return"function"==typeof e&&"number"!=typeof e.nodeType&&"function"!=typeof e.item},x=function(e){return null!=e&&e===e.window},E=C.document,c={type:!0,src:!0,nonce:!0,noModule:!0};function b(e,t,n){var r,i,o=(n=n||E).createElement("script");if(o.text=e,t)for(r in c)(i=t[r]||t.getAttribute&&t.getAttribute(r))&&o.setAttribute(r,i);n.head.appendChild(o).parentNode.removeChild(o)}function w(e){return null==e?e+"":"object"==typeof e||"function"==typeof e?n[o.call(e)]||"object":typeof e}var f="3.6.0",S=function(e,t){return new S.fn.init(e,t)};function p(e){var t=!!e&&"length"in e&&e.length,n=w(e);return!m(e)&&!x(e)&&("array"===n||0===t||"number"==typeof t&&0+~]|"+M+")"+M+"*"),U=new RegExp(M+"|>"),X=new RegExp(F),V=new RegExp("^"+I+"$"),G={ID:new RegExp("^#("+I+")"),CLASS:new RegExp("^\\.("+I+")"),TAG:new RegExp("^("+I+"|[*])"),ATTR:new RegExp("^"+W),PSEUDO:new RegExp("^"+F),CHILD:new RegExp("^:(only|first|last|nth|nth-last)-(child|of-type)(?:\\("+M+"*(even|odd|(([+-]|)(\\d*)n|)"+M+"*(?:([+-]|)"+M+"*(\\d+)|))"+M+"*\\)|)","i"),bool:new RegExp("^(?:"+R+")$","i"),needsContext:new RegExp("^"+M+"*[>+~]|:(even|odd|eq|gt|lt|nth|first|last)(?:\\("+M+"*((?:-\\d)?\\d*)"+M+"*\\)|)(?=[^-]|$)","i")},Y=/HTML$/i,Q=/^(?:input|select|textarea|button)$/i,J=/^h\d$/i,K=/^[^{]+\{\s*\[native \w/,Z=/^(?:#([\w-]+)|(\w+)|\.([\w-]+))$/,ee=/[+~]/,te=new RegExp("\\\\[\\da-fA-F]{1,6}"+M+"?|\\\\([^\\r\\n\\f])","g"),ne=function(e,t){var n="0x"+e.slice(1)-65536;return t||(n<0?String.fromCharCode(n+65536):String.fromCharCode(n>>10|55296,1023&n|56320))},re=/([\0-\x1f\x7f]|^-?\d)|^-$|[^\0-\x1f\x7f-\uFFFF\w-]/g,ie=function(e,t){return t?"\0"===e?"\ufffd":e.slice(0,-1)+"\\"+e.charCodeAt(e.length-1).toString(16)+" ":"\\"+e},oe=function(){T()},ae=be(function(e){return!0===e.disabled&&"fieldset"===e.nodeName.toLowerCase()},{dir:"parentNode",next:"legend"});try{H.apply(t=O.call(p.childNodes),p.childNodes),t[p.childNodes.length].nodeType}catch(e){H={apply:t.length?function(e,t){L.apply(e,O.call(t))}:function(e,t){var n=e.length,r=0;while(e[n++]=t[r++]);e.length=n-1}}}function se(t,e,n,r){var i,o,a,s,u,l,c,f=e&&e.ownerDocument,p=e?e.nodeType:9;if(n=n||[],"string"!=typeof t||!t||1!==p&&9!==p&&11!==p)return n;if(!r&&(T(e),e=e||C,E)){if(11!==p&&(u=Z.exec(t)))if(i=u[1]){if(9===p){if(!(a=e.getElementById(i)))return n;if(a.id===i)return n.push(a),n}else if(f&&(a=f.getElementById(i))&&y(e,a)&&a.id===i)return n.push(a),n}else{if(u[2])return H.apply(n,e.getElementsByTagName(t)),n;if((i=u[3])&&d.getElementsByClassName&&e.getElementsByClassName)return H.apply(n,e.getElementsByClassName(i)),n}if(d.qsa&&!N[t+" "]&&(!v||!v.test(t))&&(1!==p||"object"!==e.nodeName.toLowerCase())){if(c=t,f=e,1===p&&(U.test(t)||z.test(t))){(f=ee.test(t)&&ye(e.parentNode)||e)===e&&d.scope||((s=e.getAttribute("id"))?s=s.replace(re,ie):e.setAttribute("id",s=S)),o=(l=h(t)).length;while(o--)l[o]=(s?"#"+s:":scope")+" "+xe(l[o]);c=l.join(",")}try{return H.apply(n,f.querySelectorAll(c)),n}catch(e){N(t,!0)}finally{s===S&&e.removeAttribute("id")}}}return g(t.replace($,"$1"),e,n,r)}function ue(){var r=[];return function e(t,n){return r.push(t+" ")>b.cacheLength&&delete e[r.shift()],e[t+" "]=n}}function le(e){return e[S]=!0,e}function ce(e){var t=C.createElement("fieldset");try{return!!e(t)}catch(e){return!1}finally{t.parentNode&&t.parentNode.removeChild(t),t=null}}function fe(e,t){var n=e.split("|"),r=n.length;while(r--)b.attrHandle[n[r]]=t}function pe(e,t){var n=t&&e,r=n&&1===e.nodeType&&1===t.nodeType&&e.sourceIndex-t.sourceIndex;if(r)return r;if(n)while(n=n.nextSibling)if(n===t)return-1;return e?1:-1}function de(t){return function(e){return"input"===e.nodeName.toLowerCase()&&e.type===t}}function he(n){return function(e){var t=e.nodeName.toLowerCase();return("input"===t||"button"===t)&&e.type===n}}function ge(t){return function(e){return"form"in e?e.parentNode&&!1===e.disabled?"label"in e?"label"in e.parentNode?e.parentNode.disabled===t:e.disabled===t:e.isDisabled===t||e.isDisabled!==!t&&ae(e)===t:e.disabled===t:"label"in e&&e.disabled===t}}function ve(a){return le(function(o){return o=+o,le(function(e,t){var n,r=a([],e.length,o),i=r.length;while(i--)e[n=r[i]]&&(e[n]=!(t[n]=e[n]))})})}function ye(e){return e&&"undefined"!=typeof e.getElementsByTagName&&e}for(e in d=se.support={},i=se.isXML=function(e){var t=e&&e.namespaceURI,n=e&&(e.ownerDocument||e).documentElement;return!Y.test(t||n&&n.nodeName||"HTML")},T=se.setDocument=function(e){var t,n,r=e?e.ownerDocument||e:p;return r!=C&&9===r.nodeType&&r.documentElement&&(a=(C=r).documentElement,E=!i(C),p!=C&&(n=C.defaultView)&&n.top!==n&&(n.addEventListener?n.addEventListener("unload",oe,!1):n.attachEvent&&n.attachEvent("onunload",oe)),d.scope=ce(function(e){return a.appendChild(e).appendChild(C.createElement("div")),"undefined"!=typeof e.querySelectorAll&&!e.querySelectorAll(":scope fieldset div").length}),d.attributes=ce(function(e){return e.className="i",!e.getAttribute("className")}),d.getElementsByTagName=ce(function(e){return e.appendChild(C.createComment("")),!e.getElementsByTagName("*").length}),d.getElementsByClassName=K.test(C.getElementsByClassName),d.getById=ce(function(e){return a.appendChild(e).id=S,!C.getElementsByName||!C.getElementsByName(S).length}),d.getById?(b.filter.ID=function(e){var t=e.replace(te,ne);return function(e){return e.getAttribute("id")===t}},b.find.ID=function(e,t){if("undefined"!=typeof t.getElementById&&E){var n=t.getElementById(e);return n?[n]:[]}}):(b.filter.ID=function(e){var n=e.replace(te,ne);return function(e){var t="undefined"!=typeof e.getAttributeNode&&e.getAttributeNode("id");return t&&t.value===n}},b.find.ID=function(e,t){if("undefined"!=typeof t.getElementById&&E){var n,r,i,o=t.getElementById(e);if(o){if((n=o.getAttributeNode("id"))&&n.value===e)return[o];i=t.getElementsByName(e),r=0;while(o=i[r++])if((n=o.getAttributeNode("id"))&&n.value===e)return[o]}return[]}}),b.find.TAG=d.getElementsByTagName?function(e,t){return"undefined"!=typeof t.getElementsByTagName?t.getElementsByTagName(e):d.qsa?t.querySelectorAll(e):void 0}:function(e,t){var n,r=[],i=0,o=t.getElementsByTagName(e);if("*"===e){while(n=o[i++])1===n.nodeType&&r.push(n);return r}return o},b.find.CLASS=d.getElementsByClassName&&function(e,t){if("undefined"!=typeof t.getElementsByClassName&&E)return t.getElementsByClassName(e)},s=[],v=[],(d.qsa=K.test(C.querySelectorAll))&&(ce(function(e){var t;a.appendChild(e).innerHTML="",e.querySelectorAll("[msallowcapture^='']").length&&v.push("[*^$]="+M+"*(?:''|\"\")"),e.querySelectorAll("[selected]").length||v.push("\\["+M+"*(?:value|"+R+")"),e.querySelectorAll("[id~="+S+"-]").length||v.push("~="),(t=C.createElement("input")).setAttribute("name",""),e.appendChild(t),e.querySelectorAll("[name='']").length||v.push("\\["+M+"*name"+M+"*="+M+"*(?:''|\"\")"),e.querySelectorAll(":checked").length||v.push(":checked"),e.querySelectorAll("a#"+S+"+*").length||v.push(".#.+[+~]"),e.querySelectorAll("\\\f"),v.push("[\\r\\n\\f]")}),ce(function(e){e.innerHTML="";var t=C.createElement("input");t.setAttribute("type","hidden"),e.appendChild(t).setAttribute("name","D"),e.querySelectorAll("[name=d]").length&&v.push("name"+M+"*[*^$|!~]?="),2!==e.querySelectorAll(":enabled").length&&v.push(":enabled",":disabled"),a.appendChild(e).disabled=!0,2!==e.querySelectorAll(":disabled").length&&v.push(":enabled",":disabled"),e.querySelectorAll("*,:x"),v.push(",.*:")})),(d.matchesSelector=K.test(c=a.matches||a.webkitMatchesSelector||a.mozMatchesSelector||a.oMatchesSelector||a.msMatchesSelector))&&ce(function(e){d.disconnectedMatch=c.call(e,"*"),c.call(e,"[s!='']:x"),s.push("!=",F)}),v=v.length&&new RegExp(v.join("|")),s=s.length&&new RegExp(s.join("|")),t=K.test(a.compareDocumentPosition),y=t||K.test(a.contains)?function(e,t){var n=9===e.nodeType?e.documentElement:e,r=t&&t.parentNode;return e===r||!(!r||1!==r.nodeType||!(n.contains?n.contains(r):e.compareDocumentPosition&&16&e.compareDocumentPosition(r)))}:function(e,t){if(t)while(t=t.parentNode)if(t===e)return!0;return!1},j=t?function(e,t){if(e===t)return l=!0,0;var n=!e.compareDocumentPosition-!t.compareDocumentPosition;return n||(1&(n=(e.ownerDocument||e)==(t.ownerDocument||t)?e.compareDocumentPosition(t):1)||!d.sortDetached&&t.compareDocumentPosition(e)===n?e==C||e.ownerDocument==p&&y(p,e)?-1:t==C||t.ownerDocument==p&&y(p,t)?1:u?P(u,e)-P(u,t):0:4&n?-1:1)}:function(e,t){if(e===t)return l=!0,0;var n,r=0,i=e.parentNode,o=t.parentNode,a=[e],s=[t];if(!i||!o)return e==C?-1:t==C?1:i?-1:o?1:u?P(u,e)-P(u,t):0;if(i===o)return pe(e,t);n=e;while(n=n.parentNode)a.unshift(n);n=t;while(n=n.parentNode)s.unshift(n);while(a[r]===s[r])r++;return r?pe(a[r],s[r]):a[r]==p?-1:s[r]==p?1:0}),C},se.matches=function(e,t){return se(e,null,null,t)},se.matchesSelector=function(e,t){if(T(e),d.matchesSelector&&E&&!N[t+" "]&&(!s||!s.test(t))&&(!v||!v.test(t)))try{var n=c.call(e,t);if(n||d.disconnectedMatch||e.document&&11!==e.document.nodeType)return n}catch(e){N(t,!0)}return 0":{dir:"parentNode",first:!0}," ":{dir:"parentNode"},"+":{dir:"previousSibling",first:!0},"~":{dir:"previousSibling"}},preFilter:{ATTR:function(e){return e[1]=e[1].replace(te,ne),e[3]=(e[3]||e[4]||e[5]||"").replace(te,ne),"~="===e[2]&&(e[3]=" "+e[3]+" "),e.slice(0,4)},CHILD:function(e){return e[1]=e[1].toLowerCase(),"nth"===e[1].slice(0,3)?(e[3]||se.error(e[0]),e[4]=+(e[4]?e[5]+(e[6]||1):2*("even"===e[3]||"odd"===e[3])),e[5]=+(e[7]+e[8]||"odd"===e[3])):e[3]&&se.error(e[0]),e},PSEUDO:function(e){var t,n=!e[6]&&e[2];return G.CHILD.test(e[0])?null:(e[3]?e[2]=e[4]||e[5]||"":n&&X.test(n)&&(t=h(n,!0))&&(t=n.indexOf(")",n.length-t)-n.length)&&(e[0]=e[0].slice(0,t),e[2]=n.slice(0,t)),e.slice(0,3))}},filter:{TAG:function(e){var t=e.replace(te,ne).toLowerCase();return"*"===e?function(){return!0}:function(e){return e.nodeName&&e.nodeName.toLowerCase()===t}},CLASS:function(e){var t=m[e+" "];return t||(t=new RegExp("(^|"+M+")"+e+"("+M+"|$)"))&&m(e,function(e){return t.test("string"==typeof e.className&&e.className||"undefined"!=typeof e.getAttribute&&e.getAttribute("class")||"")})},ATTR:function(n,r,i){return function(e){var t=se.attr(e,n);return null==t?"!="===r:!r||(t+="","="===r?t===i:"!="===r?t!==i:"^="===r?i&&0===t.indexOf(i):"*="===r?i&&-1:\x20\t\r\n\f]*)[\x20\t\r\n\f]*\/?>(?:<\/\1>|)$/i;function j(e,n,r){return m(n)?S.grep(e,function(e,t){return!!n.call(e,t,e)!==r}):n.nodeType?S.grep(e,function(e){return e===n!==r}):"string"!=typeof n?S.grep(e,function(e){return-1)[^>]*|#([\w-]+))$/;(S.fn.init=function(e,t,n){var r,i;if(!e)return this;if(n=n||D,"string"==typeof e){if(!(r="<"===e[0]&&">"===e[e.length-1]&&3<=e.length?[null,e,null]:q.exec(e))||!r[1]&&t)return!t||t.jquery?(t||n).find(e):this.constructor(t).find(e);if(r[1]){if(t=t instanceof S?t[0]:t,S.merge(this,S.parseHTML(r[1],t&&t.nodeType?t.ownerDocument||t:E,!0)),N.test(r[1])&&S.isPlainObject(t))for(r in t)m(this[r])?this[r](t[r]):this.attr(r,t[r]);return this}return(i=E.getElementById(r[2]))&&(this[0]=i,this.length=1),this}return e.nodeType?(this[0]=e,this.length=1,this):m(e)?void 0!==n.ready?n.ready(e):e(S):S.makeArray(e,this)}).prototype=S.fn,D=S(E);var L=/^(?:parents|prev(?:Until|All))/,H={children:!0,contents:!0,next:!0,prev:!0};function O(e,t){while((e=e[t])&&1!==e.nodeType);return e}S.fn.extend({has:function(e){var t=S(e,this),n=t.length;return this.filter(function(){for(var e=0;e\x20\t\r\n\f]*)/i,he=/^$|^module$|\/(?:java|ecma)script/i;ce=E.createDocumentFragment().appendChild(E.createElement("div")),(fe=E.createElement("input")).setAttribute("type","radio"),fe.setAttribute("checked","checked"),fe.setAttribute("name","t"),ce.appendChild(fe),y.checkClone=ce.cloneNode(!0).cloneNode(!0).lastChild.checked,ce.innerHTML="",y.noCloneChecked=!!ce.cloneNode(!0).lastChild.defaultValue,ce.innerHTML="",y.option=!!ce.lastChild;var ge={thead:[1,"","
"],col:[2,"","
"],tr:[2,"","
"],td:[3,"","
"],_default:[0,"",""]};function ve(e,t){var n;return n="undefined"!=typeof e.getElementsByTagName?e.getElementsByTagName(t||"*"):"undefined"!=typeof e.querySelectorAll?e.querySelectorAll(t||"*"):[],void 0===t||t&&A(e,t)?S.merge([e],n):n}function ye(e,t){for(var n=0,r=e.length;n",""]);var me=/<|&#?\w+;/;function xe(e,t,n,r,i){for(var o,a,s,u,l,c,f=t.createDocumentFragment(),p=[],d=0,h=e.length;d\s*$/g;function je(e,t){return A(e,"table")&&A(11!==t.nodeType?t:t.firstChild,"tr")&&S(e).children("tbody")[0]||e}function De(e){return e.type=(null!==e.getAttribute("type"))+"/"+e.type,e}function qe(e){return"true/"===(e.type||"").slice(0,5)?e.type=e.type.slice(5):e.removeAttribute("type"),e}function Le(e,t){var n,r,i,o,a,s;if(1===t.nodeType){if(Y.hasData(e)&&(s=Y.get(e).events))for(i in Y.remove(t,"handle events"),s)for(n=0,r=s[i].length;n").attr(n.scriptAttrs||{}).prop({charset:n.scriptCharset,src:n.url}).on("load error",i=function(e){r.remove(),i=null,e&&t("error"===e.type?404:200,e.type)}),E.head.appendChild(r[0])},abort:function(){i&&i()}}});var _t,zt=[],Ut=/(=)\?(?=&|$)|\?\?/;S.ajaxSetup({jsonp:"callback",jsonpCallback:function(){var e=zt.pop()||S.expando+"_"+wt.guid++;return this[e]=!0,e}}),S.ajaxPrefilter("json jsonp",function(e,t,n){var r,i,o,a=!1!==e.jsonp&&(Ut.test(e.url)?"url":"string"==typeof e.data&&0===(e.contentType||"").indexOf("application/x-www-form-urlencoded")&&Ut.test(e.data)&&"data");if(a||"jsonp"===e.dataTypes[0])return r=e.jsonpCallback=m(e.jsonpCallback)?e.jsonpCallback():e.jsonpCallback,a?e[a]=e[a].replace(Ut,"$1"+r):!1!==e.jsonp&&(e.url+=(Tt.test(e.url)?"&":"?")+e.jsonp+"="+r),e.converters["script json"]=function(){return o||S.error(r+" was not called"),o[0]},e.dataTypes[0]="json",i=C[r],C[r]=function(){o=arguments},n.always(function(){void 0===i?S(C).removeProp(r):C[r]=i,e[r]&&(e.jsonpCallback=t.jsonpCallback,zt.push(r)),o&&m(i)&&i(o[0]),o=i=void 0}),"script"}),y.createHTMLDocument=((_t=E.implementation.createHTMLDocument("").body).innerHTML="
",2===_t.childNodes.length),S.parseHTML=function(e,t,n){return"string"!=typeof e?[]:("boolean"==typeof t&&(n=t,t=!1),t||(y.createHTMLDocument?((r=(t=E.implementation.createHTMLDocument("")).createElement("base")).href=E.location.href,t.head.appendChild(r)):t=E),o=!n&&[],(i=N.exec(e))?[t.createElement(i[1])]:(i=xe([e],t,o),o&&o.length&&S(o).remove(),S.merge([],i.childNodes)));var r,i,o},S.fn.load=function(e,t,n){var r,i,o,a=this,s=e.indexOf(" ");return-1").append(S.parseHTML(e)).find(r):e)}).always(n&&function(e,t){a.each(function(){n.apply(this,o||[e.responseText,t,e])})}),this},S.expr.pseudos.animated=function(t){return S.grep(S.timers,function(e){return t===e.elem}).length},S.offset={setOffset:function(e,t,n){var r,i,o,a,s,u,l=S.css(e,"position"),c=S(e),f={};"static"===l&&(e.style.position="relative"),s=c.offset(),o=S.css(e,"top"),u=S.css(e,"left"),("absolute"===l||"fixed"===l)&&-1<(o+u).indexOf("auto")?(a=(r=c.position()).top,i=r.left):(a=parseFloat(o)||0,i=parseFloat(u)||0),m(t)&&(t=t.call(e,n,S.extend({},s))),null!=t.top&&(f.top=t.top-s.top+a),null!=t.left&&(f.left=t.left-s.left+i),"using"in t?t.using.call(e,f):c.css(f)}},S.fn.extend({offset:function(t){if(arguments.length)return void 0===t?this:this.each(function(e){S.offset.setOffset(this,t,e)});var e,n,r=this[0];return r?r.getClientRects().length?(e=r.getBoundingClientRect(),n=r.ownerDocument.defaultView,{top:e.top+n.pageYOffset,left:e.left+n.pageXOffset}):{top:0,left:0}:void 0},position:function(){if(this[0]){var e,t,n,r=this[0],i={top:0,left:0};if("fixed"===S.css(r,"position"))t=r.getBoundingClientRect();else{t=this.offset(),n=r.ownerDocument,e=r.offsetParent||n.documentElement;while(e&&(e===n.body||e===n.documentElement)&&"static"===S.css(e,"position"))e=e.parentNode;e&&e!==r&&1===e.nodeType&&((i=S(e).offset()).top+=S.css(e,"borderTopWidth",!0),i.left+=S.css(e,"borderLeftWidth",!0))}return{top:t.top-i.top-S.css(r,"marginTop",!0),left:t.left-i.left-S.css(r,"marginLeft",!0)}}},offsetParent:function(){return this.map(function(){var e=this.offsetParent;while(e&&"static"===S.css(e,"position"))e=e.offsetParent;return e||re})}}),S.each({scrollLeft:"pageXOffset",scrollTop:"pageYOffset"},function(t,i){var o="pageYOffset"===i;S.fn[t]=function(e){return $(this,function(e,t,n){var r;if(x(e)?r=e:9===e.nodeType&&(r=e.defaultView),void 0===n)return r?r[i]:e[t];r?r.scrollTo(o?r.pageXOffset:n,o?n:r.pageYOffset):e[t]=n},t,e,arguments.length)}}),S.each(["top","left"],function(e,n){S.cssHooks[n]=Fe(y.pixelPosition,function(e,t){if(t)return t=We(e,n),Pe.test(t)?S(e).position()[n]+"px":t})}),S.each({Height:"height",Width:"width"},function(a,s){S.each({padding:"inner"+a,content:s,"":"outer"+a},function(r,o){S.fn[o]=function(e,t){var n=arguments.length&&(r||"boolean"!=typeof e),i=r||(!0===e||!0===t?"margin":"border");return $(this,function(e,t,n){var r;return x(e)?0===o.indexOf("outer")?e["inner"+a]:e.document.documentElement["client"+a]:9===e.nodeType?(r=e.documentElement,Math.max(e.body["scroll"+a],r["scroll"+a],e.body["offset"+a],r["offset"+a],r["client"+a])):void 0===n?S.css(e,t,i):S.style(e,t,n,i)},s,n?e:void 0,n)}})}),S.each(["ajaxStart","ajaxStop","ajaxComplete","ajaxError","ajaxSuccess","ajaxSend"],function(e,t){S.fn[t]=function(e){return this.on(t,e)}}),S.fn.extend({bind:function(e,t,n){return this.on(e,null,t,n)},unbind:function(e,t){return this.off(e,null,t)},delegate:function(e,t,n,r){return this.on(t,e,n,r)},undelegate:function(e,t,n){return 1===arguments.length?this.off(e,"**"):this.off(t,e||"**",n)},hover:function(e,t){return this.mouseenter(e).mouseleave(t||e)}}),S.each("blur focus focusin focusout resize scroll click dblclick mousedown mouseup mousemove mouseover mouseout mouseenter mouseleave change select submit keydown keypress keyup contextmenu".split(" "),function(e,n){S.fn[n]=function(e,t){return 0+~]|"+M+")"+M+"*"),U=new RegExp(M+"|>"),X=new RegExp(F),V=new RegExp("^"+I+"$"),G={ID:new RegExp("^#("+I+")"),CLASS:new RegExp("^\\.("+I+")"),TAG:new RegExp("^("+I+"|[*])"),ATTR:new RegExp("^"+W),PSEUDO:new RegExp("^"+F),CHILD:new RegExp("^:(only|first|last|nth|nth-last)-(child|of-type)(?:\\("+M+"*(even|odd|(([+-]|)(\\d*)n|)"+M+"*(?:([+-]|)"+M+"*(\\d+)|))"+M+"*\\)|)","i"),bool:new RegExp("^(?:"+R+")$","i"),needsContext:new RegExp("^"+M+"*[>+~]|:(even|odd|eq|gt|lt|nth|first|last)(?:\\("+M+"*((?:-\\d)?\\d*)"+M+"*\\)|)(?=[^-]|$)","i")},Y=/HTML$/i,Q=/^(?:input|select|textarea|button)$/i,J=/^h\d$/i,K=/^[^{]+\{\s*\[native \w/,Z=/^(?:#([\w-]+)|(\w+)|\.([\w-]+))$/,ee=/[+~]/,te=new RegExp("\\\\[\\da-fA-F]{1,6}"+M+"?|\\\\([^\\r\\n\\f])","g"),ne=function(e,t){var n="0x"+e.slice(1)-65536;return t||(n<0?String.fromCharCode(n+65536):String.fromCharCode(n>>10|55296,1023&n|56320))},re=/([\0-\x1f\x7f]|^-?\d)|^-$|[^\0-\x1f\x7f-\uFFFF\w-]/g,ie=function(e,t){return t?"\0"===e?"\ufffd":e.slice(0,-1)+"\\"+e.charCodeAt(e.length-1).toString(16)+" ":"\\"+e},oe=function(){T()},ae=be(function(e){return!0===e.disabled&&"fieldset"===e.nodeName.toLowerCase()},{dir:"parentNode",next:"legend"});try{H.apply(t=O.call(p.childNodes),p.childNodes),t[p.childNodes.length].nodeType}catch(e){H={apply:t.length?function(e,t){L.apply(e,O.call(t))}:function(e,t){var n=e.length,r=0;while(e[n++]=t[r++]);e.length=n-1}}}function se(t,e,n,r){var i,o,a,s,u,l,c,f=e&&e.ownerDocument,p=e?e.nodeType:9;if(n=n||[],"string"!=typeof t||!t||1!==p&&9!==p&&11!==p)return n;if(!r&&(T(e),e=e||C,E)){if(11!==p&&(u=Z.exec(t)))if(i=u[1]){if(9===p){if(!(a=e.getElementById(i)))return n;if(a.id===i)return n.push(a),n}else if(f&&(a=f.getElementById(i))&&y(e,a)&&a.id===i)return n.push(a),n}else{if(u[2])return H.apply(n,e.getElementsByTagName(t)),n;if((i=u[3])&&d.getElementsByClassName&&e.getElementsByClassName)return H.apply(n,e.getElementsByClassName(i)),n}if(d.qsa&&!N[t+" "]&&(!v||!v.test(t))&&(1!==p||"object"!==e.nodeName.toLowerCase())){if(c=t,f=e,1===p&&(U.test(t)||z.test(t))){(f=ee.test(t)&&ye(e.parentNode)||e)===e&&d.scope||((s=e.getAttribute("id"))?s=s.replace(re,ie):e.setAttribute("id",s=S)),o=(l=h(t)).length;while(o--)l[o]=(s?"#"+s:":scope")+" "+xe(l[o]);c=l.join(",")}try{return H.apply(n,f.querySelectorAll(c)),n}catch(e){N(t,!0)}finally{s===S&&e.removeAttribute("id")}}}return g(t.replace($,"$1"),e,n,r)}function ue(){var r=[];return function e(t,n){return r.push(t+" ")>b.cacheLength&&delete e[r.shift()],e[t+" "]=n}}function le(e){return e[S]=!0,e}function ce(e){var t=C.createElement("fieldset");try{return!!e(t)}catch(e){return!1}finally{t.parentNode&&t.parentNode.removeChild(t),t=null}}function fe(e,t){var n=e.split("|"),r=n.length;while(r--)b.attrHandle[n[r]]=t}function pe(e,t){var n=t&&e,r=n&&1===e.nodeType&&1===t.nodeType&&e.sourceIndex-t.sourceIndex;if(r)return r;if(n)while(n=n.nextSibling)if(n===t)return-1;return e?1:-1}function de(t){return function(e){return"input"===e.nodeName.toLowerCase()&&e.type===t}}function he(n){return function(e){var t=e.nodeName.toLowerCase();return("input"===t||"button"===t)&&e.type===n}}function ge(t){return function(e){return"form"in e?e.parentNode&&!1===e.disabled?"label"in e?"label"in e.parentNode?e.parentNode.disabled===t:e.disabled===t:e.isDisabled===t||e.isDisabled!==!t&&ae(e)===t:e.disabled===t:"label"in e&&e.disabled===t}}function ve(a){return le(function(o){return o=+o,le(function(e,t){var n,r=a([],e.length,o),i=r.length;while(i--)e[n=r[i]]&&(e[n]=!(t[n]=e[n]))})})}function ye(e){return e&&"undefined"!=typeof e.getElementsByTagName&&e}for(e in d=se.support={},i=se.isXML=function(e){var t=e.namespaceURI,n=(e.ownerDocument||e).documentElement;return!Y.test(t||n&&n.nodeName||"HTML")},T=se.setDocument=function(e){var t,n,r=e?e.ownerDocument||e:p;return r!=C&&9===r.nodeType&&r.documentElement&&(a=(C=r).documentElement,E=!i(C),p!=C&&(n=C.defaultView)&&n.top!==n&&(n.addEventListener?n.addEventListener("unload",oe,!1):n.attachEvent&&n.attachEvent("onunload",oe)),d.scope=ce(function(e){return a.appendChild(e).appendChild(C.createElement("div")),"undefined"!=typeof e.querySelectorAll&&!e.querySelectorAll(":scope fieldset div").length}),d.attributes=ce(function(e){return e.className="i",!e.getAttribute("className")}),d.getElementsByTagName=ce(function(e){return e.appendChild(C.createComment("")),!e.getElementsByTagName("*").length}),d.getElementsByClassName=K.test(C.getElementsByClassName),d.getById=ce(function(e){return a.appendChild(e).id=S,!C.getElementsByName||!C.getElementsByName(S).length}),d.getById?(b.filter.ID=function(e){var t=e.replace(te,ne);return function(e){return e.getAttribute("id")===t}},b.find.ID=function(e,t){if("undefined"!=typeof t.getElementById&&E){var n=t.getElementById(e);return n?[n]:[]}}):(b.filter.ID=function(e){var n=e.replace(te,ne);return function(e){var t="undefined"!=typeof e.getAttributeNode&&e.getAttributeNode("id");return t&&t.value===n}},b.find.ID=function(e,t){if("undefined"!=typeof t.getElementById&&E){var n,r,i,o=t.getElementById(e);if(o){if((n=o.getAttributeNode("id"))&&n.value===e)return[o];i=t.getElementsByName(e),r=0;while(o=i[r++])if((n=o.getAttributeNode("id"))&&n.value===e)return[o]}return[]}}),b.find.TAG=d.getElementsByTagName?function(e,t){return"undefined"!=typeof t.getElementsByTagName?t.getElementsByTagName(e):d.qsa?t.querySelectorAll(e):void 0}:function(e,t){var n,r=[],i=0,o=t.getElementsByTagName(e);if("*"===e){while(n=o[i++])1===n.nodeType&&r.push(n);return r}return o},b.find.CLASS=d.getElementsByClassName&&function(e,t){if("undefined"!=typeof t.getElementsByClassName&&E)return t.getElementsByClassName(e)},s=[],v=[],(d.qsa=K.test(C.querySelectorAll))&&(ce(function(e){var t;a.appendChild(e).innerHTML="",e.querySelectorAll("[msallowcapture^='']").length&&v.push("[*^$]="+M+"*(?:''|\"\")"),e.querySelectorAll("[selected]").length||v.push("\\["+M+"*(?:value|"+R+")"),e.querySelectorAll("[id~="+S+"-]").length||v.push("~="),(t=C.createElement("input")).setAttribute("name",""),e.appendChild(t),e.querySelectorAll("[name='']").length||v.push("\\["+M+"*name"+M+"*="+M+"*(?:''|\"\")"),e.querySelectorAll(":checked").length||v.push(":checked"),e.querySelectorAll("a#"+S+"+*").length||v.push(".#.+[+~]"),e.querySelectorAll("\\\f"),v.push("[\\r\\n\\f]")}),ce(function(e){e.innerHTML="";var t=C.createElement("input");t.setAttribute("type","hidden"),e.appendChild(t).setAttribute("name","D"),e.querySelectorAll("[name=d]").length&&v.push("name"+M+"*[*^$|!~]?="),2!==e.querySelectorAll(":enabled").length&&v.push(":enabled",":disabled"),a.appendChild(e).disabled=!0,2!==e.querySelectorAll(":disabled").length&&v.push(":enabled",":disabled"),e.querySelectorAll("*,:x"),v.push(",.*:")})),(d.matchesSelector=K.test(c=a.matches||a.webkitMatchesSelector||a.mozMatchesSelector||a.oMatchesSelector||a.msMatchesSelector))&&ce(function(e){d.disconnectedMatch=c.call(e,"*"),c.call(e,"[s!='']:x"),s.push("!=",F)}),v=v.length&&new RegExp(v.join("|")),s=s.length&&new RegExp(s.join("|")),t=K.test(a.compareDocumentPosition),y=t||K.test(a.contains)?function(e,t){var n=9===e.nodeType?e.documentElement:e,r=t&&t.parentNode;return e===r||!(!r||1!==r.nodeType||!(n.contains?n.contains(r):e.compareDocumentPosition&&16&e.compareDocumentPosition(r)))}:function(e,t){if(t)while(t=t.parentNode)if(t===e)return!0;return!1},D=t?function(e,t){if(e===t)return l=!0,0;var n=!e.compareDocumentPosition-!t.compareDocumentPosition;return n||(1&(n=(e.ownerDocument||e)==(t.ownerDocument||t)?e.compareDocumentPosition(t):1)||!d.sortDetached&&t.compareDocumentPosition(e)===n?e==C||e.ownerDocument==p&&y(p,e)?-1:t==C||t.ownerDocument==p&&y(p,t)?1:u?P(u,e)-P(u,t):0:4&n?-1:1)}:function(e,t){if(e===t)return l=!0,0;var n,r=0,i=e.parentNode,o=t.parentNode,a=[e],s=[t];if(!i||!o)return e==C?-1:t==C?1:i?-1:o?1:u?P(u,e)-P(u,t):0;if(i===o)return pe(e,t);n=e;while(n=n.parentNode)a.unshift(n);n=t;while(n=n.parentNode)s.unshift(n);while(a[r]===s[r])r++;return r?pe(a[r],s[r]):a[r]==p?-1:s[r]==p?1:0}),C},se.matches=function(e,t){return se(e,null,null,t)},se.matchesSelector=function(e,t){if(T(e),d.matchesSelector&&E&&!N[t+" "]&&(!s||!s.test(t))&&(!v||!v.test(t)))try{var n=c.call(e,t);if(n||d.disconnectedMatch||e.document&&11!==e.document.nodeType)return n}catch(e){N(t,!0)}return 0":{dir:"parentNode",first:!0}," ":{dir:"parentNode"},"+":{dir:"previousSibling",first:!0},"~":{dir:"previousSibling"}},preFilter:{ATTR:function(e){return e[1]=e[1].replace(te,ne),e[3]=(e[3]||e[4]||e[5]||"").replace(te,ne),"~="===e[2]&&(e[3]=" "+e[3]+" "),e.slice(0,4)},CHILD:function(e){return e[1]=e[1].toLowerCase(),"nth"===e[1].slice(0,3)?(e[3]||se.error(e[0]),e[4]=+(e[4]?e[5]+(e[6]||1):2*("even"===e[3]||"odd"===e[3])),e[5]=+(e[7]+e[8]||"odd"===e[3])):e[3]&&se.error(e[0]),e},PSEUDO:function(e){var t,n=!e[6]&&e[2];return G.CHILD.test(e[0])?null:(e[3]?e[2]=e[4]||e[5]||"":n&&X.test(n)&&(t=h(n,!0))&&(t=n.indexOf(")",n.length-t)-n.length)&&(e[0]=e[0].slice(0,t),e[2]=n.slice(0,t)),e.slice(0,3))}},filter:{TAG:function(e){var t=e.replace(te,ne).toLowerCase();return"*"===e?function(){return!0}:function(e){return e.nodeName&&e.nodeName.toLowerCase()===t}},CLASS:function(e){var t=m[e+" "];return t||(t=new RegExp("(^|"+M+")"+e+"("+M+"|$)"))&&m(e,function(e){return t.test("string"==typeof e.className&&e.className||"undefined"!=typeof e.getAttribute&&e.getAttribute("class")||"")})},ATTR:function(n,r,i){return function(e){var t=se.attr(e,n);return null==t?"!="===r:!r||(t+="","="===r?t===i:"!="===r?t!==i:"^="===r?i&&0===t.indexOf(i):"*="===r?i&&-1:\x20\t\r\n\f]*)[\x20\t\r\n\f]*\/?>(?:<\/\1>|)$/i;function D(e,n,r){return m(n)?S.grep(e,function(e,t){return!!n.call(e,t,e)!==r}):n.nodeType?S.grep(e,function(e){return e===n!==r}):"string"!=typeof n?S.grep(e,function(e){return-1)[^>]*|#([\w-]+))$/;(S.fn.init=function(e,t,n){var r,i;if(!e)return this;if(n=n||j,"string"==typeof e){if(!(r="<"===e[0]&&">"===e[e.length-1]&&3<=e.length?[null,e,null]:q.exec(e))||!r[1]&&t)return!t||t.jquery?(t||n).find(e):this.constructor(t).find(e);if(r[1]){if(t=t instanceof S?t[0]:t,S.merge(this,S.parseHTML(r[1],t&&t.nodeType?t.ownerDocument||t:E,!0)),N.test(r[1])&&S.isPlainObject(t))for(r in t)m(this[r])?this[r](t[r]):this.attr(r,t[r]);return this}return(i=E.getElementById(r[2]))&&(this[0]=i,this.length=1),this}return e.nodeType?(this[0]=e,this.length=1,this):m(e)?void 0!==n.ready?n.ready(e):e(S):S.makeArray(e,this)}).prototype=S.fn,j=S(E);var L=/^(?:parents|prev(?:Until|All))/,H={children:!0,contents:!0,next:!0,prev:!0};function O(e,t){while((e=e[t])&&1!==e.nodeType);return e}S.fn.extend({has:function(e){var t=S(e,this),n=t.length;return this.filter(function(){for(var e=0;e\x20\t\r\n\f]*)/i,he=/^$|^module$|\/(?:java|ecma)script/i;ce=E.createDocumentFragment().appendChild(E.createElement("div")),(fe=E.createElement("input")).setAttribute("type","radio"),fe.setAttribute("checked","checked"),fe.setAttribute("name","t"),ce.appendChild(fe),y.checkClone=ce.cloneNode(!0).cloneNode(!0).lastChild.checked,ce.innerHTML="",y.noCloneChecked=!!ce.cloneNode(!0).lastChild.defaultValue,ce.innerHTML="",y.option=!!ce.lastChild;var ge={thead:[1,"","
"],col:[2,"","
"],tr:[2,"","
"],td:[3,"","
"],_default:[0,"",""]};function ve(e,t){var n;return n="undefined"!=typeof e.getElementsByTagName?e.getElementsByTagName(t||"*"):"undefined"!=typeof e.querySelectorAll?e.querySelectorAll(t||"*"):[],void 0===t||t&&A(e,t)?S.merge([e],n):n}function ye(e,t){for(var n=0,r=e.length;n",""]);var me=/<|&#?\w+;/;function xe(e,t,n,r,i){for(var o,a,s,u,l,c,f=t.createDocumentFragment(),p=[],d=0,h=e.length;d\s*$/g;function qe(e,t){return A(e,"table")&&A(11!==t.nodeType?t:t.firstChild,"tr")&&S(e).children("tbody")[0]||e}function Le(e){return e.type=(null!==e.getAttribute("type"))+"/"+e.type,e}function He(e){return"true/"===(e.type||"").slice(0,5)?e.type=e.type.slice(5):e.removeAttribute("type"),e}function Oe(e,t){var n,r,i,o,a,s;if(1===t.nodeType){if(Y.hasData(e)&&(s=Y.get(e).events))for(i in Y.remove(t,"handle events"),s)for(n=0,r=s[i].length;n").attr(n.scriptAttrs||{}).prop({charset:n.scriptCharset,src:n.url}).on("load error",i=function(e){r.remove(),i=null,e&&t("error"===e.type?404:200,e.type)}),E.head.appendChild(r[0])},abort:function(){i&&i()}}});var Ut,Xt=[],Vt=/(=)\?(?=&|$)|\?\?/;S.ajaxSetup({jsonp:"callback",jsonpCallback:function(){var e=Xt.pop()||S.expando+"_"+Ct.guid++;return this[e]=!0,e}}),S.ajaxPrefilter("json jsonp",function(e,t,n){var r,i,o,a=!1!==e.jsonp&&(Vt.test(e.url)?"url":"string"==typeof e.data&&0===(e.contentType||"").indexOf("application/x-www-form-urlencoded")&&Vt.test(e.data)&&"data");if(a||"jsonp"===e.dataTypes[0])return r=e.jsonpCallback=m(e.jsonpCallback)?e.jsonpCallback():e.jsonpCallback,a?e[a]=e[a].replace(Vt,"$1"+r):!1!==e.jsonp&&(e.url+=(Et.test(e.url)?"&":"?")+e.jsonp+"="+r),e.converters["script json"]=function(){return o||S.error(r+" was not called"),o[0]},e.dataTypes[0]="json",i=C[r],C[r]=function(){o=arguments},n.always(function(){void 0===i?S(C).removeProp(r):C[r]=i,e[r]&&(e.jsonpCallback=t.jsonpCallback,Xt.push(r)),o&&m(i)&&i(o[0]),o=i=void 0}),"script"}),y.createHTMLDocument=((Ut=E.implementation.createHTMLDocument("").body).innerHTML="
",2===Ut.childNodes.length),S.parseHTML=function(e,t,n){return"string"!=typeof e?[]:("boolean"==typeof t&&(n=t,t=!1),t||(y.createHTMLDocument?((r=(t=E.implementation.createHTMLDocument("")).createElement("base")).href=E.location.href,t.head.appendChild(r)):t=E),o=!n&&[],(i=N.exec(e))?[t.createElement(i[1])]:(i=xe([e],t,o),o&&o.length&&S(o).remove(),S.merge([],i.childNodes)));var r,i,o},S.fn.load=function(e,t,n){var r,i,o,a=this,s=e.indexOf(" ");return-1").append(S.parseHTML(e)).find(r):e)}).always(n&&function(e,t){a.each(function(){n.apply(this,o||[e.responseText,t,e])})}),this},S.expr.pseudos.animated=function(t){return S.grep(S.timers,function(e){return t===e.elem}).length},S.offset={setOffset:function(e,t,n){var r,i,o,a,s,u,l=S.css(e,"position"),c=S(e),f={};"static"===l&&(e.style.position="relative"),s=c.offset(),o=S.css(e,"top"),u=S.css(e,"left"),("absolute"===l||"fixed"===l)&&-1<(o+u).indexOf("auto")?(a=(r=c.position()).top,i=r.left):(a=parseFloat(o)||0,i=parseFloat(u)||0),m(t)&&(t=t.call(e,n,S.extend({},s))),null!=t.top&&(f.top=t.top-s.top+a),null!=t.left&&(f.left=t.left-s.left+i),"using"in t?t.using.call(e,f):("number"==typeof f.top&&(f.top+="px"),"number"==typeof f.left&&(f.left+="px"),c.css(f))}},S.fn.extend({offset:function(t){if(arguments.length)return void 0===t?this:this.each(function(e){S.offset.setOffset(this,t,e)});var e,n,r=this[0];return r?r.getClientRects().length?(e=r.getBoundingClientRect(),n=r.ownerDocument.defaultView,{top:e.top+n.pageYOffset,left:e.left+n.pageXOffset}):{top:0,left:0}:void 0},position:function(){if(this[0]){var e,t,n,r=this[0],i={top:0,left:0};if("fixed"===S.css(r,"position"))t=r.getBoundingClientRect();else{t=this.offset(),n=r.ownerDocument,e=r.offsetParent||n.documentElement;while(e&&(e===n.body||e===n.documentElement)&&"static"===S.css(e,"position"))e=e.parentNode;e&&e!==r&&1===e.nodeType&&((i=S(e).offset()).top+=S.css(e,"borderTopWidth",!0),i.left+=S.css(e,"borderLeftWidth",!0))}return{top:t.top-i.top-S.css(r,"marginTop",!0),left:t.left-i.left-S.css(r,"marginLeft",!0)}}},offsetParent:function(){return this.map(function(){var e=this.offsetParent;while(e&&"static"===S.css(e,"position"))e=e.offsetParent;return e||re})}}),S.each({scrollLeft:"pageXOffset",scrollTop:"pageYOffset"},function(t,i){var o="pageYOffset"===i;S.fn[t]=function(e){return $(this,function(e,t,n){var r;if(x(e)?r=e:9===e.nodeType&&(r=e.defaultView),void 0===n)return r?r[i]:e[t];r?r.scrollTo(o?r.pageXOffset:n,o?n:r.pageYOffset):e[t]=n},t,e,arguments.length)}}),S.each(["top","left"],function(e,n){S.cssHooks[n]=$e(y.pixelPosition,function(e,t){if(t)return t=Be(e,n),Me.test(t)?S(e).position()[n]+"px":t})}),S.each({Height:"height",Width:"width"},function(a,s){S.each({padding:"inner"+a,content:s,"":"outer"+a},function(r,o){S.fn[o]=function(e,t){var n=arguments.length&&(r||"boolean"!=typeof e),i=r||(!0===e||!0===t?"margin":"border");return $(this,function(e,t,n){var r;return x(e)?0===o.indexOf("outer")?e["inner"+a]:e.document.documentElement["client"+a]:9===e.nodeType?(r=e.documentElement,Math.max(e.body["scroll"+a],r["scroll"+a],e.body["offset"+a],r["offset"+a],r["client"+a])):void 0===n?S.css(e,t,i):S.style(e,t,n,i)},s,n?e:void 0,n)}})}),S.each(["ajaxStart","ajaxStop","ajaxComplete","ajaxError","ajaxSuccess","ajaxSend"],function(e,t){S.fn[t]=function(e){return this.on(t,e)}}),S.fn.extend({bind:function(e,t,n){return this.on(e,null,t,n)},unbind:function(e,t){return this.off(e,null,t)},delegate:function(e,t,n,r){return this.on(t,e,n,r)},undelegate:function(e,t,n){return 1===arguments.length?this.off(e,"**"):this.off(t,e||"**",n)},hover:function(e,t){return this.mouseenter(e).mouseleave(t||e)}}),S.each("blur focus focusin focusout resize scroll click dblclick mousedown mouseup mousemove mouseover mouseout mouseenter mouseleave change select submit keydown keypress keyup contextmenu".split(" "),function(e,n){S.fn[n]=function(e,t){return 0 { - const [docname, title, anchor, descr, score, filename] = result - return score + score: function(result) { + return result[4]; }, */ @@ -30,11 +28,9 @@ if (typeof Scorer === "undefined") { // or matches in the last dotted part of the object name objPartialMatch: 6, // Additive scores depending on the priority of the object - objPrio: { - 0: 15, // used to be importantResults - 1: 5, // used to be objectResults - 2: -5, // used to be unimportantResults - }, + objPrio: {0: 15, // used to be importantResults + 1: 5, // used to be objectResults + 2: -5}, // used to be unimportantResults // Used when the priority is not in the mapping. objPrioDefault: 0, @@ -43,455 +39,456 @@ if (typeof Scorer === "undefined") { partialTitle: 7, // query found in terms term: 5, - partialTerm: 2, + partialTerm: 2 }; } -const _removeChildren = (element) => { - while (element && element.lastChild) element.removeChild(element.lastChild); -}; - -/** - * See https://developer.mozilla.org/en-US/docs/Web/JavaScript/Guide/Regular_Expressions#escaping - */ -const _escapeRegExp = (string) => - string.replace(/[.*+\-?^${}()|[\]\\]/g, "\\$&"); // $& means the whole matched string - -const _displayItem = (item, highlightTerms, searchTerms) => { - const docBuilder = DOCUMENTATION_OPTIONS.BUILDER; - const docUrlRoot = DOCUMENTATION_OPTIONS.URL_ROOT; - const docFileSuffix = DOCUMENTATION_OPTIONS.FILE_SUFFIX; - const docLinkSuffix = DOCUMENTATION_OPTIONS.LINK_SUFFIX; - const showSearchSummary = DOCUMENTATION_OPTIONS.SHOW_SEARCH_SUMMARY; - - const [docName, title, anchor, descr] = item; - - let listItem = document.createElement("li"); - let requestUrl; - let linkUrl; - if (docBuilder === "dirhtml") { - // dirhtml builder - let dirname = docName + "/"; - if (dirname.match(/\/index\/$/)) - dirname = dirname.substring(0, dirname.length - 6); - else if (dirname === "index/") dirname = ""; - requestUrl = docUrlRoot + dirname; - linkUrl = requestUrl; - } else { - // normal html builders - requestUrl = docUrlRoot + docName + docFileSuffix; - linkUrl = docName + docLinkSuffix; - } - const params = new URLSearchParams(); - params.set("highlight", [...highlightTerms].join(" ")); - let linkEl = listItem.appendChild(document.createElement("a")); - linkEl.href = linkUrl + "?" + params.toString() + anchor; - linkEl.innerHTML = title; - if (descr) - listItem.appendChild(document.createElement("span")).innerText = - " (" + descr + ")"; - else if (showSearchSummary) - fetch(requestUrl) - .then((responseData) => responseData.text()) - .then((data) => { - if (data) - listItem.appendChild( - Search.makeSearchSummary(data, searchTerms, highlightTerms) - ); - }); - Search.output.appendChild(listItem); -}; -const _finishSearch = (resultCount) => { - Search.stopPulse(); - Search.title.innerText = _("Search Results"); - if (!resultCount) - Search.status.innerText = Documentation.gettext( - "Your search did not match any documents. Please make sure that all words are spelled correctly and that you've selected enough categories." - ); - else - Search.status.innerText = _( - `Search finished, found ${resultCount} page(s) matching the search query.` - ); -}; -const _displayNextItem = ( - results, - resultCount, - highlightTerms, - searchTerms -) => { - // results left, load the summary and display it - // this is intended to be dynamic (don't sub resultsCount) - if (results.length) { - _displayItem(results.pop(), highlightTerms, searchTerms); - setTimeout( - () => _displayNextItem(results, resultCount, highlightTerms, searchTerms), - 5 - ); +if (!splitQuery) { + function splitQuery(query) { + return query.split(/\s+/); } - // search finished, update title and status message - else _finishSearch(resultCount); -}; - -/** - * Default splitQuery function. Can be overridden in ``sphinx.search`` with a - * custom function per language. - * - * The regular expression works by splitting the string on consecutive characters - * that are not Unicode letters, numbers, underscores, or emoji characters. - * This is the same as ``\W+`` in Python, preserving the surrogate pair area. - */ -if (typeof splitQuery === "undefined") { - var splitQuery = (query) => query - .split(/[^\p{Letter}\p{Number}_\p{Emoji_Presentation}]+/gu) - .filter(term => term) // remove remaining empty strings } /** * Search Module */ -const Search = { - _index: null, - _queued_query: null, - _pulse_status: -1, - - htmlToText: (htmlString) => { - const htmlElement = document - .createRange() - .createContextualFragment(htmlString); - _removeChildren(htmlElement.querySelectorAll(".headerlink")); - const docContent = htmlElement.querySelector('[role="main"]'); - if (docContent !== undefined) return docContent.textContent; - console.warn( - "Content block not found. Sphinx search tries to obtain it via '[role=main]'. Could you check your theme or template." - ); - return ""; +var Search = { + + _index : null, + _queued_query : null, + _pulse_status : -1, + + htmlToText : function(htmlString) { + var virtualDocument = document.implementation.createHTMLDocument('virtual'); + var htmlElement = $(htmlString, virtualDocument); + htmlElement.find('.headerlink').remove(); + docContent = htmlElement.find('[role=main]')[0]; + if(docContent === undefined) { + console.warn("Content block not found. Sphinx search tries to obtain it " + + "via '[role=main]'. Could you check your theme or template."); + return ""; + } + return docContent.textContent || docContent.innerText; }, - init: () => { - const query = new URLSearchParams(window.location.search).get("q"); - document - .querySelectorAll('input[name="q"]') - .forEach((el) => (el.value = query)); - if (query) Search.performSearch(query); + init : function() { + var params = $.getQueryParameters(); + if (params.q) { + var query = params.q[0]; + $('input[name="q"]')[0].value = query; + this.performSearch(query); + } }, - loadIndex: (url) => - (document.body.appendChild(document.createElement("script")).src = url), + loadIndex : function(url) { + $.ajax({type: "GET", url: url, data: null, + dataType: "script", cache: true, + complete: function(jqxhr, textstatus) { + if (textstatus != "success") { + document.getElementById("searchindexloader").src = url; + } + }}); + }, - setIndex: (index) => { - Search._index = index; - if (Search._queued_query !== null) { - const query = Search._queued_query; - Search._queued_query = null; - Search.query(query); + setIndex : function(index) { + var q; + this._index = index; + if ((q = this._queued_query) !== null) { + this._queued_query = null; + Search.query(q); } }, - hasIndex: () => Search._index !== null, - - deferQuery: (query) => (Search._queued_query = query), + hasIndex : function() { + return this._index !== null; + }, - stopPulse: () => (Search._pulse_status = -1), + deferQuery : function(query) { + this._queued_query = query; + }, - startPulse: () => { - if (Search._pulse_status >= 0) return; + stopPulse : function() { + this._pulse_status = 0; + }, - const pulse = () => { + startPulse : function() { + if (this._pulse_status >= 0) + return; + function pulse() { + var i; Search._pulse_status = (Search._pulse_status + 1) % 4; - Search.dots.innerText = ".".repeat(Search._pulse_status); - if (Search._pulse_status >= 0) window.setTimeout(pulse, 500); - }; + var dotString = ''; + for (i = 0; i < Search._pulse_status; i++) + dotString += '.'; + Search.dots.text(dotString); + if (Search._pulse_status > -1) + window.setTimeout(pulse, 500); + } pulse(); }, /** * perform a search for something (or wait until index is loaded) */ - performSearch: (query) => { + performSearch : function(query) { // create the required interface elements - const searchText = document.createElement("h2"); - searchText.textContent = _("Searching"); - const searchSummary = document.createElement("p"); - searchSummary.classList.add("search-summary"); - searchSummary.innerText = ""; - const searchList = document.createElement("ul"); - searchList.classList.add("search"); - - const out = document.getElementById("search-results"); - Search.title = out.appendChild(searchText); - Search.dots = Search.title.appendChild(document.createElement("span")); - Search.status = out.appendChild(searchSummary); - Search.output = out.appendChild(searchList); - - const searchProgress = document.getElementById("search-progress"); - // Some themes don't use the search progress node - if (searchProgress) { - searchProgress.innerText = _("Preparing search..."); - } - Search.startPulse(); + this.out = $('#search-results'); + this.title = $('

' + _('Searching') + '

').appendTo(this.out); + this.dots = $('').appendTo(this.title); + this.status = $('

 

').appendTo(this.out); + this.output = $('