-
Notifications
You must be signed in to change notification settings - Fork 22
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
297b0e1
commit 316c8c2
Showing
5 changed files
with
195 additions
and
10 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,55 @@ | ||
| <!DOCTYPE html> | ||
| <html lang="en" ng-app="QueryApp"> | ||
| <meta charset="utf-8"> | ||
| <meta name="viewport" content="width=device-width, initial-scale=1"> | ||
| <head> | ||
| <script src="/script/angularjs/angular-1.5.3/angular.min.js"></script> | ||
| <script type="text/javascript" src="/script/jquery/jquery.js"></script> | ||
| <script type="text/javascript" src="/stex/queries.js"> | ||
| </script> | ||
| <link rel="stylesheet" href="/css/bootstrap3/css/bootstrap.min.css"/> | ||
| <style> | ||
| button { | ||
| background-color: darkslategray; | ||
| } | ||
| .query-return { | ||
| font-size:x-small; | ||
| background-color: black; | ||
| color: red; | ||
| /* width: min-content; */ | ||
| height: 300px; | ||
| /* max-width: 95%; */ | ||
| overflow-y: scroll; | ||
| overflow-x: hidden; | ||
| } | ||
| .my-separator { | ||
| display:inline-block; | ||
| width:5px; | ||
| border-right: 1px solid; | ||
| height: 26px; | ||
| margin-right: 5px; | ||
| vertical-align: bottom; | ||
| } | ||
| input, select, textarea { | ||
| background-color: black; | ||
| } | ||
| </style> | ||
| </head> | ||
| <body style="background-color: #2a2a2a;color: aliceblue"> | ||
| <div class="container-fluid" ng-controller="QueryViewer"> | ||
| <h2 style="margin-top: 5px;margin-bottom: 3px">sTeX Queries</h2> | ||
| <hr/> | ||
| <b>Queries:</b> | ||
| <button ng-click="query_all()">All sTeX Symbols</button> | ||
| <button ng-click="query_all_undefined()">All <i>undefined</i> sTeX Symbols</button> | ||
| <button ng-click="query_all_with_data()">All sTeX Symbols with their macro names</button> | ||
| <hr/> | ||
| <b>Custom SPARQL Query:</b><br/>(See <a href="https://hackmd.io/@X5Y0GrH0RY-KPMg2uH7o5Q/ByvrtDbFn" target="_blank">here</a> for the ontology used) | ||
| <textarea ng-model="queryString" style="display: block;width:100%;height:150px;" rows="10" cols="50"></textarea> | ||
| <button ng-click="query_custom()">Send</button> | ||
| <hr/> | ||
| <b>Result:</b> | ||
| <pre class="query-return" id="query_return">{{n.short}} {{n.long}}</pre> | ||
| </div> | ||
|
|
||
| </body> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,42 @@ | ||
| angular.module('QueryApp', []).controller('QueryViewer', [ '$scope', '$http', function($scope, $http) { | ||
|
|
||
|
|
||
|
|
||
| $scope.query_test = function() { | ||
| document.getElementById("query_return").innerHTML = "Loading..."; | ||
| $http.get('/:sTeX/query/test').success(function(data) { | ||
| document.getElementById("query_return").innerHTML = JSON.stringify(data,null,2); | ||
| }); | ||
| }; | ||
|
|
||
|
|
||
|
|
||
| $scope.query_all = function() { | ||
| document.getElementById("query_return").innerHTML = "Loading..."; | ||
| $http.get('/:sTeX/query/all').success(function(data) { | ||
| document.getElementById("query_return").innerHTML = JSON.stringify(data,null,2); | ||
| }); | ||
| }; | ||
| $scope.query_all_undefined = function() { | ||
| document.getElementById("query_return").innerHTML = "Loading..."; | ||
| $http.get('/:sTeX/query/all_undefined').success(function(data) { | ||
| document.getElementById("query_return").innerHTML = JSON.stringify(data,null,2); | ||
| }); | ||
| }; | ||
| $scope.query_all_with_data = function() { | ||
| document.getElementById("query_return").innerHTML = "Loading..."; | ||
| $http.get('/:sTeX/query/all_with_data').success(function(data) { | ||
| document.getElementById("query_return").innerHTML = JSON.stringify(data,null,2); | ||
| }); | ||
| }; | ||
| $scope.do_query = function(s) { | ||
| document.getElementById("query_return").innerHTML = "Loading..."; | ||
| $http.post('/:query/sparql',s).success(function(data) { | ||
| document.getElementById("query_return").innerHTML = JSON.stringify(data,null,2); | ||
| }); | ||
| }; | ||
| $scope.queryString ="SELECT ?x WHERE { \n <http://mathhub.info/MiKoMH/AI/course/notes/notes.omdoc#> (<http://mathhub.info/ulo#crossrefs>|<http://mathhub.info/ulo#specifies>|<http://mathhub.info/ulo#contains>|<http://mathhub.info/ulo#has-language-module>)+ ?x .\n ?x <http://www.w3.org/1999/02/22-rdf-syntax-ns#type> <http://mathhub.info/ulo#constant> .\n}"; | ||
| $scope.query_custom = function() { | ||
| $scope.do_query($scope.queryString) | ||
| }; | ||
| }]); |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
83 changes: 83 additions & 0 deletions
83
src/mmt-stex/src/info/kwarc/mmt/stex/Extensions/QueryExtension.scala
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,83 @@ | ||
| package info.kwarc.mmt.stex.Extensions | ||
|
|
||
| import info.kwarc.mmt.api.{GlobalName, Path} | ||
| import info.kwarc.mmt.api.ontology.SPARQL.T | ||
| import info.kwarc.mmt.api.ontology.ULO | ||
| import info.kwarc.mmt.api.utils.{JSONArray, JSONNull, JSONObject, JSONString} | ||
| import info.kwarc.mmt.api.web.ServerResponse.{JsonResponse, ResourceResponse} | ||
| import info.kwarc.mmt.api.web.{ServerRequest, ServerResponse} | ||
| import info.kwarc.mmt.stex.STeXServer | ||
|
|
||
| trait QueryExtension { this : STeXServer => | ||
| protected def queryRequest(request: ServerRequest): ServerResponse = { | ||
| request.path.lastOption match { | ||
| case Some("all") => | ||
| JsonResponse(JSONArray(getAll.map(p => JSONString(p.toString)) :_*)) | ||
| case Some("all_undefined") => | ||
| JsonResponse(JSONArray(undefineds.map(p => JSONString(p.toString)): _*)) | ||
| case Some("all_with_data") => | ||
| JsonResponse(JSONArray(symbols_with_stuff.map(p => | ||
| JSONObject( | ||
| ("path", JSONString(p._1.toString)), | ||
| ("macro", p._2.map(s => JSONString("\\" + s)).getOrElse(JSONNull)), | ||
| //("notations", JSONArray(p._3.map(JSONString): _*)) | ||
| )):_*)) | ||
| case Some("test") => | ||
| JsonResponse(JSONArray(test.map(p => JSONString(p.toString)): _*)) | ||
| case _ => | ||
| ResourceResponse("stex/queries.html") | ||
| } | ||
| } | ||
|
|
||
| private lazy val archives = controller.backend.getArchives.filter { a => | ||
| a.properties.get("format").contains("stex") | ||
| } | ||
|
|
||
| private lazy val getAll: List[Path] = { // TODO hacky; should be more systematic | ||
| archives.flatMap(a => { | ||
| import info.kwarc.mmt.api.ontology.SPARQL._ | ||
| controller.depstore.query( | ||
| SELECT("x") WHERE ( | ||
| ( | ||
| T(Subject(s"mmt://memory/archive#${a.id}"), ULO.contains, V("y")) UNION | ||
| T(Subject(s"mmt://memory//archive#${a.id}"), ULO.contains, V("y")) | ||
| ) AND | ||
| T(V("y"),(ULO.contains | ULO.declares | ULO.specifies)+,V("x")) AND | ||
| HASTYPE(V("x"),ULO.constant) | ||
| ) | ||
| ).getPaths.filter(p => !p.asInstanceOf[GlobalName].module.parent.last.endsWith(".omdoc")) | ||
| }) | ||
| } | ||
|
|
||
| private def symbols_with_stuff: List[(Path,Option[String])] = { | ||
| getAll.map{p => | ||
| (p, | ||
| controller.getO(p).flatMap(SHTMLContentManagement.getMacroName), | ||
| //SHTMLContentManagement.getNotations(p.asInstanceOf[GlobalName])(controller).map{n => n.notation.toString} | ||
| ) | ||
| } | ||
| } | ||
|
|
||
| private def undefineds: List[Path] = { | ||
| getAll.filter{p => | ||
| import info.kwarc.mmt.api.ontology.SPARQL._ | ||
| controller.depstore.query( | ||
| SELECT("x") WHERE ( | ||
| T(p,ULO.docref,V("x")) UNION T(V("x"),ULO.defines,p) | ||
| ) | ||
| ).getPaths.isEmpty | ||
| } | ||
| } | ||
|
|
||
| private def test: List[Path] = { | ||
| archives.flatMap(a => { | ||
| import info.kwarc.mmt.api.ontology.SPARQL._ | ||
| controller.depstore.query( | ||
| SELECT("x") WHERE ( | ||
| T(Subject(s"mmt://memory/archive#${a.id}"), ULO.contains, V("x")) UNION | ||
| T(Subject(s"mmt://memory//archive#${a.id}"), ULO.contains, V("x")) | ||
| ) | ||
| ).getPaths | ||
| }) | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters