Commit 44eaa685b24da5795a0360cb78d5ce559a9b79d3
1 parent
feda5839
add "current page" in reserved key words for web session
remove Int x (mod Int y) which already exists somewhere else
Showing
2 changed files
with
21 additions
and
15 deletions
Show diff stats
web/CXM_generic_table.anubis
| @@ -420,16 +420,16 @@ define List(HTML_Cell(HTML_In_Form)) | @@ -420,16 +420,16 @@ define List(HTML_Cell(HTML_In_Form)) | ||
| 420 | ] | 420 | ] |
| 421 | }. | 421 | }. |
| 422 | 422 | ||
| 423 | -public define Int | ||
| 424 | - Int x (mod Int y) | ||
| 425 | - = | ||
| 426 | - if x / y is | ||
| 427 | - { | ||
| 428 | - failure then 0, | ||
| 429 | - success(result) then | ||
| 430 | - if result is (q, r) then r | ||
| 431 | - }. | ||
| 432 | - | 423 | +//public define Int |
| 424 | +// Int x (mod Int y) | ||
| 425 | +// = | ||
| 426 | +// if x / y is | ||
| 427 | +// { | ||
| 428 | +// failure then 0, | ||
| 429 | +// success(result) then | ||
| 430 | +// if result is (q, r) then r | ||
| 431 | +// }. | ||
| 432 | +// | ||
| 433 | 433 | ||
| 434 | 434 | ||
| 435 | public define HTML_In_Form | 435 | public define HTML_In_Form |
web/CXM_web_session.anubis
| @@ -16,11 +16,12 @@ read CXM_web_dump.anubis | @@ -16,11 +16,12 @@ read CXM_web_dump.anubis | ||
| 16 | 16 | ||
| 17 | reserved fields keywords | 17 | reserved fields keywords |
| 18 | 18 | ||
| 19 | - "AWS" String | ||
| 20 | - "AWS_CURRENT_PAGE_TITLE" String current web page title | ||
| 21 | - "AWS_CURRENT_APP" String current web application | ||
| 22 | - "AWS_CURRENT_SPACE" String current web space in application | ||
| 23 | - "AWS_PAGE_RENDERER" String current | 19 | + "AWS_CURRENT_PAGE_TITLE" String current web page title |
| 20 | + "AWS_CURRENT_PAGE" String current web page | ||
| 21 | + "AWS_CURRENT_APP" String current web application | ||
| 22 | + "AWS_CURRENT_SPACE" String current web space in application | ||
| 23 | + "AWS_CURRENT_CONTENT" String current in the web space | ||
| 24 | + "AWS_CURRENT_PAGE_RENDERER" String current page renderer | ||
| 24 | 25 | ||
| 25 | //"AWS_CURRENT_LEFT_MENU" Left_Menu current left menu on the page | 26 | //"AWS_CURRENT_LEFT_MENU" Left_Menu current left menu on the page |
| 26 | //"AWS_CURRENT_MENU" Menu current menu, on the top of the page | 27 | //"AWS_CURRENT_MENU" Menu current menu, on the top of the page |
| @@ -66,6 +67,7 @@ public define WEB_Session_No_Var | @@ -66,6 +67,7 @@ public define WEB_Session_No_Var | ||
| 66 | 67 | ||
| 67 | /************************************************/ | 68 | /************************************************/ |
| 68 | "AWS_CURRENT_PAGE_TITLE" String current web page title | 69 | "AWS_CURRENT_PAGE_TITLE" String current web page title |
| 70 | + "AWS_CURRENT_PAGE" String current web page | ||
| 69 | "AWS_CURRENT_APP" String current web application | 71 | "AWS_CURRENT_APP" String current web application |
| 70 | "AWS_CURRENT_SPACE" String current web space in application | 72 | "AWS_CURRENT_SPACE" String current web space in application |
| 71 | "AWS_CURRENT_CONTENT" String current in the web space | 73 | "AWS_CURRENT_CONTENT" String current in the web space |
| @@ -83,6 +85,10 @@ public define One set_web_content(WEB_Session s, String n)= replace_String(s | @@ -83,6 +85,10 @@ public define One set_web_content(WEB_Session s, String n)= replace_String(s | ||
| 83 | public define One set_web_content(Var(List(Session_Field)) fields, String n)= replace_String(fields, "AWS_CURRENT_CONTENT", n). | 85 | public define One set_web_content(Var(List(Session_Field)) fields, String n)= replace_String(fields, "AWS_CURRENT_CONTENT", n). |
| 84 | public define String get_web_content(WEB_Session s) = get_String (s.fields, "AWS_CURRENT_CONTENT", ""). | 86 | public define String get_web_content(WEB_Session s) = get_String (s.fields, "AWS_CURRENT_CONTENT", ""). |
| 85 | 87 | ||
| 88 | +public define One set_page(WEB_Session s, String n)= replace_String(s.fields, "AWS_CURRENT_PAGE", n). | ||
| 89 | +public define One set_page(Var(List(Session_Field)) fields, String n)= replace_String(fields, "AWS_CURRENT_PAGE", n). | ||
| 90 | +public define String get_page(WEB_Session s) = get_String (s.fields, "AWS_CURRENT_PAGE", ""). | ||
| 91 | + | ||
| 86 | public define One set_page_title(WEB_Session s, String n)= replace_String(s.fields, "AWS_CURRENT_PAGE_TITLE", n). | 92 | public define One set_page_title(WEB_Session s, String n)= replace_String(s.fields, "AWS_CURRENT_PAGE_TITLE", n). |
| 87 | public define One set_page_title(Var(List(Session_Field)) fields, String n)= replace_String(fields, "AWS_CURRENT_PAGE_TITLE", n). | 93 | public define One set_page_title(Var(List(Session_Field)) fields, String n)= replace_String(fields, "AWS_CURRENT_PAGE_TITLE", n). |
| 88 | public define String get_page_title(WEB_Session s) = get_String (s.fields, "AWS_CURRENT_PAGE_TITLE", ""). | 94 | public define String get_page_title(WEB_Session s) = get_String (s.fields, "AWS_CURRENT_PAGE_TITLE", ""). |