Commit Graph

  • b9c5109aaf pref: prefetch search data Xubai Wang 2022-02-20 23:05:35 +0800
  • 9f13773a7d refactor: use json ext instead of bmp Xubai Wang 2022-02-20 22:54:57 +0800
  • a86c384354 fix: Readd equations for instances Henrik Böving 2022-02-20 13:52:57 +0100
  • b87c1cc1de feat: Better equation Handling Henrik Böving 2022-02-20 13:45:18 +0100
  • 87a8b8feb0
    Merge pull request #33 from xubaiw/docstring Henrik Böving 2022-02-20 11:59:44 +0100
  • 2b97d88059 Merge branch 'docstring' of https://github.com/xubaiw/doc-gen4 into docstring Xubai Wang 2022-02-20 13:37:03 +0800
  • 2151813fe5 feat: allow intra link in code block Xubai Wang 2022-02-20 13:28:48 +0800
  • ad4d77a9c9 fix: change same end maching Xubai Wang 2022-02-20 05:03:44 +0800
  • 4c2d67cfca fix: change same end maching Xubai Wang 2022-02-20 05:03:44 +0800
  • 794923a997 fix: update Unicode.lean Xubai Wang 2022-02-20 04:50:04 +0800
  • 189e5dacdb Merge remote-tracking branch 'upstream/main' into docstring Xubai Wang 2022-02-20 03:40:55 +0800
  • 3acfc510b4 fix: no overmatch for intra link Xubai Wang 2022-02-20 03:28:03 +0800
  • 5e550c7833 refactor: docstring between basic and extra info clean up code Xubai Wang 2022-02-20 03:14:58 +0800
  • d0714c3aab chore: Don't hard code the path seps in the build dir Henrik Böving 2022-02-19 18:15:43 +0100
  • bd9ab34655
    Merge pull request #34 from xubaiw/parent-module-nav Henrik Böving 2022-02-18 22:34:57 +0100
  • 1ef736c014 fix: use flattened Html element Xubai Wang 2022-02-19 02:07:25 +0800
  • c31aef8e87 fix: remove redundant link to parent module Xubai Wang 2022-02-19 01:54:20 +0800
  • 52d087a189 Merge branch 'parent-module-nav' of https://github.com/xubaiw/doc-gen4 into parent-module-nav Xubai Wang 2022-02-18 14:12:07 +0800
  • 2f5a95b312 fix: add nav link to non leaf node modules Xubai Wang 2022-02-18 14:03:54 +0800
  • 828449ebb4 fix: add nav link to non leaf node modules Xubai Wang 2022-02-18 14:03:54 +0800
  • 3687b3466a refactor: clean up docstring module Xubai Wang 2022-02-18 12:52:01 +0800
  • d8a5f52c10 fix: fix docstring order Xubai Wang 2022-02-18 11:28:44 +0800
  • 0724806fe6 Merge branch 'docstring' of https://github.com/xubaiw/doc-gen4 into docstring Xubai Wang 2022-02-18 04:01:34 +0800
  • cce4285c96 fix: intersperse code contents Xubai Wang 2022-02-18 04:01:31 +0800
  • 5ce1ce9fe7
    Merge branch 'main' into docstring 王虚白 2022-02-18 03:38:20 +0800
  • 5dc3ab855f feat: config mathjax like doc-gen Xubai Wang 2022-02-18 03:27:00 +0800
  • 9550d1c92e refactor: use ## for intra doc Xubai Wang 2022-02-18 03:26:38 +0800
  • 89f5951f2d feat: add mathjax equation support Xubai Wang 2022-02-18 03:10:48 +0800
  • 2dac93d360 fix: fix noncomputable Henrik Böving 2022-02-17 18:59:42 +0100
  • 0b9a9f0bdc fix: remove intra link in code block Xubai Wang 2022-02-18 01:39:02 +0800
  • 11bb2af57a feat: add auto link Xubai Wang 2022-02-18 00:46:02 +0800
  • 97ddf05ab6 fix: add root to relative href Xubai Wang 2022-02-17 21:26:02 +0800
  • 1729f4aa71 fix: fix docstring heading id Xubai Wang 2022-02-17 15:26:17 +0800
  • 5790172eab fix: doc string for all DocInfo Xubai Wang 2022-02-17 13:53:29 +0800
  • b7c6a98969 refactor: separate docstring code Xubai Wang 2022-02-17 13:47:38 +0800
  • 5679be6bbc chore: bump lean version update cmark version Xubai Wang 2022-02-17 08:54:06 +0800
  • d3ce268d63 feat: mod doc heading attributes Xubai Wang 2022-02-16 02:19:40 +0800
  • 385a38a003 feat: basic mod doc without attributes Xubai Wang 2022-02-16 01:06:46 +0800
  • 8da2e2a63d feat: basic docstring support Xubai Wang 2022-02-15 19:27:12 +0800
  • 28dfc14530 fix: arity in the extern attribute Henrik Böving 2022-02-16 21:24:42 +0100
  • 7d43c83178
    Merge pull request #29 from leanprover/search Henrik Böving 2022-02-13 15:56:08 +0100
  • e6cc03b095 fix: Fix computability Henrik Böving 2022-02-13 15:52:09 +0100
  • 5fd2585c55 feat: Implement the rest of search Henrik Böving 2022-02-13 15:42:15 +0100
  • c42db4328a feat: export search.js info Henrik Böving 2022-02-13 15:03:49 +0100
  • 4b9b7d77d5 chore: Update doc-gen search js Henrik Böving 2022-02-13 14:25:37 +0100
  • 96c8a048e3
    Merge pull request #28 from leanprover/modifiers Henrik Böving 2022-02-13 03:35:21 +0100
  • d700da7284 feat: Attributes Henrik Böving 2022-02-13 03:32:53 +0100
  • 59e50943d6 feat: mark noncomputable defs and instances Henrik Böving 2022-02-12 15:57:45 +0100
  • d39b14cf7a chore: bump toolchain, bye auto pure Henrik Böving 2022-02-12 15:09:13 +0100
  • 00bf10c6f0 chore: bump toolchain Henrik Böving 2022-02-09 22:45:28 +0100
  • 8059940c30 feat: class inductives Henrik Böving 2022-02-06 20:14:36 +0100
  • 27f8b50763 feat: tag abbrevs Henrik Böving 2022-02-06 17:28:56 +0100
  • c2d18fe3b1 feat: tag declarations with unsafe and partial Henrik Böving 2022-02-06 17:06:22 +0100
  • 4490b1e674
    Merge pull request #27 from leanprover/equations Henrik Böving 2022-02-05 02:34:15 +0100
  • 5ef4ead859
    Merge branch 'main' into equations Henrik Böving 2022-02-05 02:31:00 +0100
  • 117c94031f feat: equations for simple functions Henrik Böving 2022-02-05 02:26:03 +0100
  • 419c1eb1e6 feat: equations for instances Henrik Böving 2022-02-04 22:48:08 +0100
  • f54c192e6f feat: equations Henrik Böving 2022-02-02 11:22:15 +0100
  • 2e62f636f4
    Merge pull request #26 from leanprover/custom-ctors Henrik Böving 2022-02-02 12:56:30 +0100
  • 4d63f90449 feat: Custom structure ctors Henrik Böving 2022-02-02 12:53:04 +0100
  • b1abc677a0
    Merge pull request #24 from gebner/navbarheaders Henrik Böving 2022-01-20 20:18:41 +0100
  • fd5280f30a fix: print usage when called without arguments Gabriel Ebner 2022-01-20 15:03:10 +0100
  • 5ed0a8e99f fix: do not show top-level modules twice in navbar Gabriel Ebner 2022-01-20 15:01:51 +0100
  • 69b5ee76d3 chore: use attribute spreads Gabriel Ebner 2022-01-20 14:51:24 +0100
  • e350c16417 feat: `<div [attrArray] />` Gabriel Ebner 2022-01-20 14:49:50 +0100
  • 0be10cfad6
    Merge pull request #21 from leanprover/imports Henrik Böving 2022-01-16 14:29:13 +0100
  • 9ac4eb5062 feat: imports, imported by Henrik Böving 2022-01-16 14:22:53 +0100
  • 735bfa35a7 chore: update compiler version Henrik Böving 2022-01-15 15:35:52 +0100
  • 1edf4bbdab
    Merge pull request #20 from leanprover/fix-anonymous-arrows Henrik Böving 2022-01-15 15:17:44 +0100
  • 4a3e22490f fix: Printing of argument names with macro scopes Henrik Böving 2022-01-15 15:12:55 +0100
  • b93e1c9f54
    Merge pull request #19 from leanprover/source-links Henrik Böving 2022-01-14 13:38:58 +0100
  • f7f8138e09 feat: basic source links Henrik Böving 2022-01-09 16:57:19 +0100
  • 0751cea667
    Merge pull request #18 from leanprover/constructor-links Henrik Böving 2022-01-09 14:10:25 +0100
  • 0754b43873 feat: fix links to inductive ctors and structure fields Henrik Böving 2022-01-09 14:07:50 +0100
  • b90644cfd2
    Merge pull request #17 from leanprover/sidebar-names Henrik Böving 2022-01-07 18:29:01 +0100
  • 6128791cce chore: Sort the declarations internally already Henrik Böving 2022-01-07 18:25:26 +0100
  • 2de568d5ca feat: List of declarations in internal navbar Henrik Böving 2022-01-07 17:43:49 +0100
  • 82f63cb613 feat: parameterize the URL root for links in the HTML Henrik Böving 2022-01-07 10:56:39 +0100
  • 49fdb6279d chore: Switch to leanprover community bot email for automated doc updates Henrik Böving 2022-01-07 10:44:11 +0100
  • 08c1770655 Merge pull request #16 from leanprover/cicd Henrik Böving 2022-01-07 10:32:49 +0100
  • 93f32971ec feat: CI and auto documentation preview for mathlib4 Henrik Böving 2022-01-06 22:55:29 +0100
  • ec4d114b43 feat: show all declarations in the correct order Henrik Böving 2022-01-06 17:30:33 +0100
  • eae71c61a3
    Merge pull request #14 from leanprover/class Henrik Böving 2022-01-06 14:52:21 +0100
  • b777250338 feat: list instances of classes Henrik Böving 2022-01-06 14:51:46 +0100
  • 87f959e11d feat: basic structure like information for classes Henrik Böving 2022-01-06 14:28:41 +0100
  • e67ea1d1f0 feat: change CSS to acount for classes and instances Henrik Böving 2022-01-06 14:19:14 +0100
  • 598e5835e7
    Merge pull request #13 from leanprover/structure Henrik Böving 2022-01-06 02:06:10 +0100
  • f71b2ee8b9 chore: Remove obsolete TODOs Henrik Böving 2022-01-06 02:05:23 +0100
  • 8a58752c56 feat: display structures and their fields properly Henrik Böving 2022-01-04 08:23:39 +0100
  • 3f1c0ecd77 chore: Update lean-toolchain Henrik Böving 2022-01-04 08:24:59 +0100
  • 3adb8e71d1 feat: Show inductive constructors properly Henrik Böving 2022-01-03 18:22:12 +0100
  • 85d1e4608c
    Merge pull request #1 from hargoniX/main Henrik Böving 2022-01-03 14:29:58 +0100
  • 02d8c528d9 feat: Show arguments of types of decls separately Henrik Böving 2021-12-25 16:55:30 +0100
  • 5e0956c4b0 feat: Proper linking of all constants Henrik Böving 2021-12-25 14:08:09 +0100
  • 0efbcd1f60 feat: Newline free HTML formatting Henrik Böving 2021-12-25 14:04:35 +0100
  • d18e71966c feat: Store Format instead of Syntax in DocInfo Henrik Böving 2021-12-18 00:01:31 +0100
  • 4380fe088d feat: Sanitize Syntax Henrik Böving 2021-12-17 23:53:06 +0100
  • 3c01cf1e68 feat: Name linking Henrik Böving 2021-12-17 17:20:44 +0100
  • ef716c9351 chore: Use builtin Name methods instead Henrik Böving 2021-12-17 17:04:56 +0100
  • 2df4891c9f feat: Setup infrastructure for type HTMLifying Henrik Böving 2021-12-17 15:59:43 +0100