From: Stefano Zacchiroli Date: Tue, 21 Jan 2003 11:38:40 +0000 (+0000) Subject: added html templates and pages X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=000ee25879c192864cfaa0ebc27cc91a896378df;p=helm.git added html templates and pages --- diff --git a/helm/searchEngine/html/aliaslist.html b/helm/searchEngine/html/aliaslist.html new file mode 100644 index 000000000..c74e2ca59 --- /dev/null +++ b/helm/searchEngine/html/aliaslist.html @@ -0,0 +1,79 @@ + + + + + +
+alias + + + +
+ +
+ +
+ + diff --git a/helm/searchEngine/html/blank.html b/helm/searchEngine/html/blank.html new file mode 100644 index 000000000..903e3169b --- /dev/null +++ b/helm/searchEngine/html/blank.html @@ -0,0 +1,4 @@ + + + + \ No newline at end of file diff --git a/helm/searchEngine/html/boole.html b/helm/searchEngine/html/boole.html new file mode 100644 index 000000000..015ac57c8 --- /dev/null +++ b/helm/searchEngine/html/boole.html @@ -0,0 +1,66 @@ + + + + + +

+ +

+

Select one of the following:

+
+
+ ( [boole] )
+ [boole]
+ [boole] [boole]
+ [val] +[val]
+
+ +
+ + \ No newline at end of file diff --git a/helm/searchEngine/html/editor.html b/helm/searchEngine/html/editor.html new file mode 100644 index 000000000..b032f0c4c --- /dev/null +++ b/helm/searchEngine/html/editor.html @@ -0,0 +1,120 @@ + + + + + + + +
+
+ +
 +
+
+
+
+ + + + + + diff --git a/helm/searchEngine/html/editorpdq.html b/helm/searchEngine/html/editorpdq.html new file mode 100644 index 000000000..ae49abc02 --- /dev/null +++ b/helm/searchEngine/html/editorpdq.html @@ -0,0 +1,90 @@ + + + + + +
+ Your list of alias. + +
+
Your expression.
+ + + +
+ + + diff --git a/helm/searchEngine/html/expnamedsubst.html b/helm/searchEngine/html/expnamedsubst.html new file mode 100644 index 000000000..bb8173389 --- /dev/null +++ b/helm/searchEngine/html/expnamedsubst.html @@ -0,0 +1,78 @@ + + + + + +You must now enter a list of named_subst. A named_subst is an Id or a Varuri followed by ":=" followed by an expression. +You may enter as many of them as you want (even none), after each one click the button "add" or press enter and it will be added. When you are done, click "done". +
+
+ Insert here the Id or the Uri you want to add. + +
+ +
+ +
+ + \ No newline at end of file diff --git a/helm/searchEngine/html/expr.html b/helm/searchEngine/html/expr.html new file mode 100644 index 000000000..291b40cc2 --- /dev/null +++ b/helm/searchEngine/html/expr.html @@ -0,0 +1,51 @@ + + + + + +You are entering an expression. Select one of the following. +
+\[Genid][Expr].[Expr]
+![Genid]:[Expr].[Expr]
+[Expr]->[Expr]
+([Expr])->[Expr]
+
+ ( [Expr list] )
+ +
+ + \ No newline at end of file diff --git a/helm/searchEngine/html/genid.html b/helm/searchEngine/html/genid.html new file mode 100644 index 000000000..8883ca369 --- /dev/null +++ b/helm/searchEngine/html/genid.html @@ -0,0 +1,27 @@ + + + + + +You are now entering a Genid. It may be a simple Id, or an Uri followed by nothing or by an Exp_Named_Subst. +
+ Insert here the Id +
+ Or insert here the Uri. The uri may not be a Conuri.
+ +
+ + diff --git a/helm/searchEngine/html/grammar.html b/helm/searchEngine/html/grammar.html new file mode 100644 index 000000000..a18b27cd7 --- /dev/null +++ b/helm/searchEngine/html/grammar.html @@ -0,0 +1,76 @@ + + + + + +

<string>::= '"' [ "\" . | '^ " \' ] * '"' + +

<path>::= <string> [ "/" <string> ] * + +

<string_list>::= <string> [ "," <string> ] * + +

<alpha>::= [ 'A - Z' | 'a - z' |' :_' ] + + +

<number>::= [ '0 - 9' ] + + +

<id>::= <alpha> [ <alpha> | <number> ] * + +

<rvar>::= "@" <id> + +

<svar>::= "%" <id> + +

<vvar>::= "$" <id> + +

<refine>::= [ "sub" | "super" ] ? + +

<qualifier>::= [ "inverse" ] ? <refine> <path> + +

<assign>::= <vvar> "<-" <path> + +

<attr_list>::= [ "attr" <assign> [ "," <assign>] * ] ? + +

<set>::= "ref" <val>
+                 +| "pattern" <val>
+                 +| <svar>
+                 +| <rvar>
+                 +| "(" <set> ")"
+                 +| "relation" <qualifier> <val> <attr_list>
+                 +| "select" <rvar> "in" <set> "where" <boole>
+                 +| <set> [ "union" | "intersect" | "diff" ] <set>
+                 +| "let" <svar> "be" <set> "in" <set>
+                 +| "let" <vvar> "be" <val> "in" <set>
+ +

<boole>::= [ "false" | "true" ]
+                    +| "(" <boole> ")"
+                    +| [ "not" | "ex" ] <boole>
+                    +| <boole> [ "and" | "or" ] <boole>
+                    +| <val> [ "sub" | "meet" | "eq" ] <val>
+ +

<val>::= "{" [ <string_list> ] ? "}"
+                 +| <string>
+                 +| "refof" <set>
+                 +| <rvar> "." <vvar>
+                 +| <vvar>
+                 +| "(" <val> ")"
+                 +| "property" <qualifier> <val> + + \ No newline at end of file diff --git a/helm/searchEngine/html/grammarpdq.html b/helm/searchEngine/html/grammarpdq.html new file mode 100644 index 000000000..55fec7673 --- /dev/null +++ b/helm/searchEngine/html/grammarpdq.html @@ -0,0 +1,22 @@ + + + + + + +

<Id>::=[ 'A-Z' | 'a-z' ][ 'A-Z' | 'a-z' | '0-9' | \- | _ | \' ]* + +

<Uri>::=<Conuri> | <Varuri> | <Indtyuri> | <Indconuri> + +

<Conuri>::="cic:/" [<Id "/" ]*<Id> ".con" + +

<Varuri>::="cic:/" [<Id> "/" ]*<Id> ".var" + +

<Indtyuri>::="cic:/" [<Id> "/" ]*<Id> ".ind#1/" ['0-9']+ + +

<Indconuri>::="cic:/" [<Id> "/" ]*<Id> ".ind#1/" ['0-9']+ "/" ['0-9']+ + +

<Exp_Named_Subst>::="{" [ [ [<Id> | <Varuri> ] ":=" <Expression> ";" ]* [ [<Id> | <Varuri> ] ":=" <Expression> ] ]? "}" + + \ No newline at end of file diff --git a/helm/searchEngine/html/index.html b/helm/searchEngine/html/index.html new file mode 100644 index 000000000..d26024e56 --- /dev/null +++ b/helm/searchEngine/html/index.html @@ -0,0 +1,346 @@ + + + + + + diff --git a/helm/searchEngine/html/loc_obj.html b/helm/searchEngine/html/loc_obj.html new file mode 100644 index 000000000..97e831400 --- /dev/null +++ b/helm/searchEngine/html/loc_obj.html @@ -0,0 +1,18 @@ + + + + + +

+ +Insert here the name of the object you want to search. +
+
+ + diff --git a/helm/searchEngine/html/mat_con.html b/helm/searchEngine/html/mat_con.html new file mode 100644 index 000000000..3f4d37e41 --- /dev/null +++ b/helm/searchEngine/html/mat_con.html @@ -0,0 +1,16 @@ + + + + + + + \ No newline at end of file diff --git a/helm/searchEngine/html/paginacollink.html b/helm/searchEngine/html/paginacollink.html new file mode 100644 index 000000000..83f41bcf9 --- /dev/null +++ b/helm/searchEngine/html/paginacollink.html @@ -0,0 +1,13 @@ + + + + + +Query composer + + diff --git a/helm/searchEngine/html/pdq.html b/helm/searchEngine/html/pdq.html new file mode 100644 index 000000000..9088ad495 --- /dev/null +++ b/helm/searchEngine/html/pdq.html @@ -0,0 +1,130 @@ + + + + + + diff --git a/helm/searchEngine/html/query_choice.html b/helm/searchEngine/html/query_choice.html new file mode 100644 index 000000000..8cb800ffd --- /dev/null +++ b/helm/searchEngine/html/query_choice.html @@ -0,0 +1,32 @@ + + + + + +
+ +
+ Locate Object
+ Match Conclusion
+ Search Pattern +
+
+ + + diff --git a/helm/searchEngine/html/set.html b/helm/searchEngine/html/set.html new file mode 100644 index 000000000..3154d937a --- /dev/null +++ b/helm/searchEngine/html/set.html @@ -0,0 +1,157 @@ + + + + + +

+ +

+

Select one of the following:

+
+ ref [val]
+ pattern [val]
+ +
+ +
+ ( [set] )
+ relation + + + +[val] +
+ select @ +in [set] where [boole]
[set] + +[set]
+ let % be [set] in [set]
+ let $ be [val] in [set]
+
+ +