From 370067f013d0f9fd3ad4bb03184c00e8c2455586 Mon Sep 17 00:00:00 2001 From: yhirose Date: Sun, 24 May 2020 22:14:43 -0400 Subject: [PATCH] Added filters parameter to peglint and playground --- docs/index.html | 11 ++++++++--- docs/index.js | 15 ++++++++++++++- docs/native.cpp | 40 +++++++++++++++++++++++++++------------- docs/native.js | 5 +---- docs/native.wasm | Bin 417251 -> 352721 bytes docs/style.css | 4 +++- lint/peglint.cc | 39 +++++++++++++++++++++++++++++++++------ 7 files changed, 86 insertions(+), 28 deletions(-) diff --git a/docs/index.html b/docs/index.html index aa6ae3b..4588dcc 100644 --- a/docs/index.html +++ b/docs/index.html @@ -1,14 +1,14 @@ -PEG Playground - v0.1.5 +PEG Playground - v0.1.6
    -
  • Grammar:
    • +
  • Grammar
  • Valid
{{syntax}}
@@ -16,11 +16,16 @@
    -
  • Code:
    • +
  • Source Code
  • Valid
{{source}}
+
AST

+    
Optimized AST     
+      On:   
+      Filters: 
+    

     

     

   

diff --git a/docs/index.js b/docs/index.js
index 6622316..b34b229 100644
--- a/docs/index.js
+++ b/docs/index.js
@@ -27,6 +27,9 @@ codeAstOptimized.setOptions({
 })
 codeAstOptimized.renderer.$cursorLayer.element.style.opacity=0;
 
+$('#optimize').prop('checked', localStorage.getItem('optimize') == 'true');
+$('#filters').val(localStorage.getItem('filters'));
+
 function generateErrorListHTML(errors) {
   let html = '