/[mojave]/metaprl/support/display/summary.ml
ViewVC logotype

Log of /metaprl/support/display/summary.ml

Parent Directory Parent Directory | Revision Log Revision Log


Links to HEAD: (view) (download) (annotate)
Sticky Revision:

Revision 9655 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 31 18:16:04 2006 UTC (14 years, 7 months ago) by nogin
File length: 35841 byte(s)
Diff to previous 9531
- In browser mode, use "/foo" relative URLs instead of the
  "https://host:port/foo" ones whenever possible. This is needed in order to
  make it easier to access the MetaPRL session indirectly (e.g. via an ssh
  tunnel).

  Only three places will now use the FQ URL:
   - startup message 
   - autologin file
   - form passed to the external editor

- A few display form fixes and improvements.



Revision 9531 - (view) (download) (annotate) - [select for diffs]
Modified Thu Aug 24 19:04:44 2006 UTC (14 years, 10 months ago) by nogin
File length: 35807 byte(s)
Diff to previous 8705
Implemented support for "opqaue" definitions. An "opaque" definition can only
be unfolded inside the theory that it's in.

In order to use this, add the keyword "opaque" right after "define" in .ml
file.

Caveats:
 - Currently we only implement a "soft" restriction that can be easily
   circumvented. The "opaqueness" currently means that the rewrite will be
   added to the toploop resource as a "private" (not inheritable) entry. In
   other words, the definition unfolding conversion will only be visible in
   the toploop of the module that it's in, but one can easily make it visible
   outside of the module through ML.
 - Note that any resource annotation on an "opaque" definition will
   automatically be considered private (i.e. not be inherited by descendant
   theories).

Todo:
 - The syntax is currently fragile - for example, for const definitions one
   has to use "define opaque const", while "define const opaque" will be
   rejected. We should allow an arbitrary ordering of these "flags".
 - We should consider enforcing the "opaqueness" of a definition via the
   refiner's sentinels. Alternatively, we might implement both the "soft opaque"
   restriction and the "hard opaque" one, but this will probably be
   unnecessary.

P.S. I had to fix two HOAS proofs that refered to other module's definition
for no good reason. Both proofs actually became simpler as a result,
suggesting that the "opaqueness enforcement" is actually a good idea,

P.P.S. Also, a number of proofs lost some (presumably unnecessary) primitive
proof steps (probably because of the resource annotations becoming private -
see the second caveat above). Again, seems like a good thing.


Revision 8705 - (view) (download) (annotate) - [select for diffs]
Modified Wed Feb 15 06:59:08 2006 UTC (15 years, 4 months ago) by nogin
File length: 35682 byte(s)
Diff to previous 8541
- Filter_reflection: module names should not be capitalized.

- OMakefile_theories: rules for generating .p4 and .p4i for the reflected
  theories (these are pretty-printed versions of the generated OCaml code;
  useful for debugging the filter).

- OMakefile_theories: in rev 8704 I've ordered the new dependencies for the
  reflect_% files incorrectly (the theory .SUBDIRS did not have them in
  scope); fixed.

- Filter_prog: generate the show_loading debugging call at the beginning and
  end of every theory.

- A _huge_ number of theory files: removed the manual "show_loading" calls as
  they will now be automatically generated.


Revision 8541 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jan 21 00:36:59 2006 UTC (15 years, 5 months ago) by nogin
File length: 35768 byte(s)
Diff to previous 8503
Fixing a display form typo.


Revision 8503 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jan 18 07:44:07 2006 UTC (15 years, 5 months ago) by nogin
File length: 35767 byte(s)
Diff to previous 8385
*** WARNING : BREAKS BINARY COMPATIBILITY ***
***  Export your proofs before updating!  ***

This adds a private/public flag to all the resource improvements (including
annotations). The public improvements get inherited by ancestors, while
private ones remain local to the current theory.

Syntax: 

private let resource += ...
public let resource += ...

interactive foo {| public intro [AutoMustComplete]; private intro [] |} ...

The private/public flag is optional, "public" is assumed by default.

Note: short of not breaking the existing code, this is completely untested.
Will try testing tomorrow, unless Jason beats me to it.


Revision 8385 - (view) (download) (annotate) - [select for diffs]
Modified Thu Dec 29 21:34:13 2005 UTC (15 years, 5 months ago) by jyh
File length: 35516 byte(s)
Diff to previous 8261
Reformulating the Provable theorems.


Revision 8261 - (view) (download) (annotate) - [select for diffs]
Modified Sun Dec 4 04:00:26 2005 UTC (15 years, 6 months ago) by nogin
File length: 35207 byte(s)
Diff to previous 7879
Change the parse-time representation of the "default context dependencies" to
be v<|!!|> (two exclamation signs) instead of v<|v|>.


Revision 7879 - (view) (download) (annotate) - [select for diffs]
Modified Sun Oct 9 00:19:09 2005 UTC (15 years, 8 months ago) by jyh
File length: 35211 byte(s)
Diff to previous 7569
!! This breaks binary compatibility !!
!! Export your theories before doing an update !!

Two things:
    - Use omake_0_9_7_pre7/libmojave instead of the trunk libmojave
    - Added a minimal grammar to ITT

I believe I have fixed the "functional value" marshaling problem,
but PLEASE let me know if you encounter a "functional value"
problem.

This appears as follows:
 
    # save ()
    Invalid Argument:
        output_value: functional value

The workaround is to use "export ()" instead of "save ()" if this
happens.


Revision 7569 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 7 16:24:25 2005 UTC (15 years, 11 months ago) by nogin
File length: 35217 byte(s)
Diff to previous 7568
Minor display forms update


Revision 7568 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 7 06:26:56 2005 UTC (15 years, 11 months ago) by nogin
File length: 35086 byte(s)
Diff to previous 7563
Adding a preminimary implementation of the ILC basics in MetaPRL


Revision 7563 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 7 02:30:10 2005 UTC (15 years, 11 months ago) by nogin
File length: 34803 byte(s)
Diff to previous 7524
This is a huge commit that is mostly no-op:

- Updated the standard preamble text to point to the correct location for the
  documentation and to avoid mentioning Nuprl.

- Changed "Nuprl-Light" -> "MetaPRL" in a few places (amazingly, we still had
  those).

- Split the Nuprl_font file into Mpfont and Mpsymbols.

- Protected a few display forms in ITT with a "doc docoff".


Revision 7524 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 1 08:44:31 2005 UTC (15 years, 11 months ago) by nogin
File length: 34816 byte(s)
Diff to previous 7521
More comment formatting. Now every toplevel "doc" item has an _implicit_
@begin[doc]...@end[doc] wrapper around it (except for "doc docoff") and
explicit @begin[doc]...@end[doc] and @doc{...} should no longer be used.


Revision 7521 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 1 05:31:30 2005 UTC (15 years, 11 months ago) by nogin
File length: 35124 byte(s)
Diff to previous 7312
Working on making the "doc" comments more uniform.


Revision 7312 - (view) (download) (annotate) - [select for diffs]
Modified Sun May 22 20:57:44 2005 UTC (16 years, 1 month ago) by nogin
File length: 35217 byte(s)
Diff to previous 7286
Documentation fixes:

 - A lot of spelling fixes

 - Let omake know that MP_DEBUG=spell implies dependency on lib/words

 - When building the lib/english_dictionary.dat, build it in a temporary file
   first, followed by a rename to make it possible to run several instances
   of filter-spell in parallel.

 - A number of extra "doc docoff" added around display forms "let resource +="
   and other similar items

 - A few display form fixes.

 - Made the pages in the all-theories file wider.


Revision 7286 - (view) (download) (annotate) - [select for diffs]
Modified Tue May 17 12:58:04 2005 UTC (16 years, 1 month ago) by nogin
File length: 35324 byte(s)
Diff to previous 7284
TeX fixes.


Revision 7284 - (view) (download) (annotate) - [select for diffs]
Modified Tue May 17 04:36:15 2005 UTC (16 years, 1 month ago) by nogin
File length: 35300 byte(s)
Diff to previous 7249
Added a theory of "vector bindings". I still have to prove couple of theorems
(I only proved the trivial ones so far), and may be add a few more theorems.

Also, I've fixed the display form for conditional rewrites (which was wrong
when # of conditions <> 1).


Revision 7249 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 5 23:09:30 2005 UTC (16 years, 1 month ago) by nogin
File length: 35090 byte(s)
Diff to previous 7221
Renamed Ocaml!OCaml -> Ocaml!TyOCaml (to avoid clashes with Comment!OCaml).


Revision 7221 - (view) (download) (annotate) - [select for diffs]
Modified Fri Apr 15 08:39:11 2005 UTC (16 years, 2 months ago) by nogin
File length: 35086 byte(s)
Diff to previous 7102
Created a typeclass MTerm for meta-terms and changed the
Summary!meta_operators to have the MTerm type instead of Dform.


Revision 7102 - (view) (download) (annotate) - [select for diffs]
Modified Mon Apr 4 01:39:43 2005 UTC (16 years, 2 months ago) by nogin
File length: 35053 byte(s)
Diff to previous 6994
Updated display forms for the "declare" directives to match the current term
encoding of those directives.


Revision 6994 - (view) (download) (annotate) - [select for diffs]
Modified Tue Mar 22 04:40:59 2005 UTC (16 years, 3 months ago) by nogin
File length: 34417 byte(s)
Diff to previous 6923
- Iforms now do not have to be duplicated in .mli and .ml - iforms that exist
  in .mli, but not in .ml will now be automatically copied to .ml.

- No ML code is generated for iforms now; since filter_grammar handles
  iforms internally, there is no need for explicit ML code.

- The .cmoz/.cmiz data structure for iforms now contains neither proofs nor
  resources (note - MetaPRL should still be able to read older binaries).

- Removed references to arguments and conditions from the code for iforms,
  since iforms can not be conditional and can not take arguments.


Revision 6923 - (view) (download) (annotate) - [select for diffs]
Modified Tue Mar 15 03:21:25 2005 UTC (16 years, 3 months ago) by nogin
File length: 34692 byte(s)
Diff to previous 6762
Added a fake_mlrw operator to make documenting ML rewrites easier.


Revision 6762 - (view) (download) (annotate) - [select for diffs]
Modified Sat Feb 26 01:46:17 2005 UTC (16 years, 3 months ago) by nogin
File length: 34539 byte(s)
Diff to previous 6661
Added a display from for iform items; minor fix in display forms for primitive
rules.


Revision 6661 - (view) (download) (annotate) - [select for diffs]
Modified Sat Feb 12 03:44:21 2005 UTC (16 years, 4 months ago) by jyh
File length: 33820 byte(s)
Diff to previous 6624
Actually, only two files needed fixing with the new Ocaml typeclass.
I changed the name to OCaml...  It is just that OCaml is more like the
real name, and is easier to type in.


Revision 6624 - (view) (download) (annotate) - [select for diffs]
Modified Mon Feb 7 12:25:55 2005 UTC (16 years, 4 months ago) by nogin
File length: 33804 byte(s)
Diff to previous 6579
***************************************************************************
****             !!!!!         WARNING            !!!!!                ****
***************************************************************************
!!!!!           This commit breaks binary compatibility               !!!!!
!!!!!         Export all your uncommitted proofs before updating      !!!!!
!!!!!                                                                 !!!!!
!!!!!  If you export to a .prla that did not exist before, you will   !!!!!
!!!!!  to edit it manually after you update - find the line that      !!!!!
!!!!!  starts with "NPerv!cons" replace the last (third) occurrence   !!!!!
!!!!!  of "cons" with "xcons", then replace last (third) occurrence   !!!!!
!!!!!  nil" with "xnil" on the "Perv!nil" line.                       !!!!!
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!

Merging the opname_classes branch!

This commit inroduces types to MetaPRL syntax with an informal (but pretty
precise) typechecking. Hopefully Jason will write some documentation
describing how to use this.

This fixes bug 370 and bug 371.


Revision 6579 - (view) (download) (annotate) - [select for diffs]
Modified Thu Feb 3 10:03:33 2005 UTC (16 years, 4 months ago) by nogin
File length: 29985 byte(s)
Diff to previous 6574
Display forms updates to support the recently added address parameters.


Revision 6574 - (view) (download) (annotate) - [select for diffs]
Modified Thu Feb 3 08:34:46 2005 UTC (16 years, 4 months ago) by nogin
File length: 29803 byte(s)
Diff to previous 6572
This brings the support for non-sequent contexts one step closer. Now the
non-sequent contexts are properly recognized by the filter and the
corresponding address arguments are properly recognized and properly passed to
the rewriter.

The rewriter support, however, is still incomplete (this is the last missing
piece of the puzzle) - any non-trivial usage of contexts is likely to result
in Invalid_argument("...not supported...") from the rewriter.


Revision 6572 - (view) (download) (annotate) - [select for diffs]
Modified Thu Feb 3 06:28:40 2005 UTC (16 years, 4 months ago) by nogin
File length: 29112 byte(s)
Diff to previous 6444
Removing an unused opname


Revision 6444 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jan 19 21:15:05 2005 UTC (16 years, 5 months ago) by nogin
File length: 29138 byte(s)
Diff to previous 6040
No-op: removed a number of unused "open" statements


Revision 6040 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 8 05:34:20 2004 UTC (16 years, 11 months ago) by nogin
File length: 29153 byte(s)
Diff to previous 5956
A few display form updates.


Revision 5956 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jun 20 05:09:03 2004 UTC (17 years ago) by nogin
File length: 28977 byte(s)
Diff to previous 5954
- The Lm_big_int.of_string had no support for non-decimal formats (0xN, 0bN,
  etc) and no sanity checking (for example, "0x" was interpreted as 72!). I
  made Lm_big_int.of_string to act the same way as Pervasives.int_of_string.

- I changed the way long arrows are translated to HTML in an attept to make
  then actually be long. Please verify under IE and other browsers!

- The extract term (for primiteve rules) needs to be in a slot.


Revision 5954 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jun 19 23:49:18 2004 UTC (17 years ago) by nogin
File length: 28971 byte(s)
Diff to previous 5952
1) Group the modules into theories. Now the filesystem structure has the
following form: "/group/module/rule/nn/nn/nn/..."

Note that "old-style" locations are still valid - any attempt to go to
"/module/..." would result in getting to "/group/module/..." for the group
that the module resides in (but weird things might happen if a group name
clashes with a module name :-(, so do not do that).

The group name and description are specified using THEORYNAME and THEORYDESC
variables in [O]Makefile.

2) I've added an "end" anchor to the end of the messages frame, so hopefully
it will keep scrolling to the right place.


Revision 5952 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jun 19 23:01:14 2004 UTC (17 years ago) by jyh
File length: 29568 byte(s)
Diff to previous 5948
Moved file display forms from Summary to Shell_fs.


Revision 5948 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jun 19 04:03:40 2004 UTC (17 years ago) by jyh
File length: 31097 byte(s)
Diff to previous 5937
Moved the Shell.command struct outside of the shell, so that we can
use these commands in other modules.

Someday we should think about moving Shell_mp and Shell_p4 into the
shell/support directory so we can avoid this imperative nonsense.
One thing to consider, we can abandon Shell_p4 entirely.


Revision 5937 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 18 15:43:37 2004 UTC (17 years ago) by jyh
File length: 31070 byte(s)
Diff to previous 5930
I tried to move the display forms to Shell_fs, but it didn't work,
so I moved it back.


Revision 5930 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 18 05:02:50 2004 UTC (17 years ago) by nogin
File length: 30849 byte(s)
Diff to previous 5924
A few display form fixes:
- directory and file listings should use newline, not hspace
- proof node display needs to put goal/subgoal/assumption/etc terms in a slot.


Revision 5924 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 18 01:15:11 2004 UTC (17 years ago) by jyh
File length: 30818 byte(s)
Diff to previous 5907
Added file support.


Revision 5907 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 16 07:53:11 2004 UTC (17 years ago) by jyh
File length: 30449 byte(s)
Diff to previous 5896
I thought I should commit before we get too out of date.
This is a partial commit; I'll finish off the loose ends
in the morning.

This adds the /fs path for viewing the Unix filesystem.

Notes on this commit:
   1. Removed the "view_*" functions in Shell_core.  These
      duplicated work, and were pretty pointless.

      However, in the browser, I see the following problem:
      the "refresh" function is not called correctly.  The symptom
      is that the display is in "prl" mode.  The solution, until
      I fix in the morning, is to call "refresh ()" explicitly.

   2. Use cd "/fs" to view the filesystem.  However, file editing
      with "cd" is not currently implemented; it is waiting on
      the recent discussion on "proposal for handling pwd()"
      on the onlynews@metaprl.org list.

   3. Shell identifiers now strings.  Sorry for this change, but
      it makes the implementation much easier.  The proper
      path is https://..../session/id1/frameset.


Revision 5896 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jun 13 11:28:58 2004 UTC (17 years ago) by nogin
File length: 29542 byte(s)
Diff to previous 5894
In print_theory, use LsAll (as opposed to the "print nothing" empty set!).

Note, that before the recent ls options management changes we used a custom
selector that took care of automatically ingoring things like ML code. Now
notghing is ignored automatically (a good thing IMHO), which means that we
have to be more careful in placing "docoff" in all the right places.


Revision 5894 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jun 13 08:56:44 2004 UTC (17 years ago) by nogin
File length: 29409 byte(s)
Diff to previous 5883
- Added a "D" (LsDocumentation) flag and a corresponding browser interface
  menu entry to be able to control whether documentation is displayed or not.

- The default view flags are now
  [LsFormal; LsParent; LsRules; LsRewrites; LsDocumentation]

- Now when "u" (lsUnjustified) is removed from the view flags set, the default
  flags are restored (the former "hide everything" behavior did not make much
  sense IMO).

- Removed the "Interface\nbegin\n...\nend" wrapper from the theory display.
  It only waisted 3 lines and 4 columns of screen space without contributing
  anything (and was making things especially confusing when ls options
  other than "all" were used).

- In prl and HTML mode, made the display of the documentation closer to
  the TeX style and less source-like. The individial display forms for some
  pieces of documentation still need work, but overall it IMHO looks OK in prl
  and pretty good in HTML.


Revision 5883 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 11 16:33:41 2004 UTC (17 years ago) by jyh
File length: 29592 byte(s)
Diff to previous 5881
Synchronization fixes.


Revision 5881 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 11 05:26:34 2004 UTC (17 years ago) by nogin
File length: 29610 byte(s)
Diff to previous 5878
Got rif of the unused "internal" flag for the display forms.


Revision 5878 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jun 10 22:51:04 2004 UTC (17 years ago) by nogin
File length: 30486 byte(s)
Diff to previous 5877
Updated a few display forms (including one for sequents and meta-sequents)
to use slot{} in the right places.


Revision 5877 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jun 10 22:06:02 2004 UTC (17 years ago) by jyh
File length: 30486 byte(s)
Diff to previous 5756
Removing some slot terms.  Note that anything displayed in a slot
is selectable from the browser.


Revision 5756 - (view) (download) (annotate) - [select for diffs]
Modified Wed May 5 03:51:20 2004 UTC (17 years, 1 month ago) by jyh
File length: 30488 byte(s)
Diff to previous 5723
In HTML mode: the status line should give *relative* links.


Revision 5723 - (view) (download) (annotate) - [select for diffs]
Modified Mon Apr 26 02:40:08 2004 UTC (17 years, 1 month ago) by nogin
File length: 30488 byte(s)
Diff to previous 5718
In TeX mode, put quotes in    displayed as ``...''.


Revision 5718 - (view) (download) (annotate) - [select for diffs]
Modified Sun Apr 25 04:15:09 2004 UTC (17 years, 2 months ago) by jyh
File length: 30316 byte(s)
Diff to previous 5680
For the formatter, added an "azone" that assumes that its body is
"atomic."  That is, the body is to be typeset all or none.  The width
of an atomic block is 1 unit.

This addresses the formatting problem where multi-character
sequences were getting split.  By default, if we use UTF-8, the
formatter would interpret a multi-character unicode sequence
as multiple characters.  By wrapping it:
    azone <utf-8-sequence> ezone
the utf-8-sequence gets interpreted as an atomic unit.

This should work properly in prl and html mode.  The TeX version
is not implemented, but is no big deal for the moment.

For PRL mode, we may or may not want to split multiple character
Unicode sequences, like atomic["������������������"] (Leftrightarrow)
since it is actually a sequence of several unicode characters.


Revision 5680 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 20 11:16:07 2004 UTC (17 years, 2 months ago) by nogin
File length: 30249 byte(s)
Diff to previous 5668
1. Make sure all session (i.e. non-special) URLs end with a /.
   Rationale:
      (a) It used to be the case that both ".../itt_fset" and ".../itt_fset/"
          would display the itt_fset theory. Obviously, the relative links
          would only work correctly in at most one of the two.
      (b) Between always stripping the last / and always insisting on the
          / ending I chose the latter since it makes figuring out the links
          much easier (e.g. this way the link to a rule in a theory listing
          does not have to include the theory name, just the rule name). Also,
          all the entries in MetaPRL are directory-like (since they are allowed
          to have subentries), so this appears to be consistent.

   As in a standard web server, attempt to go to a URL that does not end with
   a /, but is otherwise valid results in a redirect to a proper URL (i.e. with
   the missing / appended).

2. Linkified the rule and rewrite names. For now all of them are linkified, even
   the primitive ones - this should be fixed eventually. The CSS class is "rule_name".

3. Added the charset information (charset=utf-8) to all the html pages, as required
   in the standard.

4. Changed the style.css, page.html and style-related stuff in layout.js to be
   fully standards-complient (and pass the validator). Note that this also included
   deleting the non-standard "onResize" attribute. Unfortunalely, the divs still
   do not scroll.


Revision 5668 - (view) (download) (annotate) - [select for diffs]
Modified Mon Apr 19 01:46:53 2004 UTC (17 years, 2 months ago) by jyh
File length: 30236 byte(s)
Diff to previous 5647
This is an annoying commit.  It looks massive, but many of the changes
are just to "open" statements.  Here is the issue that is addressed.
   1. Format is a superset of Printf, and it is much better.
   2. MetaPRL's Rformat is a superset of Format, and it is much better.

This commit moves Rformat into libmojave, as Lm_rformat.  With this
commit, all output normally goes through Lm_rformat.  Feel free to
continue to use Format/Printf in special cases, but normal user output
should go through Lm_format/Lm_printf.  You will probably need to use
Lm_pervasives as well.

Lm_pervasives defines an (output_rbuffer : out_channel -> Lm_buffer.t -> unit)
that should be used instead of the print_text_channel function.

There is a new FORMAT option in mk/config.  Define FORMAT=Format to
enable old behavior if you have trouble.

There are two reasons behind this:
   1. We had a mix of files that use Printf and those that use Format
      for output.  This was a mess.  For instance format-style print
      directives (like "@[<hv 3>Content of text box@]@.") can't be
      used in raw Printf.  This meant that output functions had
      to be duplicated, one version for Printf, and one for Format.
      This commit solves the problem.
   2. Another reason, and the real reason behind this, is to allow
      output to be diverted based on the display device.


Revision 5647 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 14 19:02:36 2004 UTC (17 years, 2 months ago) by jyh
File length: 30221 byte(s)
Diff to previous 5576
Added rudimentary support for display in a Web Browser.
To use, use the command "mpopt -browser [-port <int>]",
and follow the directions.  The interface is basically
the same as the normal toploop.  You type commands in
the input area, and MetaPRL displays the output.

Some notes about authentication.  The interface uses
challenge/response validation based on MD5 sums.
The connection requires a password, which is stored
in the clear in a protected file on the MetaPRL host,
and optionally as a cookie in your browser.  The
password is never sent in the clear over the network.

This isn't finished yet, but is pretty usable.  I would
appreciate comments.

TODO:
   1. Some exceptions are not being caught.  In general
      exception printing should be directed to the browser.
   2. Normal output should also be directed to the browser.
   3. Somehow Mozilla is not remembering cookies, which
      means that you have to enter your password more
      often than necessary.  Undoubtably this is due
      to my lack of Javascript knowledge.  If this can be
      fixed, the challenge can be updated frequently.
   4. There are some leftover files from a frame-based
      interface.  Frames are awkward, so I'll delete these
      files after the commit.
   5. I haven't tried it on Win32.


Revision 5576 - (view) (download) (annotate) - [select for diffs]
Modified Tue Mar 30 06:34:42 2004 UTC (17 years, 2 months ago) by nogin
File length: 29819 byte(s)
Diff to previous 5575
A number of display form updates.


Revision 5575 - (view) (download) (annotate) - [select for diffs]
Modified Tue Mar 30 06:05:01 2004 UTC (17 years, 2 months ago) by nogin
File length: 29791 byte(s)
Diff to previous 5335
Adding tail-call optimizations. This makes the asm.s file for the test_fact
28 (out of 114) lines shorter. The optimizations are mostly added as
untrusted (interactive) rewrites, but not yet fully proven.


Revision 5335 - (view) (download) (annotate) - [select for diffs]
Modified Tue Feb 3 02:02:56 2004 UTC (17 years, 4 months ago) by nogin
File length: 29775 byte(s)
Diff to previous 5119
Display the status of the current node (e.g. the status of the proof generated
by the current rulebox only).
I implemented it to be displayed after the path status in "< >".


Revision 5119 - (view) (download) (annotate) - [select for diffs]
Modified Tue Nov 25 00:34:17 2003 UTC (17 years, 7 months ago) by nogin
File length: 29568 byte(s)
Diff to previous 5115
- Do not print a warning message in the Readline history file does not exist.

- Fixed some of the summary dforms (this is a follow-up for
http://cvs.cs.cornell.edu:12000/commitlogs/metaprl/2003-11.html#03/11/19.14:50:46 )

- Updated the BUGS list a bit.


Revision 5115 - (view) (download) (annotate) - [select for diffs]
Modified Wed Nov 19 19:50:46 2003 UTC (17 years, 7 months ago) by nogin
File length: 29592 byte(s)
Diff to previous 5114
******** WARNING - this commit breaks .prlb compatibility ******
******** Export all unsaved proofs to .prla before updating ****

- This commit fully implements the "infix" keyword that allows declaring
infix operators in MetaPRL files (with proper inheritance and scoping).
We used to have a partial implementation of it, but it did not work and was
not used.

- I also added the "suffix" keyword that is similar to the "infix" one.

- I changed the implementation of the standard infixes (such as thenT and thenC)
and the standard suffix (ttca) to use the proper mechanism instead of a filter
hack that defined all the infixes and suffixes globally as a part of the filter
code.


Revision 5114 - (view) (download) (annotate) - [select for diffs]
Modified Wed Nov 19 19:48:50 2003 UTC (17 years, 7 months ago) by nogin
File length: 29494 byte(s)
Diff to previous 4916
This is a no-op commit that removes some white space.


Revision 4916 - (view) (download) (annotate) - [select for diffs]
Modified Wed Sep 3 22:47:35 2003 UTC (17 years, 9 months ago) by nogin
File length: 29553 byte(s)
Diff to previous 4911
Disable the display of cache status for now.


Revision 4911 - (view) (download) (annotate) - [select for diffs]
Modified Wed Sep 3 02:57:45 2003 UTC (17 years, 9 months ago) by nogin
File length: 29314 byte(s)
Diff to previous 4909
Xin & Aleksey:
- Fixed and improved a number of display forms.
- Made a number of improvements to the documentation text.
- Fixed the recent breakage in Itt_rfun (removed the ``experimental'' rule
that Xin have added and removed the unneeded assumption from the original rule).


Revision 4909 - (view) (download) (annotate) - [select for diffs]
Modified Mon Sep 1 23:59:50 2003 UTC (17 years, 9 months ago) by xiny
File length: 29035 byte(s)
Diff to previous 4883
Typo fixes in the documentation.


Revision 4883 - (view) (download) (annotate) - [select for diffs]
Modified Wed Aug 27 19:38:57 2003 UTC (17 years, 9 months ago) by nogin
File length: 29035 byte(s)
Diff to previous 4810
- Removed (using the util/clean-opens script) approx. 2400 unneeded "open"
 statements. This will hopefully reduce the dependency tree size, reduce
the dependency analysis time during compilation and possibly speed up
some partial compilations.

- Removed a number of blank lines (MetaPRL policy is to try not to have more
than one blank line in a row)

- A few minor changes to better disambiguate cases where two modules declare
a type with the same name and both modules are opened.


Revision 4810 - (view) (download) (annotate) - [select for diffs]
Modified Sat Aug 2 12:51:22 2003 UTC (17 years, 10 months ago) by nogin
File length: 29103 byte(s)
Diff to previous 4766
Minor display forms updates. "make latex" now works.


Revision 4766 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 22 02:55:13 2003 UTC (17 years, 11 months ago) by nogin
File length: 29091 byte(s)
Diff to previous 4726
- Restoring a display form that was missing.
- Switching macro.ml to a more canonical syntax (it seems that the curried
syntax for constructors will not be supported in future versions of OCaml).


Revision 4726 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 9 10:31:26 2003 UTC (17 years, 11 months ago) by nogin
File length: 28986 byte(s)
Diff to previous 4723
Got rid of the "arg_subst" part of the tactic_arg - we never used it, and
I do not thing it is likely to be useful in the future.


Revision 4723 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 9 07:20:04 2003 UTC (17 years, 11 months ago) by nogin
File length: 29117 byte(s)
Diff to previous 4698
Merging in the abstract_vars branch:
- variables are now an abstract type, not strings
- MVar parameters are gone

See the branch log messages for more information.

P.S. This is a pretty big change, so I bumped the version number
in mk/preface.


Revision 4698 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 4 11:09:48 2003 UTC (17 years, 11 months ago) by nogin
File length: 28972 byte(s)
Diff to previous 4681
Implemented the <:con< ... >> quotation that is similar to << ... >>, but allows
anti-quotations, which makes it a very espressive mechanism for term construction.

Currently supported syntax:

Terms:
 - $e$    where e is an ML expression of type term
 - !t!    where t is a traditional term "constant" (allows using input shortcuts)
 - '$e$   where e is an ML expression of type string (e.g. creates a variable expr).
 - opname[params]{bterm; bterm; ... } - standard format (params and/or bterms can be omited)

Params:
 - "str"      - string constant
 - id[:kind]  - (kind is one of s,t,n,l) - meta-variable (kind is "s" by default)
 - [0-9]+     - numeric constant
 - $e:kind    - where e is an ML expression of appropriate type
                (string for s,t; Mp_num.num for n, level_exp for l)

Bterm:
 - t
 - bvar, bvar, ..., bvar. term

Bvar:
 - id      - constant bvar
 - $e$     - where e is an ML expression of type string


Revision 4681 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jun 24 13:50:21 2003 UTC (18 years ago) by nogin
File length: 31605 byte(s)
Diff to previous 4675
Display forms for the new PRL bindings.


Revision 4675 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jun 20 00:27:08 2003 UTC (18 years ago) by nogin
File length: 30941 byte(s)
Diff to previous 4611
Fixing display form for the ML rewrites.


Revision 4611 - (view) (download) (annotate) - [select for diffs]
Modified Mon May 19 10:04:06 2003 UTC (18 years, 1 month ago) by nogin
File length: 30952 byte(s)
Diff to previous 4539
- Amended the dform for the "define" directive to include the "displayed as"
part
- Simplified a bunch of proofs in itt_bool.


Revision 4539 - (view) (download) (annotate) - [select for diffs]
Added Fri May 2 04:32:45 2003 UTC (18 years, 1 month ago) by nogin
File length: 30836 byte(s)
This is a first part of a directory restructuring.
I've created support/display, support/shell and support/tactics and
moved everything from theories/tactic and theories/ocaml into support.

P.S. This would break omake, sorry.


This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.26