summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* actually usable code structure for isabelle-protoHEADmasterstuebinm2021-10-263-95/+67
|
* better code structure for isabelle-protostuebinm2021-10-263-135/+148
|
* slightly less hacky proof of conceptstuebinm2021-10-262-70/+145
|
* proof of concept: talking to `isabelle server`stuebinm2021-09-215-21/+632
| | | | | for now this just checks a file given on the command line, and panics if anything at all goes wrong.
* update readmestuebinm2021-09-041-54/+33
|
* restructure nix stuffstuebinm2021-09-044-13/+24
| | | | | There's now a packageset in default.nix, and individual files for the rust and shell script stuff.
* isabat: move into /bin dir in packagestuebinm2021-09-041-1/+2
|
* update nix sourcesstuebinm2021-09-042-7/+7
|
* add some sanity checks to isabatstuebinm2021-09-042-1/+19
| | | | (will now print errors if bat/the highlighter theme is missing)
* add isabat scriptstuebinm2021-09-042-0/+34
| | | | | This just calls the isabelle2nix util and pipes its output directly into bat, resulting in a somewhat usable cli tool for .thy files.
* package name: isabelle-dump → isabelle-unicodestuebinm2021-09-041-1/+1
|
* crate name: util → isabelle2unicodestuebinm2021-09-043-2/+2
|
* basic sublime text highlighter syntax (for bat)stuebinm2021-09-041-0/+47
| | | | | | | | | | | | | | | This is mostly based on the syntax generated by `isabelle vscode_grammar` for the list of keywords; choice of scopes is heavily biased by my understanding of the subset of isabelle syntax I actually know about. For now, it makes no attempt to actually understand anything of what is going on in a file (except for strings/comments) and simply matches keywords. Note that scope selection does not make sense, and is mostly based on looking into which scopes are assigned useful colours by common highlighter themes (mostly bat's default theme and TwoDark for now)
* somewhat pointless generalisation of a type signaturestuebinm2021-09-031-5/+7
| | | | | There's no real reason for this other than that I wanted to know if abstracting over &[T] -> T and &str -> String etc. was possible.
* remove grmtoolsstuebinm2021-09-0313-1076/+124
| | | | | | | | | | the parser using grmtools was way oversized for just doing escape sequences, and only really existed since I wanted to play around with it. The new implementation depends on no external crates, uses just an iter wrapped into a nicely composable function, and appears to be exactly equivalent (but faster).
* add nix derivationstuebinm2021-06-234-0/+221
| | | | (using naersk)
* initial commitstuebinm2021-06-2316-0/+1699
generated by cgit v1.2.3 (git 2.25.1) at 2024-05-04 18:53:06 +0000