Fix typos

doc/applications/index.md

@@ -18,7 +18,7 @@ In particular, these include
 The [MMT API](../api) based on MMT provides a number of knowledge management services including
 
 * notation-based presentation,
-* interactive web-browisng,
+* interactive web-browsing,
 * MMT-aware databases with custom indexing and retrieval,
 * project-based abstraction and work flows for building, distribution, and sharing,
 * management of change,

doc/applications/intellij/index.md

@@ -3,7 +3,7 @@ layout: doc
 title: IntelliJ-MMT Plugin
 ---
 
-[IntelliJ IDEA](https://www.jetbrains.com/idea/) is a multi-purpose Java-based IDE. An **MMT plugin** adds functionality to deal with MMT sourecs. It serves the usual features of "language plugins":
+[IntelliJ IDEA](https://www.jetbrains.com/idea/) is a multi-purpose Java-based IDE. An **MMT plugin** adds functionality to deal with MMT sources. It serves the usual features of "language plugins":
 
 - syntax highlighting
 - type checking

doc/applications/intellij/installation.md

@@ -48,5 +48,5 @@ Since MMT files make heavy use of Unicode math charcters, be sure to have a font
 
 ### Notes on automatic type checking
 
-- By default, the Plugin does **not** type check the terms of an open *mmt*-file, since doing so is computationally expensive and inconvenvient for the user. Type checking can be easily activated and deactivated in the *Errors* panel of the MMT tool window (View -> Tool Windows -> MMT)
+- By default, the Plugin does **not** type check the terms of an open *mmt*-file, since doing so is computationally expensive and inconvenient for the user. Type checking can be easily activated and deactivated in the *Errors* panel of the MMT tool window (View -> Tool Windows -> MMT)
 - The *Document Tree* (on the left border of the IntelliJ-Window) only shows the syntax tree of the document that has been type checked last. To see the tree for the currently opened document, check the *Type Checking* checkbox in the *Errors* panel. Automatically navigating the syntax tree by caret position in the document can be turned on and off with the corresponding check box at the top of the *Document Tree* panel.

doc/applications/jedit.md

@@ -52,7 +52,7 @@ This turns the system into a (very simple) interactive theorem prover.
 
 The type checker treats any occurrence of _ in MMT terms as a fresh unknown and tries to infer its value.
 This includes calling the (experimental and very weak) automated theorem prover of MMT.
-If successful, the term is inserted into the internal syntax (as shown by Sidekick) but the _ remains in the soruce.
+If successful, the term is inserted into the internal syntax (as shown by Sidekick) but the _ remains in the source.
 If the prove fails but the expected type of the subterm is found, a hole-term is introduced.
 In the latter case, the command introduce-hole can be used to replace _ with the hole-term in the source (e.g., in order to use auto-completion).
 

doc/applications/server.md

@@ -52,7 +52,7 @@ Some features are:
       * a *symbol* shows its full MMT URI as a tooltip.
       * a *variable* selects its declaration.
     * The *right-click menu* permits setting visibility options for the selected subexpression.
-        These show/hide parts of the expression that were infered by the system:
+        These show/hide parts of the expression that were inferred by the system:
       * *reconstructed types*: the omitted types of bound variables
       * *implicit arguments*: the omitted arguments to operator applications
       * *redundant brackets*: brackets that are not needed due to operator precedences

doc/applications/shell.md

@@ -12,7 +12,7 @@ Each subclass comes with scaladoc and can be best understood by browsing the kno
 The up-to-date context-free grammar for shell commands is part of the constructor parser in the companion object `Action` and can be best understood by reading the source code.
 
 ### ANSI Formatting in the MMT Shell
-Some shell output uses [ANSI escapes](https://en.wikipedia.org/wiki/ANSI_escape_code) for highlighting. To display the formating, you can use [ansicon](https://github.com/adoxa/ansicon) for the windows console or [ansi console](https://web.archive.org/web/20200816075948/http://mihai-nita.net/2013/06/03/eclipse-plugin-ansi-in-console/) for the eclipse console. (Both are optional and very easy to install and use.) Unix shells should understand it natively.
+Some shell output uses [ANSI escapes](https://en.wikipedia.org/wiki/ANSI_escape_code) for highlighting. To display the formatting, you can use [ansicon](https://github.com/adoxa/ansicon) for the windows console or [ansi console](https://web.archive.org/web/20200816075948/http://mihai-nita.net/2013/06/03/eclipse-plugin-ansi-in-console/) for the eclipse console. (Both are optional and very easy to install and use.) Unix shells should understand it natively.
 
 ### MMT Scripts
 An MMT script is a text file containing one shell command per line. (Empty lines are allowed, lines starting with // are ignored.)

doc/applications/tgview.md

@@ -2,7 +2,7 @@
 layout: doc
 title: TGView (the MMT Theory Graph viewer)
 ---
-TGView is a brower-based theory graph viewer based on the [VisJS](http://visjs.org/)
+TGView is a browser-based theory graph viewer based on the [VisJS](http://visjs.org/)
 network library. The code is [available on GitHub](https://github.com/UniFormal/TGView),
 and a [MathHub instance](http://mmt.mathhub.info/graphs/tgview) gives visual access to the
 MathHub archives as interactive theory graphs.

doc/archives/Mathhub/lmh.md

@@ -35,7 +35,7 @@ LMH also allows installing a specific branch of an archive. The syntax for this
 
     lmh install <name of archive>@<version>
 
-Archvies are versioned using git. 
+Archives are versioned using git. 
 A version of an archive can be a branch name or a git commit hash (Technically anything that is a ref in git).
 When a non-existing version of the archive is specified, lmh will display a warning message and then fall back to the default version. 
 If `lmh install` with a specific version is called on an archive that is already installed, it will make sure to update to the specified version. 

doc/archives/building.md

@@ -10,7 +10,7 @@ MMT can be used as a build tool using a special [shell command](../applications/
 ### Defining Build Targets
 
 The collection of build targets is maintained by the [extension manager](../api/extensions/). New build targets are defined by implementing the [`archives.BuildTarget`](apidoc://info.kwarc.mmt.api.archives.BuildTarget) class.
-Build target modfiers and change management are supported for automatically for every build target.
+Build target modifiers and change management are supported for automatically for every build target.
 
 ### Build Target Modifiers
 

doc/archives/meta_inf.md

@@ -20,5 +20,5 @@ narration-base	| the URI prefix prepended to the file paths inside the archives
 source, content, narration, relational |	custom folder names for specific dimensions (see the [build tool](building) for details)
 ns	| the default namespace of the archive used for all files that do not declare a namespace
 ns-PREFIX	| a namespace binding for PREFIX that is in effect for all files in the archives (unless a file redefines the prefix)
-dependencies | comma-seperated dependencies for the archive in question. <span class="detail">Every archive implicitly has an additional dependency on the 'meta-inf' archive of its group even if it is not listed. For example on MathHub (to which the concepts also apply to), the archive [MitM/Foundation](https://gl.mathhub.info/MitM/Foundation) has the implicit dependency [MitM/meta-inf](https://gl.mathhub.info/MitM/meta-inf).</span>
+dependencies | comma-separated dependencies for the archive in question. <span class="detail">Every archive implicitly has an additional dependency on the 'meta-inf' archive of its group even if it is not listed. For example on MathHub (to which the concepts also apply to), the archive [MitM/Foundation](https://gl.mathhub.info/MitM/Foundation) has the implicit dependency [MitM/meta-inf](https://gl.mathhub.info/MitM/meta-inf).</span>
 foundation | the (assumed to be common) **meta theory** for all modules in the archive.

doc/development/contributing.md

@@ -73,7 +73,7 @@ There are two essential workflows:
 
 #### Updating the release branch
 
-Before a release is made the version string stored in [src/mmt-api/resources/versioning/system.txt](https://github.com/UniFormal/MMT/blob/master/src/mmt-api/resources/versioning/system.txt) should be increased appropriatly. 
+Before a release is made the version string stored in [src/mmt-api/resources/versioning/system.txt](https://github.com/UniFormal/MMT/blob/master/src/mmt-api/resources/versioning/system.txt) should be increased appropriately. 
 
 Once such a change has landed on master, when then again use pull requests to mark a version of MMT as a release. 
 This time we merge from ```master``` onto ```release```. 

doc/development/releases.md

@@ -461,7 +461,7 @@ Released on [22nd February 2017](https://github.com/UniFormal/MMT/releases/tag/v
   * Initial version of Active Computation Extension
 * Improvements:
   * Update to Travis Build Scripts
-  * Webserver Improvements, including CORS support, hostname support, and client side libarary updates]
+  * Webserver Improvements, including CORS support, hostname support, and client side library updates]
 
 #### Release 4
 

doc/development/scala.md

@@ -18,7 +18,7 @@ Configure your IDEs accordingly and do not change styling recklessly.
 All indentation must be by spaces (no tabs).
 
 The depth of indentation is not fixed. It is typically 2-4 spaces.
-It does not have to be consistent throughtout a file.
+It does not have to be consistent throughout a file.
 
 #### Imports
 

doc/language/declarations.md

@@ -120,7 +120,7 @@ The syntax for structures is
 * Even though structures are declarations, they have a [module](modules) body and are thus delimited by the module [delimiter](delimiters) ![`\GS`](../img/GS.png) instead of the declaration delimiter ![`\RS`](../img/RS.png).
 * Simple includes are still delimited with ![`\RS`](../img/RS.png).
 * The name of each declaration in a structure has to correspond to the name of a declaration in the `<domain>`. 
-* Components (aliases, types, definitions etc.) explicitely given in a structure *override* the corresponding component of the declaration in the `<domain>`, all other components are inherited from the latter. In particular, structures can introduce definitions for (not necessarily) previously undefined constants, in which case the (new) definition has to have the (induced/old) type of the constant. It is recommended to *never override the type* of a symbol in a structure. If no component of a declaration is to be modified, it can be left implicit. In this case a fresh copy of the declaration is inherited. If such multiplication is not desired for some declarations, they can be assigned to a previously inherited version of the declaration.
+* Components (aliases, types, definitions etc.) explicitly given in a structure *override* the corresponding component of the declaration in the `<domain>`, all other components are inherited from the latter. In particular, structures can introduce definitions for (not necessarily) previously undefined constants, in which case the (new) definition has to have the (induced/old) type of the constant. It is recommended to *never override the type* of a symbol in a structure. If no component of a declaration is to be modified, it can be left implicit. In this case a fresh copy of the declaration is inherited. If such multiplication is not desired for some declarations, they can be assigned to a previously inherited version of the declaration.
 * The full [URI](uris) of an induced declaration `<declname>` in a structure `<struct>` in a module `<mod>` is `<mod> ? <struct> / <declname>`. It is this declaration, that is visible from the outside and can be used in subsequent (to the structure) declarations. In contrast, the URI `<mod> / <struct> ? <declname>` refers to the plain declaration as declared *directly in the structure*, i.e. without inheritance. The latter should never be used outside of the [API](../api) and is invisible to declarations outside of the structure.
 * Unlike simple includes, multiple *named structures* with the same `<domain>` are **not** redundant. Each structure introduces fresh (possibly modified) copies of the declarations in the domain. 
 * The limit of the previous point is the [*meta theory*](modules.html#theories) of the domain. If two structures `s1`,`s2` have corresponding domains `dom1`,`dom2` with the same meta theory `meta`, then *everything in the dependency closure of `meta`* will be included exactly once.

doc/language/implicit.md

@@ -23,7 +23,7 @@ If there is an implicit morphism m from S to T, all names c of S can be used in
 Similarly, every morphism out of T can be treated as a morphism out of S by composing with m.
 This happens automatically, i.e., the user does not have to refer to m, hence the name *implicit* morphisms.
 
-Of course, this only works if m is uniuqe, i.e., there may at most 1 implicit morphism between any two theories.
+Of course, this only works if m is unique, i.e., there may at most 1 implicit morphism between any two theories.
 In other words, the subgraph of implicit morphisms must commute.
 
 A number of examples are given in the research paper on implicit morphisms.
@@ -177,7 +177,7 @@ MMT flattens every include i of S in T and by composing it with every include in
 The order is relevant because the declarations included by i can already be used in the declarations between i and a later include with the same domain.
 
 There is one relaxation though.
-If the later include i2 of R is primitve, it can often be dropped even if an earlier include i1 of R has a different kind or a definition.
+If the later include i2 of R is primitive, it can often be dropped even if an earlier include i1 of R has a different kind or a definition.
 This is justified because:
 * If i2 is a realization, the promise of i2 is trivial because it has already been fulfilled by i1.
 * If i2 is a plain include and i1 already provides a definition m, dropping i2 amounts to implicitly instantiating all R-constants in the domain of i2 via m.

doc/language/index.md

@@ -5,7 +5,7 @@ title: The MMT Language
 
 This sections gives an overview of the **general language structure** of MMT.
 To be more concrete, it also explains one specific **concrete syntax**, which is the main syntax used to write MMT content natively.
-A description of MMT's **abstract syntax** and the corrseponding internal data structures can be found [here](../api/syntax)
+A description of MMT's **abstract syntax** and the corresponding internal data structures can be found [here](../api/syntax)
 
 MMT is a language for formal mathematics that pays special attention to [*foundation-independence*](../philosophy/independence), scalability, and modularity.
 MMT follows the [OMDoc](http://www.omdoc.org/) philosophy and will be integrated into the upcoming OMDoc 2 format.

doc/language/inductive.md

@@ -5,15 +5,15 @@ title: Inductive Types
 
 ### Declaraing an inductive type
 
-The structural feature **inductive** for inductive types can be used to elaborate to define (mutally) inductive types. A derived declaration for this features consists of:
+The structural feature **inductive** for inductive types can be used to elaborate to define (mutually) inductive types. A derived declaration for this features consists of:
 
 * A name of the derived declaration
 * A list of parameters of the derived declaration (similar to theory parameters)
 * The internal declarations defining the inductive type
 
 There are three types of internal declarations:
 
-* Type-Level internal declarations declaring the (mutaully) inductively-defined types we want to define
+* Type-Level internal declarations declaring the (mutually) inductively-defined types we want to define
 * The constructors of those types
 * Further outgoing termlevel declarations, i.e. for declaring additional properties of the inductive type
 
@@ -34,8 +34,8 @@ Here we have a typelevel `<tpl>` (of type `<tp>`), a constructor `<con>` of `<tp
 There are some restrictions on the internal declarations of derived declaration of the structural feature for inductive types for the derived declaration to be well-formed. In particular:
 
 * The body of the derived declarations must be well-formed as an MMT theory.
-* The internal declarations must be (at most) shallow polymorphicly typed
-* The constructors may not be dependently-typed, except for dependencies on arguments occuring in all constructors of the inductively-defined type
+* The internal declarations must be (at most) shallow polymorphically typed
+* The constructors may not be dependently-typed, except for dependencies on arguments occurring in all constructors of the inductively-defined type
 * The constructors may not have arguments of higher order in an inductively-defined type.
 * The outgoing declarations must be consistent with each other and the elaboration of the typelevel declarations and constructors (in particular the no-confusion declarations)
 

doc/language/inductivedefinitions.md

@@ -24,7 +24,7 @@ The types of the internal declarations given here can also be automatically infe
 
 #### Elaboration of inductive definitions
 
-Inductive definitions are elaborated to the following delarations:
+Inductive definitions are elaborated to the following delirations:
 
 * A declaration of the specified inductively-defined function for each type inductively-defined by `<indTp>`
 * A declaration axiomatizing the definition for each constructor case

doc/language/informal.md

@@ -2,6 +2,6 @@
 layout: doc
 title: Flexiformal Knowledge
 ---
-Currently, MMT concentrates on the formal subset of the [OMDoc](../philosophy/omdoc), which postulates that mathematatical knowledge should be represented [flexiformally](http://kwarc.info/kohlhase/papers/synasc13.pdf), i.e. with flexible formality. Foundational steps towards extending the structural core of MMT were taken in [Mihnea Iancu's PhD thesis](https://opus.jacobs-university.de/frontdoor/index/index/docId/721). The implementation is already very mature (and heavily used in our production workflows), but documentation has not been written yet. 
+Currently, MMT concentrates on the formal subset of the [OMDoc](../philosophy/omdoc), which postulates that mathematical knowledge should be represented [flexiformally](http://kwarc.info/kohlhase/papers/synasc13.pdf), i.e. with flexible formality. Foundational steps towards extending the structural core of MMT were taken in [Mihnea Iancu's PhD thesis](https://opus.jacobs-university.de/frontdoor/index/index/docId/721). The implementation is already very mature (and heavily used in our production workflows), but documentation has not been written yet. 
 
 The bulk of flexiformalizations in the MMT world are generated from [sTeX](http://github.com/KWARC/sTeX), a semantics-enhanced version of LaTeX which can be [converted to](https://uniformal.github.io/doc/applications/stex) flexiformal MMT. Much of this content is hosted on [MathHub](http://mathhub.info). 

doc/language/modules.md

@@ -20,13 +20,13 @@ Theories can be *nested*, like this:
 
 ![`theory <outer> : <metatheory1> =	<previousbody> theory <inner> : <metatheory2> =	<innerbody>	\GS	<laterbody> \GS`](../img/nestedtheory.png)
 
-in which case the visible context of both the inner theory as well as `<laterbody>` is `<previousbody>`, i.e. the inner theory can see all previous declarations of the outer theory, but at no point can the outer theory see inside the inner theory (unless explicitely [included](declarations.html#structures)).
+in which case the visible context of both the inner theory as well as `<laterbody>` is `<previousbody>`, i.e. the inner theory can see all previous declarations of the outer theory, but at no point can the outer theory see inside the inner theory (unless explicitly [included](declarations.html#structures)).
 
 ### Views
 
 Given two theories `A` and `B`, a **view** from `A` to `B` maps all [declarations](declarations) in `A` to expressions over symbols in `B`, while preserving *typing judgments*. i.e. if `|- a : tpA` in `A` and `v:A->B` is a view, then `|- v(a) : v(tpA)`. Hence, views are *truth preserving*. `A` is the *domain* of `v` and `B` is the *codomain*.
 
-Their conrete syntax is
+Their concrete syntax is
 
 ![`view <name> : <domain> -> <codomain> = <assignments> \GS`](../img/view.png)