Skip to content

Commit

Permalink
Merge pull request #4700 from martinbaker/mydoc
Browse files Browse the repository at this point in the history
Add Documentation for Elaborator Reflection
  • Loading branch information
melted authored Dec 2, 2019
2 parents 21434e0 + cf3071d commit 0736219
Show file tree
Hide file tree
Showing 50 changed files with 7,552 additions and 6 deletions.
13 changes: 13 additions & 0 deletions docs/_static/theme_overrides.css
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
/* override table width restrictions */
@media screen and (min-width: 767px) {

.wy-table-responsive table td {
/* !important prevents the common CSS stylesheets from overriding
this as on RTD they are loaded after this stylesheet */
white-space: normal !important;
}

.wy-table-responsive {
overflow: visible !important;
}
}
8 changes: 7 additions & 1 deletion docs/conf.py
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@

# General information about the project.
project = u'Idris'
copyright = u'2017, The Idris Community'
copyright = u'2017-2019, The Idris Community'
author = u'The Idris Community'

# The version info for the project you're documenting, acts as replacement for
Expand Down Expand Up @@ -151,6 +151,12 @@
# so a file named "default.css" will overwrite the builtin "default.css".
html_static_path = ['_static']

html_context = {
'css_files': [
'_static/theme_overrides.css', # override wide tables in RTD theme
],
}

# Add any extra paths that contain custom files (such as robots.txt or
# .htaccess) here, relative to this directory. These files are copied
# directly to the root of the documentation.
Expand Down
16 changes: 16 additions & 0 deletions docs/image/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
Many of the images in this directory have two files with the same name but a different extension:

* The SVG file, being vector graphics, is best for drawing and modifying.
* The PNG file, being raster graphics, gives more consistent rendering.

The image has therefore been generated as an SVG file and then exported to the PNG file.

So, if you need to modify an image, I suggest the following sequence:

* Edit the SVG file using a suitable editor (I use Inkscape).
* Export the changes to the PNG file, overwriting the old version.
* upload both files.

Note, when exporting in Inkscape:
* Select everything first, this stops an enormous boundary being exported.
* After selecting the file to export to and clicking OK, don't forget to click on export button as well.
Binary file added docs/image/attack.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
199 changes: 199 additions & 0 deletions docs/image/attack.svg
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added docs/image/binders.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading

0 comments on commit 0736219

Please sign in to comment.