| 1 | /* =========================================================== | |
| 2 | * JFreeChart : a free chart library for the Java(tm) platform | |
| 3 | * =========================================================== | |
| 4 | * | |
| 5 | * (C) Copyright 2000-2009, by Object Refinery Limited and Contributors. | |
| 6 | * | |
| 7 | * Project Info: http://www.jfree.org/jfreechart/index.html | |
| 8 | * | |
| 9 | * This library is free software; you can redistribute it and/or modify it | |
| 10 | * under the terms of the GNU Lesser General Public License as published by | |
| 11 | * the Free Software Foundation; either version 2.1 of the License, or | |
| 12 | * (at your option) any later version. | |
| 13 | * | |
| 14 | * This library is distributed in the hope that it will be useful, but | |
| 15 | * WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY | |
| 16 | * or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public | |
| 17 | * License for more details. | |
| 18 | * | |
| 19 | * You should have received a copy of the GNU Lesser General Public | |
| 20 | * License along with this library; if not, write to the Free Software | |
| 21 | * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, | |
| 22 | * USA. | |
| 23 | * | |
| 24 | * [Java is a trademark or registered trademark of Sun Microsystems, Inc. | |
| 25 | * in the United States and other countries.] | |
| 26 | * | |
| 27 | * ------------------------- | |
| 28 | * TimeSeriesChartDemo1.java | |
| 29 | * ------------------------- | |
| 30 | * (C) Copyright 2003-2009, by Object Refinery Limited and Contributors. | |
| 31 | * | |
| 32 | * Original Author: David Gilbert (for Object Refinery Limited); | |
| 33 | * Contributor(s): ; | |
| 34 | * | |
| 35 | * Changes | |
| 36 | * ------- | |
| 37 | * 09-Mar-2005 : Version 1, copied from the demo collection that ships with | |
| 38 | * the JFreeChart Developer Guide (DG); | |
| 39 | * 20-Jun-2007 : Removed JCommon dependencies (DG); | |
| 40 | * | |
| 41 | */ | |
| 42 | ||
| 43 | package org.jfree.chart.demo; | |
| 44 | ||
| 45 | import java.awt.Color; | |
| 46 | import java.text.SimpleDateFormat; | |
| 47 | ||
| 48 | import javax.swing.JPanel; | |
| 49 | ||
| 50 | import org.jfree.chart.ChartFactory; | |
| 51 | import org.jfree.chart.ChartPanel; | |
| 52 | import org.jfree.chart.JFreeChart; | |
| 53 | import org.jfree.chart.axis.DateAxis; | |
| 54 | import org.jfree.chart.plot.XYPlot; | |
| 55 | import org.jfree.chart.renderer.xy.XYItemRenderer; | |
| 56 | import org.jfree.chart.renderer.xy.XYLineAndShapeRenderer; | |
| 57 | import org.jfree.chart.util.ApplicationFrame; | |
| 58 | import org.jfree.chart.util.RectangleInsets; | |
| 59 | import org.jfree.chart.util.RefineryUtilities; | |
| 60 | import org.jfree.data.time.Month; | |
| 61 | import org.jfree.data.time.TimeSeries; | |
| 62 | import org.jfree.data.time.TimeSeriesCollection; | |
| 63 | import org.jfree.data.xy.XYDataset; | |
| 64 | ||
| 65 | /** | |
| 66 | * An example of a time series chart. For the most part, default settings are | |
| 67 | * used, except that the renderer is modified to show filled shapes (as well as | |
| 68 | * lines) at each data point. | |
| 69 | */ | |
| 70 | public class TimeSeriesChartDemo1 extends ApplicationFrame { | |
| 71 | ||
| 72 | /** | |
| 73 | * A demonstration application showing how to create a simple time series | |
| 74 | * chart. This example uses monthly data. | |
| 75 | * | |
| 76 | * @param title the frame title. | |
| 77 | */ | |
| 78 | public TimeSeriesChartDemo1(String title) { | |
| 79 | super(title); | |
| 80 | ChartPanel chartPanel = (ChartPanel) createDemoPanel(); | |
| 81 |
1
1. |
chartPanel.setPreferredSize(new java.awt.Dimension(500, 270)); |
| 82 |
1
1. |
setContentPane(chartPanel); |
| 83 | } | |
| 84 | ||
| 85 | /** | |
| 86 | * Creates a chart. | |
| 87 | * | |
| 88 | * @param dataset a dataset. | |
| 89 | * | |
| 90 | * @return A chart. | |
| 91 | */ | |
| 92 | private static JFreeChart createChart(XYDataset dataset) { | |
| 93 | ||
| 94 | JFreeChart chart = ChartFactory.createTimeSeriesChart( | |
| 95 | "Legal & General Unit Trust Prices", "Date", "Price Per Unit", | |
| 96 | dataset, true); | |
| 97 | ||
| 98 |
1
1. createChart : removed call to org/jfree/chart/JFreeChart::setBackgroundPaint → NO_COVERAGE |
chart.setBackgroundPaint(Color.white); |
| 99 | ||
| 100 | XYPlot plot = (XYPlot) chart.getPlot(); | |
| 101 |
1
1. createChart : removed call to org/jfree/chart/plot/XYPlot::setBackgroundPaint → NO_COVERAGE |
plot.setBackgroundPaint(Color.lightGray); |
| 102 |
1
1. createChart : removed call to org/jfree/chart/plot/XYPlot::setDomainGridlinePaint → NO_COVERAGE |
plot.setDomainGridlinePaint(Color.white); |
| 103 |
1
1. createChart : removed call to org/jfree/chart/plot/XYPlot::setRangeGridlinePaint → NO_COVERAGE |
plot.setRangeGridlinePaint(Color.white); |
| 104 |
1
1. createChart : removed call to org/jfree/chart/plot/XYPlot::setAxisOffset → NO_COVERAGE |
plot.setAxisOffset(new RectangleInsets(5.0, 5.0, 5.0, 5.0)); |
| 105 |
1
1. createChart : removed call to org/jfree/chart/plot/XYPlot::setDomainCrosshairVisible → NO_COVERAGE |
plot.setDomainCrosshairVisible(true); |
| 106 |
1
1. createChart : removed call to org/jfree/chart/plot/XYPlot::setRangeCrosshairVisible → NO_COVERAGE |
plot.setRangeCrosshairVisible(true); |
| 107 | ||
| 108 | XYItemRenderer r = plot.getRenderer(); | |
| 109 |
1
1. createChart : negated conditional → NO_COVERAGE |
if (r instanceof XYLineAndShapeRenderer) { |
| 110 | XYLineAndShapeRenderer renderer = (XYLineAndShapeRenderer) r; | |
| 111 |
1
1. createChart : removed call to org/jfree/chart/renderer/xy/XYLineAndShapeRenderer::setBaseShapesVisible → NO_COVERAGE |
renderer.setBaseShapesVisible(true); |
| 112 |
1
1. createChart : removed call to org/jfree/chart/renderer/xy/XYLineAndShapeRenderer::setBaseShapesFilled → NO_COVERAGE |
renderer.setBaseShapesFilled(true); |
| 113 |
1
1. createChart : removed call to org/jfree/chart/renderer/xy/XYLineAndShapeRenderer::setDrawSeriesLineAsPath → NO_COVERAGE |
renderer.setDrawSeriesLineAsPath(true); |
| 114 | } | |
| 115 | ||
| 116 | DateAxis axis = (DateAxis) plot.getDomainAxis(); | |
| 117 |
1
1. createChart : removed call to org/jfree/chart/axis/DateAxis::setDateFormatOverride → NO_COVERAGE |
axis.setDateFormatOverride(new SimpleDateFormat("MMM-yyyy")); |
| 118 | ||
| 119 |
1
1. createChart : mutated return of Object value for org/jfree/chart/demo/TimeSeriesChartDemo1::createChart to ( if (x != null) null else throw new RuntimeException ) → NO_COVERAGE |
return chart; |
| 120 | ||
| 121 | } | |
| 122 | ||
| 123 | /** | |
| 124 | * Creates a dataset, consisting of two series of monthly data. | |
| 125 | * | |
| 126 | * @return The dataset. | |
| 127 | */ | |
| 128 | private static XYDataset createDataset() { | |
| 129 | ||
| 130 | TimeSeries s1 = new TimeSeries("L&G European Index Trust"); | |
| 131 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s1.add(new Month(2, 2001), 181.8); |
| 132 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s1.add(new Month(3, 2001), 167.3); |
| 133 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s1.add(new Month(4, 2001), 153.8); |
| 134 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s1.add(new Month(5, 2001), 167.6); |
| 135 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s1.add(new Month(6, 2001), 158.8); |
| 136 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s1.add(new Month(7, 2001), 148.3); |
| 137 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s1.add(new Month(8, 2001), 153.9); |
| 138 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s1.add(new Month(9, 2001), 142.7); |
| 139 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s1.add(new Month(10, 2001), 123.2); |
| 140 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s1.add(new Month(11, 2001), 131.8); |
| 141 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s1.add(new Month(12, 2001), 139.6); |
| 142 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s1.add(new Month(1, 2002), 142.9); |
| 143 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s1.add(new Month(2, 2002), 138.7); |
| 144 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s1.add(new Month(3, 2002), 137.3); |
| 145 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s1.add(new Month(4, 2002), 143.9); |
| 146 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s1.add(new Month(5, 2002), 139.8); |
| 147 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s1.add(new Month(6, 2002), 137.0); |
| 148 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s1.add(new Month(7, 2002), 132.8); |
| 149 | ||
| 150 | TimeSeries s2 = new TimeSeries("L&G UK Index Trust"); | |
| 151 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s2.add(new Month(2, 2001), 129.6); |
| 152 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s2.add(new Month(3, 2001), 123.2); |
| 153 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s2.add(new Month(4, 2001), 117.2); |
| 154 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s2.add(new Month(5, 2001), 124.1); |
| 155 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s2.add(new Month(6, 2001), 122.6); |
| 156 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s2.add(new Month(7, 2001), 119.2); |
| 157 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s2.add(new Month(8, 2001), 116.5); |
| 158 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s2.add(new Month(9, 2001), 112.7); |
| 159 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s2.add(new Month(10, 2001), 101.5); |
| 160 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s2.add(new Month(11, 2001), 106.1); |
| 161 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s2.add(new Month(12, 2001), 110.3); |
| 162 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s2.add(new Month(1, 2002), 111.7); |
| 163 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s2.add(new Month(2, 2002), 111.0); |
| 164 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s2.add(new Month(3, 2002), 109.6); |
| 165 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s2.add(new Month(4, 2002), 113.2); |
| 166 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s2.add(new Month(5, 2002), 111.6); |
| 167 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s2.add(new Month(6, 2002), 108.8); |
| 168 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeries::add → NO_COVERAGE |
s2.add(new Month(7, 2002), 101.6); |
| 169 | ||
| 170 | // ****************************************************************** | |
| 171 | // More than 150 demo applications are included with the JFreeChart | |
| 172 | // Developer Guide...for more information, see: | |
| 173 | // | |
| 174 | // > http://www.object-refinery.com/jfreechart/guide.html | |
| 175 | // | |
| 176 | // ****************************************************************** | |
| 177 | ||
| 178 | TimeSeriesCollection dataset = new TimeSeriesCollection(); | |
| 179 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeriesCollection::addSeries → NO_COVERAGE |
dataset.addSeries(s1); |
| 180 |
1
1. createDataset : removed call to org/jfree/data/time/TimeSeriesCollection::addSeries → NO_COVERAGE |
dataset.addSeries(s2); |
| 181 | ||
| 182 |
1
1. createDataset : mutated return of Object value for org/jfree/chart/demo/TimeSeriesChartDemo1::createDataset to ( if (x != null) null else throw new RuntimeException ) → NO_COVERAGE |
return dataset; |
| 183 | ||
| 184 | } | |
| 185 | ||
| 186 | /** | |
| 187 | * Creates a panel for the demo (used by SuperDemo.java). | |
| 188 | * | |
| 189 | * @return A panel. | |
| 190 | */ | |
| 191 | public static JPanel createDemoPanel() { | |
| 192 | JFreeChart chart = createChart(createDataset()); | |
| 193 | ChartPanel panel = new ChartPanel(chart); | |
| 194 |
1
1. createDemoPanel : removed call to org/jfree/chart/ChartPanel::setFillZoomRectangle → NO_COVERAGE |
panel.setFillZoomRectangle(true); |
| 195 |
1
1. createDemoPanel : removed call to org/jfree/chart/ChartPanel::setMouseWheelEnabled → NO_COVERAGE |
panel.setMouseWheelEnabled(true); |
| 196 |
1
1. createDemoPanel : mutated return of Object value for org/jfree/chart/demo/TimeSeriesChartDemo1::createDemoPanel to ( if (x != null) null else throw new RuntimeException ) → NO_COVERAGE |
return panel; |
| 197 | } | |
| 198 | ||
| 199 | /** | |
| 200 | * Starting point for the demonstration application. | |
| 201 | * | |
| 202 | * @param args ignored. | |
| 203 | */ | |
| 204 | public static void main(String[] args) { | |
| 205 | ||
| 206 | TimeSeriesChartDemo1 demo = new TimeSeriesChartDemo1( | |
| 207 | "Time Series Chart Demo 1"); | |
| 208 |
1
1. main : removed call to org/jfree/chart/demo/TimeSeriesChartDemo1::pack → NO_COVERAGE |
demo.pack(); |
| 209 |
1
1. main : removed call to org/jfree/chart/util/RefineryUtilities::centerFrameOnScreen → NO_COVERAGE |
RefineryUtilities.centerFrameOnScreen(demo); |
| 210 |
1
1. main : removed call to org/jfree/chart/demo/TimeSeriesChartDemo1::setVisible → NO_COVERAGE |
demo.setVisible(true); |
| 211 | ||
| 212 | } | |
| 213 | ||
| 214 | } | |
Mutations | ||
| 81 |
1.1 |
|
| 82 |
1.1 |
|
| 98 |
1.1 |
|
| 101 |
1.1 |
|
| 102 |
1.1 |
|
| 103 |
1.1 |
|
| 104 |
1.1 |
|
| 105 |
1.1 |
|
| 106 |
1.1 |
|
| 109 |
1.1 |
|
| 111 |
1.1 |
|
| 112 |
1.1 |
|
| 113 |
1.1 |
|
| 117 |
1.1 |
|
| 119 |
1.1 |
|
| 131 |
1.1 |
|
| 132 |
1.1 |
|
| 133 |
1.1 |
|
| 134 |
1.1 |
|
| 135 |
1.1 |
|
| 136 |
1.1 |
|
| 137 |
1.1 |
|
| 138 |
1.1 |
|
| 139 |
1.1 |
|
| 140 |
1.1 |
|
| 141 |
1.1 |
|
| 142 |
1.1 |
|
| 143 |
1.1 |
|
| 144 |
1.1 |
|
| 145 |
1.1 |
|
| 146 |
1.1 |
|
| 147 |
1.1 |
|
| 148 |
1.1 |
|
| 151 |
1.1 |
|
| 152 |
1.1 |
|
| 153 |
1.1 |
|
| 154 |
1.1 |
|
| 155 |
1.1 |
|
| 156 |
1.1 |
|
| 157 |
1.1 |
|
| 158 |
1.1 |
|
| 159 |
1.1 |
|
| 160 |
1.1 |
|
| 161 |
1.1 |
|
| 162 |
1.1 |
|
| 163 |
1.1 |
|
| 164 |
1.1 |
|
| 165 |
1.1 |
|
| 166 |
1.1 |
|
| 167 |
1.1 |
|
| 168 |
1.1 |
|
| 179 |
1.1 |
|
| 180 |
1.1 |
|
| 182 |
1.1 |
|
| 194 |
1.1 |
|
| 195 |
1.1 |
|
| 196 |
1.1 |
|
| 208 |
1.1 |
|
| 209 |
1.1 |
|
| 210 |
1.1 |


debris ice model surface balance glaciers mass ablation data glacier Mullins measured climate temperature time Fig. debris-covered conditions critical rate thickness supraglacial Friedman average changes modern EBM energy past snow {border-style Marchant modelled snowfall solar zone Supplementary atmospheric px;} #ffffff;} accumulation heat precipitation radiation Antarctica IDL Res. forcing meteorological ref. estimate insolation using valley change Geophys. Glaciol. Mackay annual determined flow layer results (see according albedo englacial zones AWS Antarctic downwelling roughness values ASD: Antarctica. Geogr. dynamics environmental example, formation glacial mean measurement rates step total use wind year Sci. based buried estimated measurements period point range rockfall stability summer temperatures value water Head Mars Surface bare computed effective function longwave modelling nearby net px; record rock set threshold ydh {font-family – ka, ‘Methods' Glacier aerodynamic compute continuous daily development estimates flux font-size fresh height high ice-accumulation input internal layers located recorded region sensitivity shortwave used vapour velocity −), ∼ ka -year Figs Glacier, Hock McMurdo Pleistocene Processes Science Taylor age air alpine areas combined corresponding distributed double; equal fluxes following geomorphic ground higher history implications latent location loss numerical obliquity obliquity-paced paleo parameter period. points pressure radar resolution temperature, transfer variations years . cm a Dry Nature Paleo Phys. Valleys, and/or anemometer approach associated available border-color border-width calculated clean cold cold-based concentration conditions, conditions. data, density different directly down-wasting dry equation fit glacier, glaciers, glaciers. global ice, ice-surface ice. include installed length likely lower mast micrometeorological near negative observed radiation, records representative represented represents solid; speeds stake step. study sublimation transmissivity uppermost upwelling velocities {font-style {font-weight ∼ m (). (.°S, (enclosed (that (the ASD Ann. Antarctica, Debris EBM, Earth Finally, GPR Geomorphology Holmgren Huybers Modern Mountains, NSF Periglac. Planet. Quat. Results Rev. TOA Victoria address approximate bold bulk case collected constant cosmogenic cosmogenic-nuclide courier; defined depth derive derived determine direct distance downwasting em; equations events executed firn functions headwall high-latitude highlight horizontal includes insolation, is, linear local major minimum morphological order polar precipitation, profile proxy pt;} refs relative rocks rocky section). similar small southern stakes station stations thermopile units


Techitos Warehouse / Estudio Felipe Escudero
- Curated by Clara Ott
- about 5 hours
Industrial Architecture · Pifo, Ecuador
- version="1.0" encoding="UTF-8"? Architects: Estudio Felipe Escudero
- version="1.0" encoding="UTF-8"?YearCompletion year of this architecture project Year: 2018
- version="1.0" encoding="UTF-8"?PhotographsPhotographs: JAG Studio
- Lead architects Felipe Escudero y Esteban Naranjo
- Design team Isabel Delgado, Kate Troutman, Luis Fernando Sanchez
- Contractor Hugo Ordonez
- Structural engineer Galo Villacis
- Structure contractor Tecnomec
- Lightning Cilo Suarez
More Specs Less Specs
Text description provided by the architects. Tradition, modernity. The industrial building synthesizes the essence of the company that resides in its interior. The design is characterized by differently sized gable roofs, covered by an undulating skin of black aluminum. The building’s aesthetic is complemented by a geometry bounded by sharp cuts at its borders. In the building’s largest warehouse, we find controlled temperature storage for cheese. The inner skin is covered by polyurethane panels that thermally insulate the inner space from the outside.
The office areas are located in the smaller warehouses. The vaulted spaces cause anyone who enters to feel as if they have been immersed into a gothic episode. A contrast is felt in the loft styled spaces, at the wide surfaces of the windows which take advantage of the valley view, and design details that bring a beautiful contemporary touch to the building. Interior lights were conceived as a sculpture, which inhabits the space in a three-dimensional way. The construction has been devised to bear within its limits a yard with a central tree. Thus, inhabitants can enjoy an atmosphere of rest and contemplation, an atmosphere that almost seems to take us to an alternate reality.
Little Roofs was planned with the base idea of taking advantage of all the possibilities of design, starting with a familiar and purely functional building, located in an area of vehicular maneuvers. As a part of this logic, a giant scale pattern was drawn over the surface of the fields, which complements this work. The guard house at the entrance is like a baby to the main structure. It uses the same geometry at a smaller scale, which makes the project in its totality look like a family of mountains. Just like the ones that surround the valleys of the Andean range.


Work out the following equations in the slideshow on a piece of paper or whiteboard.
You can check your answer by clicking the next button.
Slideshow Activity
Directions: Work out the following equations in the slideshow on a piece of paper or whiteboard.
You can check your answer by clicking the next button.
Equation 1
Solve this first equation on a whiteboard or sheet of paper.
Click next to view the answer.


PokemonGo is a free-to-play, location-based augmented reality game developed by Niantic for iOS and Android devices, released in July 2016 with a slow release schedule around the globe.
First off, I'd like to clarify: I do not condone the use of third party tools for PokemonGo as they break the terms of service. I personally use a scanner (Described later) as I feel the game is unfairly balanced for players outside of large cities. I definitely do not condone spoofing or botting, and if you do either of these, you should feel bad.
With the disclaimer out of the way, I'll say it. I love PokemonGo. It's the perfect blend of fresh gameplay with the nostalgia of a well known IP. It's not without it's problems, though. The game has become increasingly frustrating to play due to a combination of terrible changes and lack of communication.
When the game first launched, I'd argue the core gameplay was at its best. It included an in-game tracker that allowed users to track down exactly where rare Pokemon were quickly, provided they were in the sightings list (Around 500 meters)
It's easy to see why this system was so appealing. You notice a rare Pokemon on the sightings list, then wander in certain directions until the distance changes, allowing you to triangulate exactly where the Pokemon is.
During this early period, server issues plagued the game, often only having ~60% uptime - likely an effect caused by the insane popularity of the game. Just before the official UK launch, the footstep tracking system suddenly broke. The number of footsteps remained forever at three, making it much harder to track down. It's estimated that this was to try and combat the server issues, as the distance of the Pokemon to the user would have to be calculated server-side and would likely take a large amount of resources.
This "bug" caused an uproar in the PokemonGo community. The only way you could really catch Pokemon was by walking around until you happen across it. People experimented with triangulating by watching to see when the Pokemon dropped off of the sightings list, but this didn't work due to the Pokemon not being removed from the sightings list. Only by closing the app would the list be cleared. You could travel from London to Manchester and still have Pokemon from London in your sightings.
The lack of any direction to reach Pokemon prompted people to find other ways of finding these Pokemon - and so the dev community excelled...
The most important discovery in the developer community for PokemonGo was that of the API. GitHub user Mila432 (Project recently removed because of a cease and desist letter) reverse engineered the game and discovered the use of an internal API by Niantic. He then developed a publicly accessible version, which used the official Niantic servers to make calls as if you were a normal user, but without the need to actually use a mobile device or use the games UI.
This included functionality to retrieve Pokemon co-ordinates, find local Pokestops, catch Pokemon and lots of other things. This really opened the door for a ton of third party tools, some more sinister than others. The largest projects were "scanners", which allowed players to find Pokemon across their whole city through a web browser.
I'll explain briefly HOW these scanners work. You create a large amount of Pokemon accounts, then use these to repeatedly log into the servers at differing locations to check for Pokemon. Any pokemon found are added to the database, which are then displayed using some front-end system. The issue with this method of finding Pokemon is the scan range is only ~70 meters. When I was scanning across my whole city (186km squared or thereabouts), I was using upwards of 200 accounts, each logging in and scanning every 10-15 seconds. I've heard stories of people using upwards of 5000+ accounts for some services. As you can guess, this is a huge drain on the Niantic servers.
The biggest online service was likely Pokevision (Pictured above). At its peak, it was costing them more than $500 per day for the maps licensing. The service gained 1.2 million Twitter followers in less than 3 weeks. On July 31st, they shutdown due to pressure from Niantic and Nintendo.
With the lack of a good replacement for Pokevision, players (including me), began to look at privately hosted map services, with the most popular options being PokemonGo-map and Pokeminer. Both tried to achieve different objectives - Pokeminer was more suited towards mass analysis of Pokemon spawn-points over large areas. It included heat-map data from you scans (Which is how I created a list of "nests" for my local city, found here). It's easy to use with large amounts of accounts (200+) and didn't have many issues. I originally used this to create city-wide alerts for rare Pokemon using a Twitter and Facebook bot
PokemonGo-Map, on the other-hand, was the much more publicly accepted home scanner solution. It was trending on GitHub for several days. Although difficult to get working with multiple accounts originally, it has developed into a huge project with many optimisations added. The front-end is much higher quality than Pokeminer, and was generally easier to set up with MySQL.
The absolute biggest of these optimisations was by reddit user TBTerra. It had been found that each spawnpoint had a specific time at which a random Pokemon spawned at each hour, such as 11 minutes 55 seconds past every hour. This meant that instead of repeatedly scanning areas where Pokemon might not be, we could scan a spawn-point just after the Pokemon should have spawned. This does require a list of spawn-points, but this is fairly easy to extract from running the program normally and extracted using a simple SQL query to get a JSON file of all spawns. This new method worked incredibly, reducing the amount of accounts needed to efficiently scan a 186km squared area from 200+ accounts to only 15! It would seem all the issues surrounding scanners are solved, right? Low impact on the server, low complexity scanning systems, easy installation.
But alas, Niantic continued to brigade against the use of scanners. They introduced IP bans, where if x number of requests are made from a single IP within y time, the API would send back empty objects, as if nothing nearby was found. After this, they started permanently banning scanning accounts, as well as added captchas to the account creation process, preventing the mass creation of accounts for scanning.
So where do we go from here? There are several options from what I can see:
Niantic optimise their API and make it an official, public API. This would give them a chance to prevent the high server load and possibly close off the API from bots. They tried to prevent unofficial access with Unknown 6 which I didn't cover here, but it didn't last long.
A crowdsourced, decentralised PokemonGo-Map. Essentially, have a VPS running an application server, where users use a modified scanning client and submit locations of rare Pokemon back to the application server. You could gather a community of local players, give them the client (In which they make all the API calls, with their own accounts) that scans locations given to them by the main server. As long as the clients are listening to the server, they would be able to effectively cover ground rather than having 3-4 people all scanning one dense area. Accounts would be unlikely to get scanning accounts banned in this scenario too, as users would use their own small set of accounts, likely no bigger than 4-5 accounts - No IP bans with so little accounts and it's not difficult to create a new account if one gets banned. Since the server would need to be open, rare Pokemon finds would have to be verified server side to ensure it's not a faked Pokemon. This wouldn't be load heavy, though, as it's unlikely to find more than 1-2 rare pokemon every 15 minutes over large areas. It's also important to note that this would only work with rare Pokemon, as having too many Pokemon to verify would cause IP bans/account bans on the server-side of things.
Niantic need to realise that the balance for rural areas is off, and unless they change the meta of the game from "Wander round for 30 hours until you find something rare" then people will always try and create these tools. It's better to be in control of how these systems work/ Hopefully they'll find the error of their ways until it's too late.


Before I was a web professional, before all the project management, front-end coding, and CMS rejiggering, I was an English major. My BA is in writing and, as such, I tend to approach most things I do from the stance of an author.
That being said, the Author User Experience (AUX) of WordPress has been on my mind for a while now. To me, regardless of use, WordPress is about sharing content: articles, images, audio, video. Specifically, WordPress is all about words. It’s right in the name and everything!
When I look at the WordPress admin as it stands now, I see so many amazing author tools. But I only see them because I know where to look—I have been using the tool since 2007 (WP 2.1 - Ella) and have watched it grow.
But familiarity or not, the WordPress authoring experience leaves much to be desired. In fact, I never write new content directly in the WP admin. Rather, I compose my drafts in some outside word processing application (typically Google Docs, but I’ve often just typed out posts in a plain text editor like Notepad or TextEdit). I never thought much of it, but the question must be asked: why do I do this? The obvious answer is because the writing experience inside of WordPress is disruptively jostling, but what specifically is breaking my authoring flow?
For this exploration of the WP AUX, I’m willfully ignoring my I-am-a-web-professional knowledge base and am reviewing the WordPress admin from the stance of a writer of words. I full well know that many of my suggestions run counter to technical hurdles and rationale, but luckily, since I don’t do back-end coding, I can let my suggestions run unfettered by such pesky restrictions as project lineage, technical practicality, or general reality.
Impediments in the WordPress writing experience
The Title
For WordPress authors, the writing experience begins on the Add New Post screen. The very first visual ask of the page is Enter title here. Most authors would agree that the title is the last thing to coalesce during the writing experience. Yet here, it is the first request being made.
So perhaps an author enters a placeholder title for the time being. Once a WP post has a title, the system autosaves the draft and uses the title as a slug to create the permalink. The permalink is the URL of the as-of-yet published article (I won’t get into the fact that all fresh WordPress installs do not have permalinks set as the URL structure by default, which is a continually surprising thing. SEO may be a bit of smoke and mirrors at times, but having informative, human-readable URLs is a must.)
And as jarring as that might be, if you have entered a misspelled word into the title field, there is no red squiggly signifier of your error. Instead, a permalink is generated with the typo for all to see.
What’s great here is that WordPress does allow you to edit the slug, or will automatically generate a new one if the title is changed and re-saved, but it’s still a distraction to the writing process, placing many choices and interactions ahead of the author just typing out their thoughts.
Now, authors could ignore the title field to start (my weirdo brain has trouble doing so), but again, this is WordPress is asking writers to immediately step out of the writing process and actively overlook the (assumed) desired workflow.
Plus, even if you gracefully ignore the title field, once the untitled post is saved, it is given a temporary URL, like www.yoursitename.com/113-98, that does not clue you in on the post’s topic. It’s also pretty ugly to see that advertised just above the writing window. And if you step away from writing and try to come back to this later via the All Posts screen, the presentation of untitled posts is: (no title) - Draft. I typically have a few articles in the creation hopper, so this lack of identifier is troubling and will require a few clicks to find the sought after draft.
Now, let’s leave the title behind us and move on to the actual writing experience.
The WYSIWYG
The WYSIWYG (What You See Is What You Get) is the field to enter all of your article’s content. There are a LOT of controls here. Buttons for adding Media, toggles between the Visual mode and the TEXT mode (being a recovering coder, I prefer the latter), and oodles of formatting options. Again, this is all visual noise standing between the author and their writing. It would be great if all of these things could be hidden or minimized to a single button, similar to how Gmail handles their text formatting toolbar.
The writing field itself is so dinky in WordPress. It’s jammed between the left navigation and the right column of metaboxes for various tasks. I find the actual space for writing my posts within WordPress as too narrow. It’s treated just like any other metabox on the page and feels less like an opportunity to express oneself as a form field on the DMV’s website.
WordPress provides an author two options to counter this Orwellian writing experience: Distraction-free Mode and Screen Options.
To start with the latter, one could use the Screen Options tab to scale down to a single column, but in my experience, most new users don’t even notice the control at the top right of the admin screen. And if you do go this route, any other functionality you may want (like Save) is absolutely buried beneath the writing field. Yes, one can drag-and-drop metaboxes amongst themselves, but not above the writing pane. No mixing!
Distraction-free mode is WordPress’s attempt to dismiss all that visual flotsam and let the author just write. And yes, it makes a good deal of stuff disappear from view, but the writing pane itself does not grow at all. It just stays the same, like it’s saving the place of the left nav. It’s just left stranded slightly off-center in a field of beige-y gray. <img src=”/images/distraction-free.png” title=”Thank god that Word Count is displayed at the bottom though - total AUX win [/sarcasm]”
I’d love to see the screen space dedicated to writing (remember, this is the admin page for writing) to be maximized as much as possible. As mentioned earlier, hiding the formatting tool is a good first step, but let’s use that screen real estate. Let go of the textbox look and feel and, instead, inspire authors to create by giving them a canvas that looks the part.
People have played around with this concept quite a bit, hacking WordPress via seemingly abandoned plugins or visually on Dribbble, but I find much of these to be overly styled. Perhaps it’s my aesthetic, or just my focus on a straightforward writing experience, but I feel a simple yet absorbing writing experience is what WordPress deserves.
The Excerpt
Steeped in WordPress’s blogging heritage (and immortalized in its code), an excerpt is often used on front-end index pages in lieu of displaying the full post content. If not provided, yet called by the WordPress theme in use, the first 55 words of the post are extracted and displayed in its stead.
The idea behind the Excerpt is to provide a teaser of the article’s full content. But the nomenclature is very clinical - almost sterile. The way I think about teasers (and publishing professionals think about deks is something to tantalize the reader while simultaneously building their expectations about the content. It’s the what and the why moment: What is this article about and Why should I read it?
Screen placement aside (as covered above, you can’t get this metafield above the main content field without coding), semantics matter. I’d love to see the presentation of this field move beyond the default descriptor of optional hand-crafted summaries of your content. Bo-ring. This is the marketing moment and could be spruced up to be an Elevator Pitch or even the Hypothesis of the article for the scientifically-minded among us. AUX is more that the visual; it’s about finding the right placement and workflows to engage authors in the writing process. In short, words matter.
Taxonomy: Categories and Tags
Content is only as good as the taxonomies we place upon it. When we search and do research, we’re diving into specific topics. Taxonomic terms (the categories and the tags we apply to our content), helps a reader find what they want.
Any WordPress professional has tried to explain the difference between categories and tags to non-technical authors. Why not cut this conversation off at the start and prompt authors for taxonomies in a differing way.
With categories, I can a more deliberate engagement of the AUX by building a prompt right into the admin’s navigational layout. Historically, blog themes have used language like Filed in for categories, which connotes an archival placement. So rather than shove the Category metabox off to the side or way down the page, tap into the mental process of the author as creator and lead with it.
With tags, the WordPress admin is much for freeform, which I like. Tags are just no pressure and presented as such. And while we could retread the aforementioned screen-placement-of-the-metabox line of critique, let’s instead think about how we tag our content.
Right now, it’s a manual process. Instead, the CMS could do scans of the post’s content and, when a term either jibes with a previously used tag or is used so often in the post as to reach critical taxonomic mass, a tag could be added automatically to a list, ready to be culled or edited by the author once the writing process reaches that point.
What’s more, this automated tagging could support adding variations on a term as well. Your excellent post about your cat could generate the tag cat. But this smart system would also create the plural cats, the scientific feline, and maybe the extrapolation pet. (It’s your imagination’s call if crazy cat lady is also generated).
There are a bunch of plugins that attempt this functionality, but having tested none of them, here they are in order of Still Being Paid Attention to by the Plugin Author:
- https://wordpress.org/plugins/strictly-autotags/
- https://wordpress.org/plugins/automatic-post-tagger/
- https://wordpress.org/plugins/auto-add-tags/
- Abandoned: https://wordpress.org/plugins/auto-tag/
- Abandoned: https://wordpress.org/plugins/auto-tag-generator/
Whether making it more deliberate or propped up by the CMS, WordPress taxonomies can be rethought to make authors’ experiences more focused on the writing.
The Publish Button
This is the one that really grinds my gears. There an author is, composing content to their muse’s delight. They’ve revised, re-thunk, categories, tagged, and achieved that magical moment when they can say to themselves, “Yes, this is ready for the assumedly existing audience of my site. Let’s publish!
So what does an author do now, once they reach the final step in the WordPress AUX? To publish their article, they scroll all the way to the top of the screen again to reach the Publish metabox. I’m no above the fold proselytizer or anything—far from it—but when we’re dealing with a user journey such as this, to force a complete about-face in the final step just feels wrong.
Make the Publish metabox’s layout horizontal and have it stick to the top (or bottom) of the screen as an author scrolls their way down through their article content. For added jazz, the post title could also display in the sticky Publish bar, as could myriad other helpful icons that trigger dropdown menus of functionality.
This is an easy win for WordPress and for the authors who use it.


Name:
Address:
City:
State:
Zip:
Country:
Name on card:
Credit card number:
Expiry Date:
01
02
03
04
05
06
07
08
09
10
11
12
/
CVC:
Fill entire form with default (MasterCard) values
Fill out the name field after 3 seconds
Fill the CVC field with an invalid value
Fill the credit card number and expiration fields only
Fill an expired expiration date
Fill conflicting names
Clear the CVC field
Clear the name fields
Clear the month field
Clear the year field
Clear the expiration date fields
Clear the address fields
Add more fields for current form
Submit


OUR OFFER
INTERSTELLAR
REPAIR THE SHIP
OR SUFFOCATE IN THE COLD
OF THE COSMOS
THRILLER
PUT THE CLUES TOGETHER
TO RESCUE A KIDNAPPED CHILD
REPAIR THE SHIP
OR SUFFOCATE IN THE COLD
OF THE COSMOS
PUT THE CLUES TOGETHER
TO RESCUE A KIDNAPPED CHILD


Definition in file CEdge.h.
Include dependency graph for CEdge.h:
This graph shows which files directly or indirectly include this file:
Go to the source code of this file.


Full window
Mobile Portrait
Mobile Landscape
Small Tablet Portrait
Small Tablet Landscape
Tablet Portrait
Tablet Landscape
Logged In
Reload Template


CatchMap created by Wes Weaverwesmapping.com • @WesWeaver • @wes_fishes_philly • CatchMap on Github This software is free and open source.


Objective
Seeking a challenging career in the field of Civil Structural Engineering in a stimulating and growth oriented environment that utilizes my skills and provides opportunity for learning.
EDUCATIONAL QUALIFICATIONS AND CERTIFICATIONS
Master of Science in Structural Engineering
Jawahar Lal Nehru Technological University Hyderabad, Hyderabad.
Bachelor of Science in Civil Engineering
Osmania University (MJCET), Hyderabad. 2007-2010
Experience
DB STERLIN CONSULTANTS, Chicago, IL.Served as Construction Engineer for Grand Avenue Reconstruction Project which includes partial reconstruction and pavement widening with a composite pavement which will replace the parking and outer travel lanes and update drainage. Sustainable improvements include installation of permeable concrete sidewalks on approximately 20% of the total project, ADA Ramps and new LED arterial davit street lighting.


Abstract
Several groups recently coupled CRISPR perturbations and single-cell RNA-seq for pooled genetic screens. We demonstrate that vector designs of these studies are susceptible to ~50% swapping of guide RNA–barcode associations because of lentiviral template switching. We optimized a published alternative, CROP-seq, in which the guide RNA also serves as the barcode, and here confirm that this strategy performs robustly and doubled the rate at which guides are assigned to cells to 94%.
*co-first author
**co-senior author


Home
Pat's Salmmon Cookies: Sales Data
Shop Name:
Minimum customers per hour
Maximum customers per hour
Avg cookies purchased


--- layout: home title: Game I/O subtitle: Game development workshops and resources use-site-title: true ---
Workshops
Introduction of the workshops, programming language, game development framework and workshop leader.
Start this workshop
Introduction of the different systems of the Phaser Game Engine
Learn the basics of making Pixel Art
Coming soon


In addition to shutter support through GCode. It is possible to wire shutter directly to Raspberry Pi GPIO.
- Servo Motor: By wiring servo motor's pulse pin to GPIO you can control shutters directly.
- True/False: Makes GPIO HIGH and LOW suitable for magnetic shutters or separate shutter control boards.


# orm/instrumentation.py
# Copyright (C) 2005-2015 the SQLAlchemy authors and contributors
# <see AUTHORS file>
#
# This module is part of SQLAlchemy and is released under
# the MIT License: http://www.opensource.org/licenses/mit-license.php
"""Defines SQLAlchemy's system of class instrumentation.
This module is usually not directly visible to user applications, but
defines a large part of the ORM's interactivity.
instrumentation.py deals with registration of end-user classes
for state tracking. It interacts closely with state.py
and attributes.py which establish per-instance and per-class-attribute
instrumentation, respectively.
The class instrumentation system can be customized on a per-class
or global basis using the :mod:`sqlalchemy.ext.instrumentation`
module, which provides the means to build and specify
alternate instrumentation forms.
.. versionchanged: 0.8
The instrumentation extension system was moved out of the
ORM and into the external :mod:`sqlalchemy.ext.instrumentation`
package. When that package is imported, it installs
itself within sqlalchemy.orm so that its more comprehensive
resolution mechanics take effect.
"""
from . import exc, collections, interfaces, state
from .. import util
from . import base
_memoized_key_collection = util.group_expirable_memoized_property()
class ClassManager(dict):
"""tracks state information at the class level."""
MANAGER_ATTR = base.DEFAULT_MANAGER_ATTR
STATE_ATTR = base.DEFAULT_STATE_ATTR
_state_setter = staticmethod(util.attrsetter(STATE_ATTR))
deferred_scalar_loader = None
original_init = object.__init__
factory = None
def __init__(self, class_):
self.class_ = class_
self.info = {}
self.new_init = None
self.local_attrs = {}
self.originals = {}
self._bases = [mgr for mgr in [
manager_of_class(base)
for base in self.class_.__bases__
if isinstance(base, type)
] if mgr is not None]
for base in self._bases:
self.update(base)
self.dispatch._events._new_classmanager_instance(class_, self)
# events._InstanceEventsHold.populate(class_, self)
for basecls in class_.__mro__:
mgr = manager_of_class(basecls)
if mgr is not None:
self.dispatch._update(mgr.dispatch)
self.manage()
self._instrument_init()
if '__del__' in class_.__dict__:
util.warn("__del__() method on class %s will "
"cause unreachable cycles and memory leaks, "
"as SQLAlchemy instrumentation often creates "
"reference cycles. Please remove this method." %
class_)
def __hash__(self):
return id(self)
def __eq__(self, other):
return other is self
@property
def is_mapped(self):
return 'mapper' in self.__dict__
@_memoized_key_collection
def _all_key_set(self):
return frozenset(self)
@_memoized_key_collection
def _collection_impl_keys(self):
return frozenset([
attr.key for attr in self.values() if attr.impl.collection])
@_memoized_key_collection
def _scalar_loader_impls(self):
return frozenset([
attr.impl for attr in
self.values() if attr.impl.accepts_scalar_loader])
@util.memoized_property
def mapper(self):
# raises unless self.mapper has been assigned
raise exc.UnmappedClassError(self.class_)
def _all_sqla_attributes(self, exclude=None):
"""return an iterator of all classbound attributes that are
implement :class:`.InspectionAttr`.
This includes :class:`.QueryableAttribute` as well as extension
types such as :class:`.hybrid_property` and
:class:`.AssociationProxy`.
"""
if exclude is None:
exclude = set()
for supercls in self.class_.__mro__:
for key in set(supercls.__dict__).difference(exclude):
exclude.add(key)
val = supercls.__dict__[key]
if isinstance(val, interfaces.InspectionAttr):
yield key, val
def _attr_has_impl(self, key):
"""Return True if the given attribute is fully initialized.
i.e. has an impl.
"""
return key in self and self[key].impl is not None
def _subclass_manager(self, cls):
"""Create a new ClassManager for a subclass of this ClassManager's
class.
This is called automatically when attributes are instrumented so that
the attributes can be propagated to subclasses against their own
class-local manager, without the need for mappers etc. to have already
pre-configured managers for the full class hierarchy. Mappers
can post-configure the auto-generated ClassManager when needed.
"""
manager = manager_of_class(cls)
if manager is None:
manager = _instrumentation_factory.create_manager_for_cls(cls)
return manager
def _instrument_init(self):
# TODO: self.class_.__init__ is often the already-instrumented
# __init__ from an instrumented superclass. We still need to make
# our own wrapper, but it would
# be nice to wrap the original __init__ and not our existing wrapper
# of such, since this adds method overhead.
self.original_init = self.class_.__init__
self.new_init = _generate_init(self.class_, self)
self.install_member('__init__', self.new_init)
def _uninstrument_init(self):
if self.new_init:
self.uninstall_member('__init__')
self.new_init = None
@util.memoized_property
def _state_constructor(self):
self.dispatch.first_init(self, self.class_)
return state.InstanceState
def manage(self):
"""Mark this instance as the manager for its class."""
setattr(self.class_, self.MANAGER_ATTR, self)
def dispose(self):
"""Dissasociate this manager from its class."""
delattr(self.class_, self.MANAGER_ATTR)
@util.hybridmethod
def manager_getter(self):
return _default_manager_getter
@util.hybridmethod
def state_getter(self):
"""Return a (instance) -> InstanceState callable.
"state getter" callables should raise either KeyError or
AttributeError if no InstanceState could be found for the
instance.
"""
return _default_state_getter
@util.hybridmethod
def dict_getter(self):
return _default_dict_getter
def instrument_attribute(self, key, inst, propagated=False):
if propagated:
if key in self.local_attrs:
return # don't override local attr with inherited attr
else:
self.local_attrs[key] = inst
self.install_descriptor(key, inst)
_memoized_key_collection.expire_instance(self)
self[key] = inst
for cls in self.class_.__subclasses__():
manager = self._subclass_manager(cls)
manager.instrument_attribute(key, inst, True)
def subclass_managers(self, recursive):
for cls in self.class_.__subclasses__():
mgr = manager_of_class(cls)
if mgr is not None and mgr is not self:
yield mgr
if recursive:
for m in mgr.subclass_managers(True):
yield m
def post_configure_attribute(self, key):
_instrumentation_factory.dispatch.\
attribute_instrument(self.class_, key, self[key])
def uninstrument_attribute(self, key, propagated=False):
if key not in self:
return
if propagated:
if key in self.local_attrs:
return # don't get rid of local attr
else:
del self.local_attrs[key]
self.uninstall_descriptor(key)
_memoized_key_collection.expire_instance(self)
del self[key]
for cls in self.class_.__subclasses__():
manager = manager_of_class(cls)
if manager:
manager.uninstrument_attribute(key, True)
def unregister(self):
"""remove all instrumentation established by this ClassManager."""
self._uninstrument_init()
self.mapper = self.dispatch = None
self.info.clear()
for key in list(self):
if key in self.local_attrs:
self.uninstrument_attribute(key)
def install_descriptor(self, key, inst):
if key in (self.STATE_ATTR, self.MANAGER_ATTR):
raise KeyError("%r: requested attribute name conflicts with "
"instrumentation attribute of the same name." %
key)
setattr(self.class_, key, inst)
def uninstall_descriptor(self, key):
delattr(self.class_, key)
def install_member(self, key, implementation):
if key in (self.STATE_ATTR, self.MANAGER_ATTR):
raise KeyError("%r: requested attribute name conflicts with "
"instrumentation attribute of the same name." %
key)
self.originals.setdefault(key, getattr(self.class_, key, None))
setattr(self.class_, key, implementation)
def uninstall_member(self, key):
original = self.originals.pop(key, None)
if original is not None:
setattr(self.class_, key, original)
def instrument_collection_class(self, key, collection_class):
return collections.prepare_instrumentation(collection_class)
def initialize_collection(self, key, state, factory):
user_data = factory()
adapter = collections.CollectionAdapter(
self.get_impl(key), state, user_data)
return adapter, user_data
def is_instrumented(self, key, search=False):
if search:
return key in self
else:
return key in self.local_attrs
def get_impl(self, key):
return self[key].impl
@property
def attributes(self):
return iter(self.values())
# InstanceState management
def new_instance(self, state=None):
instance = self.class_.__new__(self.class_)
if state is None:
state = self._state_constructor(instance, self)
self._state_setter(instance, state)
return instance
def setup_instance(self, instance, state=None):
if state is None:
state = self._state_constructor(instance, self)
self._state_setter(instance, state)
def teardown_instance(self, instance):
delattr(instance, self.STATE_ATTR)
def _serialize(self, state, state_dict):
return _SerializeManager(state, state_dict)
def _new_state_if_none(self, instance):
"""Install a default InstanceState if none is present.
A private convenience method used by the __init__ decorator.
"""
if hasattr(instance, self.STATE_ATTR):
return False
elif self.class_ is not instance.__class__ and \
self.is_mapped:
# this will create a new ClassManager for the
# subclass, without a mapper. This is likely a
# user error situation but allow the object
# to be constructed, so that it is usable
# in a non-ORM context at least.
return self._subclass_manager(instance.__class__).\
_new_state_if_none(instance)
else:
state = self._state_constructor(instance, self)
self._state_setter(instance, state)
return state
def has_state(self, instance):
return hasattr(instance, self.STATE_ATTR)
def has_parent(self, state, key, optimistic=False):
"""TODO"""
return self.get_impl(key).hasparent(state, optimistic=optimistic)
def __bool__(self):
"""All ClassManagers are non-zero regardless of attribute state."""
return True
__nonzero__ = __bool__
def __repr__(self):
return '<%s of %r at %x>' % (
self.__class__.__name__, self.class_, id(self))
class _SerializeManager(object):
"""Provide serialization of a :class:`.ClassManager`.
The :class:`.InstanceState` uses ``__init__()`` on serialize
and ``__call__()`` on deserialize.
"""
def __init__(self, state, d):
self.class_ = state.class_
manager = state.manager
manager.dispatch.pickle(state, d)
def __call__(self, state, inst, state_dict):
state.manager = manager = manager_of_class(self.class_)
if manager is None:
raise exc.UnmappedInstanceError(
inst,
"Cannot deserialize object of type %r - "
"no mapper() has "
"been configured for this class within the current "
"Python process!" %
self.class_)
elif manager.is_mapped and not manager.mapper.configured:
manager.mapper._configure_all()
# setup _sa_instance_state ahead of time so that
# unpickle events can access the object normally.
# see [ticket:2362]
if inst is not None:
manager.setup_instance(inst, state)
manager.dispatch.unpickle(state, state_dict)
class InstrumentationFactory(object):
"""Factory for new ClassManager instances."""
def create_manager_for_cls(self, class_):
assert class_ is not None
assert manager_of_class(class_) is None
# give a more complicated subclass
# a chance to do what it wants here
manager, factory = self._locate_extended_factory(class_)
if factory is None:
factory = ClassManager
manager = factory(class_)
self._check_conflicts(class_, factory)
manager.factory = factory
self.dispatch.class_instrument(class_)
return manager
def _locate_extended_factory(self, class_):
"""Overridden by a subclass to do an extended lookup."""
return None, None
def _check_conflicts(self, class_, factory):
"""Overridden by a subclass to test for conflicting factories."""
return
def unregister(self, class_):
manager = manager_of_class(class_)
manager.unregister()
manager.dispose()
self.dispatch.class_uninstrument(class_)
if ClassManager.MANAGER_ATTR in class_.__dict__:
delattr(class_, ClassManager.MANAGER_ATTR)
# this attribute is replaced by sqlalchemy.ext.instrumentation
# when importred.
_instrumentation_factory = InstrumentationFactory()
# these attributes are replaced by sqlalchemy.ext.instrumentation
# when a non-standard InstrumentationManager class is first
# used to instrument a class.
instance_state = _default_state_getter = base.instance_state
instance_dict = _default_dict_getter = base.instance_dict
manager_of_class = _default_manager_getter = base.manager_of_class
def register_class(class_):
"""Register class instrumentation.
Returns the existing or newly created class manager.
"""
manager = manager_of_class(class_)
if manager is None:
manager = _instrumentation_factory.create_manager_for_cls(class_)
return manager
def unregister_class(class_):
"""Unregister class instrumentation."""
_instrumentation_factory.unregister(class_)
def is_instrumented(instance, key):
"""Return True if the given attribute on the given instance is
instrumented by the attributes package.
This function may be used regardless of instrumentation
applied directly to the class, i.e. no descriptors are required.
"""
return manager_of_class(instance.__class__).\
is_instrumented(key, search=True)
def _generate_init(class_, class_manager):
"""Build an __init__ decorator that triggers ClassManager events."""
# TODO: we should use the ClassManager's notion of the
# original '__init__' method, once ClassManager is fixed
# to always reference that.
original__init__ = class_.__init__
assert original__init__
# Go through some effort here and don't change the user's __init__
# calling signature, including the unlikely case that it has
# a return value.
# FIXME: need to juggle local names to avoid constructor argument
# clashes.
func_body = """\
def __init__(%(apply_pos)s):
new_state = class_manager._new_state_if_none(%(self_arg)s)
if new_state:
return new_state._initialize_instance(%(apply_kw)s)
else:
return original__init__(%(apply_kw)s)
"""
func_vars = util.format_argspec_init(original__init__, grouped=False)
func_text = func_body % func_vars
if util.py2k:
func = getattr(original__init__, 'im_func', original__init__)
func_defaults = getattr(func, 'func_defaults', None)
else:
func_defaults = getattr(original__init__, '__defaults__', None)
func_kw_defaults = getattr(original__init__, '__kwdefaults__', None)
env = locals().copy()
exec(func_text, env)
__init__ = env['__init__']
__init__.__doc__ = original__init__.__doc__
if func_defaults:
__init__.__defaults__ = func_defaults
if not util.py2k and func_kw_defaults:
__init__.__kwdefaults__ = func_kw_defaults
return __init__


--- layout: doc title: Documentation ---
This chapter sketches some of the internal functions and variables of Proof General, to help developers who wish to understand or modify the code.
Most of the documentation below is generated automatically from the comments in the code. Because Emacs lisp is interpreted and self-documenting, the best way to find your way around the source is inside Emacs once Proof General is loaded. Read the source files, and use functions such as C-h v and C-h f.
The code is split into files. The following sections document the important files, kept in the ‘generic/’ subdirectory.
| 14.1 Spans | ||
| 14.2 Proof General site configuration | ||
| 14.3 Configuration variable mechanisms | ||
| 14.4 Global variables | ||
| 14.5 Proof script mode | ||
| 14.6 Proof shell mode | ||
| 14.7 Debugging |
Spans are an abstraction of Emacs overlays originally used to help bridge the gulf between GNU Emacs and XEmacs. See the file ‘lib/span.el’. XEmacs calls these extents which is a name still used in some parts of the code.
The file ‘proof-site.el’ contains the initial configuration for Proof General for the site (or user) and the choice of provers.
The first part of the configuration is to set
proof-home-directory
to the directory that ‘proof-site.el’
is located in, or to the variable of the environment variable
PROOFGENERAL_HOME
if that is set.
Directory where Proof General is installed.
Based on where the file ‘proof-site.el’ was loaded from.
Falls back to consulting the environment variable ‘PROOFGENERAL_HOME’ if
proof-site.el couldn’t know where it was executed from.
Further directory variables allow the files of Proof General to be split
up and installed across a system if need be, rather than under the
proof-home-directory
root.
Where Proof General image files are installed. Ends with slash.
Where Proof General Info files are installed. Ends with slash.
After defining these settings, we define a mode stub for each
proof assistant enabled. The mode stub will autoload Proof General for
the right proof assistant when a file is visited with the corresponding
extension. The proof assistants enabled are the ones listed
in the proof-assistants
setting.
Choice of proof assistants to use with Proof General.
A list of symbols chosen from: ‘coq’ ‘easycrypt’ ‘phox’ ‘qrhl’ ‘pgshell’ ‘pgocaml’ ‘pghaskell’.
If nil, the default will be ALL available proof assistants.
Each proof assistant defines its own instance of Proof General, providing session control, script management, etc. Proof General will be started automatically for the assistants chosen here. To avoid accidently invoking a proof assistant you don’t have, only select the proof assistants you (or your site) may need.
You can select which proof assistants you want by setting this variable before ‘proof-site.el’ is loaded, or by setting the environment variable ‘PROOFGENERAL_ASSISTANTS’ to the symbols you want, for example "coq easycrypt". Or you can edit the file ‘proof-site.el’ itself.
Note: to change proof assistant, you must start a new Emacs session.
The file ‘proof-site.el’ also defines a version variable.
Version string identifying Proof General release.
The file ‘proof-config.el’ defines the configuration variables for Proof General, including instantiation parameters and user options. See previous chapters for details of its contents. Here we mention some conventions for declaring user options.
Global user options and instantiation parameters are declared using
defcustom
as usual. User options should have ‘*
’ as the
first character of their docstrings (standard Emacs convention) and live
in the customize group proof-user-options
. See
‘proof-config.el’ for the groups for instantiation parameters.
User options which are generic (having separate instances for each
prover) and instantiation parameters (by definition generic) can be
declared using the special macro defpgcustom
. It is used in the
same way as defcustom
, except that the symbol declared will
automatically be prefixed by the current proof assistant symbol.
Define a new customization variable <PA>-sym for the current proof assistant.
This is intended for defining settings which are useful for any prover,
but which the user may require different values of across provers.
The function proof-assistant-<SYM> is also defined, which can be used in the generic portion of Proof General to access the value for the current prover.
Arguments args are as for ‘defcustom’, which see. If a :group argument is not supplied, the setting will be added to the internal settings for the current prover (named <PA>-config).
In specific instances of Proof General, the macro defpgdefault
can be used to give a default value for a generic setting.
Set default for the proof assistant specific variable <PA>-sym to value.
This should be used in prover-specific code to alter the default values
for prover specific settings.
Usage: (defpgdefault SYM value)
All new instantiation variables are best declared using the
defpgcustom
mechanism (old code may be converted gradually).
Customizations which are liable to be different for different instances
of Proof General are also best declared in this way. An example is the
use of X Symbol, controlled by PA-x-symbol-enable
, since
it works poorly or not at all with some provers.
To access the generic settings, the following four functions and macros are useful.
Return the value for SYM for the current prover.
This macro should only be invoked once a specific prover is engaged.
Return the symbol for SYM for the current prover. SYM not evaluated.
This macro should only be called once a specific prover is known.
Return the symbol for SYM for the current prover. SYM evaluated.
This macro should only be invoked once a specific prover is engaged.
If changing a user option setting amounts to more than just setting a
variable (it may have some dynamic effect), we can set the
custom-set
property for the variable to the function
proof-set-value
which does an ordinary set-default
to set
the variable, and then calls a function with the same name as the
variable, to do whatever is necessary according to the new value for the
variable.
There are several settings which can be switched on or off by the user,
which use this proof-set-value
mechanism. They are controlled by
boolean variables with names like proof-foo-enable
, and
appear at the start of the customize group proof-user-options
.
They should be edited by the user through the customization mechanism,
and set in the code using customize-set-variable
.
In proof-utils.el
there is a handy macro,
proof-deftoggle
, which constructs an interactive function
for toggling boolean customize settings. We can use this to make an
interactive function proof-foo-toggle
to put on a menu or
bind to a key, for example.
This general scheme is followed as far as possible, to give uniform
behaviour and appearance for boolean user options, as well as
interfacing properly with the customize
mechanism.
Set a customize variable using ‘set-default
’ and a function.
We first call ‘set-default
’ to set sym to value.
Then if there is a function sym (i.e. with the same name as the
variable sym), it is called to take some dynamic action for the new
setting.
If there is no function sym, we try stripping
‘proof-assistant-symbol
’ and adding "proof-" instead to get
a function name. This extends proof-set-value
to work with
generic individual settings.
The dynamic action call only happens when values change: as an approximation we test whether proof-config is fully-loaded yet.
Define a function VAR-toggle for toggling a boolean customize setting VAR.
The toggle function uses ‘customize-set-variable
’ to change the variable.
othername gives an alternative name than the default <VAR>-toggle.
The name of the defined function is returned.
Global variables are defined in ‘proof.el’. The same file defines a few utility functions and some triggers to load in the other files.
The currently active scripting buffer or nil if none.
Process buffer where the proof assistant is run.
The response buffer.
The goals buffer.
Symbol for the type of this buffer: 'script
, 'shell
, 'goals
, or 'response
.
List of files currently included in proof process.
This list contains files in canonical truename format
(see ‘file-truename
’).
Whenever a new file is being processed, it gets added to this list
via the ‘proof-shell-process-file
’ configuration settings.
When the prover retracts a file, this list is resynchronised via the
‘proof-shell-retract-files-regexp
’ and ‘proof-shell-compute-new-files-list
’
configuration settings.
Only files which have been fully processed should be included here. Proof General itself will automatically add the filenames of a script buffer which has been completely read when scripting is deactivated. It will automatically remove the filename of a script buffer which is completely unread when scripting is deactivated.
NB: Currently there is no generic provision for removing files which are only partly read-in due to an error, so ideally the proof assistant should only output a processed message when a file has been successfully read.
Flag indicating that a completed proof has just been observed.
If non-nil, the value counts the commands from the last command
of the proof (starting from 1).
Flag indicating that an error or interrupt has just occurred.
Set to 'error
or 'interrupt
if one was observed from the proof
assistant during the last group of commands.
The file ‘proof-script.el’ contains the main code for proof script mode, as well as definitions of menus, key-bindings, and user-level functions.
Proof scripts have two important variables for the locked and queue regions. These variables are local to each script buffer (although we only really need one queue span in total rather than one per buffer).
The locked span of the buffer.
Each script buffer has its own locked span, which may be detached
from the buffer.
Proof General allows buffers in other modes also to be locked;
these also have a non-nil value for this variable.
The queue span of the buffer. May be detached if inactive or empty.
Each script buffer has its own queue span, although only the active
scripting buffer may have an active queue span.
Various utility functions manipulate and examine the spans. An
important one is proof-init-segmentation
.
Initialise the queue and locked spans in a proof script buffer.
Allocate spans if need be. The spans are detached from the
buffer, so the regions are made empty by this function.
Also clear list of script portions.
For locking files loaded by a proof assistant, we use the next function.
Ensure buffer marked completely processed, completing with a single step.
If buffer already contains a locked region, only the remainder of the buffer is closed off atomically (although undo for the initial portion is unlikely to work, the decoration may be worth retaining).
This works for buffers which are not in proof scripting mode too, to allow other files loaded by proof assistants to be marked read-only.
Atomic locking is instigated by the next function, which uses the
variables proof-included-files-list
documented earlier
(see section Handling Multiple Files and see section Global variables).
Register a possibly new file as having been processed by the prover.
If informprover is non-nil, the proof assistant will be told about this, to co-ordinate with its internal file-management. (Otherwise we assume that it is a message from the proof assistant which triggers this call). In this case, the user will be queried to save some buffers, unless noquestions is non-nil.
No action is taken if the file is already registered.
A warning message is issued if the register request came from the proof assistant and Emacs has a modified buffer visiting the file.
(Unlocking is done by
proof-shell-process-urgent-message-retract
together with
proof-restart-buffers
.)
An important pair of functions activate and deactivate scripting for the
current buffer. A change in the state of active scripting can trigger
various actions, such as starting up the proof assistant, or altering
proof-included-files-list
.
Ready prover and activate scripting for the current script buffer.
The current buffer is prepared for scripting. No changes are
necessary if it is already in Scripting minor mode. Otherwise, it
will become the new active scripting buffer, provided scripting can be
switched off in the previous active scripting buffer with
‘proof-deactivate-scripting
’.
Activating a new script buffer is a good time to ask if the user
wants to save some buffers; this is done if the user option
‘proof-query-file-save-when-activating-scripting
’ is set and
provided the optional argument nosaves is non-nil.
The optional argument queuemode relaxes the test for a busy proof shell to allow one which has mode queuemode. In all other cases, a proof shell busy error is given.
Finally, the hooks ‘proof-activate-scripting-hook
’ are run. This can
be a useful place to configure the proof assistant for scripting in a
particular file, for example, loading the correct theory, or whatever.
If the hooks issue commands to the proof assistant (via
‘proof-shell-invisible-command
’) which result in an error, the
activation is considered to have failed and an error is given.
Try to deactivate scripting for the active scripting buffer.
Aims to set ‘proof-script-buffer
’ to nil and turn off the
modeline indicator. No action is required there is no active
scripting buffer.
We make sure that the active scripting buffer either has no locked
region or a full locked region (everything in it has been processed).
If this is not already the case, we question the user whether to
retract or assert, or automatically take the action indicated in the
user option ‘proof-auto-action-when-deactivating-scripting
’.
If ‘proof-no-fully-processed-buffer
’ is t there is only the choice
to fully retract the active scripting buffer. In this case the
active scripting buffer is retracted even if it was fully processed.
Setting ‘proof-auto-action-when-deactivating-scripting
’ to 'process
is ignored in this case.
If the scripting buffer is (or has become) fully processed, and it is
associated with a file, it is registered on
‘proof-included-files-list
’. Conversely, if it is (or has become)
empty, we make sure that it is not registered. This is to be
certain that the included files list behaves as we might expect with
respect to the active scripting buffer, in an attempt to harmonize
mixed scripting and file reading in the prover.
This function either succeeds, fails because the user refused to
process or retract a partly finished buffer, or gives an error message
because retraction or processing failed. If this function succeeds,
then ‘proof-script-buffer
’ is nil afterwards.
The optional argument forcedaction overrides the user option
‘proof-auto-action-when-deactivating-scripting
’ and prevents
questioning the user. It is used to make a value for
the ‘kill-buffer-hook
’ for scripting buffers, so that when
a scripting buffer is killed it is always retracted.
The function proof-segment-up-to
is the main one used for parsing
the proof script buffer. There are several variants of this function
available corresponding to different parsing strategies; the appropriate
one is aliased to proof-segment-up-to
according to which
configuration variables have been set.
proof-script-sexp-commands
is set, the choice is
proof-script-generic-parse-sexp
.
item If only proof-script-command-end-regexp
or proof-terminal-string
are set,
then the default is proof-script-generic-parse-cmdend
.
proof-script-command-start-regexp
is set, the choice is
proof-script-generic-parse-cmdstart
.
The function proof-semis-to-vanillas
uses
proof-segment-up-to
to convert a parsed region of the script into
a series of commands to be sent to the proof assistant.
For ‘proof-script-parse-function
’ if ‘proof-script-command-end-regexp
’ set.
For ‘proof-script-parse-function
’ if ‘proof-script-command-start-regexp
’ is set.
Used for ‘proof-script-parse-function
’ if ‘proof-script-sexp-commands
’ is set.
Create vanilla spans for semis and a list for the queue.
Proof terminator positions semis has the form returned by
the function ‘proof-segment-up-to’. The argument list is destroyed.
The callback in each queue element is ‘proof-done-advancing
’.
If the variable ‘proof-script-preprocess
’ is set (to the name of
a function), call that function to construct the first element of
each queue item.
The optional queueflags are added to each queue item.
The function proof-assert-until-point
is the main one used to
process commands in the script buffer. It’s actually used to implement
the assert-until-point, electric terminator keypress, and
find-next-terminator behaviours. In different cases we want different
things, but usually the information (i.e. are we inside a comment) isn’t
available until we’ve actually run proof-segment-up-to (point)
,
hence all the different options when we’ve done so.
Process the region from the end of the locked-region until point.
The main command for retracting parts of a script is
proof-retract-until-point
.
Set up the proof process for retracting until point.
This calculates the commands to undo to the current point within
the locked region. If invoked outside the locked region, undo
the last successfully processed command. See ‘proof-retract-target
’.
After retraction has succeeded in the prover, the filter will call
‘proof-done-retracting
’. If undo-action is non-nil, it will
then be invoked on the region in the proof script corresponding to
the proof command sequence.
displayflags control output shown to user, see ‘proof-action-list
’.
Before the retraction is calculated, we enforce the file-level
protocol with ‘proof-activate-scripting
’. This has a couple
of effects:
1. If the file is completely processed, we have to re-open it for scripting again which may involve retracting other (dependent) files.
2. We may query the user whether to save some buffers.
Step 2 may seem odd – we’re undoing (in) the buffer, after all – but what may happen is that when scripting starts going forward again, we hit a command that loads other files, but the user hasn’t saved the latest edits. Therefore it is right to query saves here.
To clean up when scripting is stopped, a script buffer is killed,
a file is retract (and thus must be unlocked), or the
proof assistant exits, we use the functions
proof-restart-buffers
and
proof-script-remove-all-spans-and-deactivate
.
Remove all extents in buffers and maybe reset ‘proof-script-buffer
’.
The high-level effect is that all members of buffers are
completely unlocked, including all the necessary cleanup. No
effect on a buffer which is nil or killed. If one of the buffers
is the current scripting buffer, then ‘proof-script-buffer
’ will
deactivated.
Remove all spans from scripting buffers via ‘proof-restart-buffers
’.
The proof shell mode code is in the file ‘proof-shell.el’. Proof
shell mode is defined to inherit from scomint-mode
using
define-derived-mode
near the end of the file. The
‘scomint.el’ package stands for “simplified comint”, where
comint-mode
is the standard Emacs mode for running an
embedded command interpreter. In scomint
, many of the
interactive commands have been removed to speed up the process
handling, because it isn’t intended that the user interacts
directly with the shell in Proof General.
The bulk of the code in the proof-shell
package is concerned with
sending code to and from the shell, and processing output for the
associated buffers (goals and response).
Good process handling is a tricky issue. Proof General attempts to manage the process strictly, by maintaining a queue of commands to send to the process. Once a command has been processed, another one is popped off the queue and sent.
There are several important internal variables which control interaction with the process.
A lock indicating that the proof shell is processing.
The lock notes that we are processing a queue of commands being sent to the prover, and indicates whether the commands correspond to script management from a buffer (rather than being ad-hoc query commands to the prover).
When processing commands from a buffer for script management,
this will be set to the queue mode 'advancing
or 'retracting
to
indicate the direction of movement.
When this is non-nil, ‘proof-shell-ready-prover
’ will give
an error if called with a different requested queue mode.
See also functions ‘proof-activate-scripting
’ and
‘proof-shell-available-p
’.
Marker in proof shell buffer pointing to previous command input.
The main queue of things to do: spans, commands and actions.
The value is a list of lists of the form
(span commands action [DISPLAYFLAGS]) |
which is the queue of things to do.
span is a region in the sources, where commands come from. Often, additional properties are recorded as properties of span.
commands is a list of strings, holding the text to be send to the prover. It might be the empty list if nothing needs to be sent to the prover, such as, for comments. Usually commands contains just 1 string, but it might also contains more elements. The text should be obtained with ‘(mapconcat ’identity commands " ")’, where the last argument is a space.
action is the callback to be invoked when this item has been
processed by the prover. For normal scripting items it is
‘proof-done-advancing
’, for retract items
‘proof-done-retracting
’, but there are more possibilities (e.g.
‘proof-done-invisible
’, ‘proof-shell-set-silent
’,
‘proof-shell-clear-silent
’ and ‘proof-tree-show-goal-callback
’).
The displayflags are set for non-scripting commands or for when scripting should not bother the user. They may include
|
Note that 'invisible
does not imply any of the others. If flags
are non-empty, interactive cues will be surpressed. (E.g.,
printing hints).
See the functions ‘proof-start-queue
’ and ‘proof-shell-exec-loop
’.
In Proof General 4.2 and earlier it was always the case that all
items from the queue region were present in
proof-action-list
. Because of the new parallel background
compilation for Coq, this is no longer the case. Prover specific
code may now store items from the queue region somewhere else. To
notify generic Proof General about this, it must set
proof-second-action-list-active
for the time where some
queue items are missing from proof-action-list
. In this
case Proof General keeps the proof shell lock and the queue span
even in case proof-action-list
gets empty. Coq uses this
feature to hold back Require commands and the following text
until the asynchronous background compilation finishes.
Signals that some items are waiting outside of ‘proof-action-list
’.
If this is t it means that some items from the queue region are
waiting for being processed in a place different from
‘proof-action-list
’. In this case Proof General must behave as if
‘proof-action-list
’ would be non-empty, when it is, in fact, empty.
This is used, for instance, for parallel background compilation
for Coq: The Require command and the following items are not put
into ‘proof-action-list
’ and are stored somewhere else until the
background compilation finishes. Then those items are put into
‘proof-action-list
’ for getting processed.
Choice of syntax tree encoding for terms.
If nil, prover is expected to make no optimisations. If non-nil, the pretty printer of the prover only reports local changes. For Coq 6.2, use t.
The function proof-shell-start
is used to initialise a shell
buffer and the associated buffers.
Initialise a shell-like buffer for a proof assistant.
Does nothing if proof assistant is already running.
Also generates goal and response buffers.
If ‘proof-prog-name-ask
’ is set, query the user for the
process command.
The function proof-shell-kill-function
performs the converse
function of shutting things down; it is used as a hook function for
kill-buffer-hook
. Then no harm occurs if the user kills the
shell directly, or if it is done more cautiously via
proof-shell-exit
. The function proof-shell-restart
allows
a less drastic way of restarting scripting, other than killing and
restarting the process.
Function run when a proof-shell buffer is killed.
Try to shut down the proof process nicely and clear locked
regions and state variables. Value for ‘kill-buffer-hook
’ in
shell buffer, called by ‘proof-shell-bail-out
’ if process exits.
Query the user and exit the proof process.
This simply kills the ‘proof-shell-buffer
’ relying on the hook function
‘proof-shell-kill-function
’ to do the hard work. If optional
argument dont-ask is non-nil, the proof process is terminated
without confirmation.
The kill function uses ‘<PA>-quit-timeout’ as a timeout to wait
after sending ‘proof-shell-quit-cmd
’ before rudely killing the process.
This function should not be called if
‘proof-shell-exit-in-progress
’ is t, because a recursive call of
‘proof-shell-kill-function
’ will give strange errors.
Value for the process sentinel for the proof assistant process.
If the proof assistant dies, run ‘proof-shell-kill-function
’ to
cleanup and remove the associated buffers. The shell buffer is
left around so the user may discover what killed the process.
event is the string describing the change.
Clear script buffers and send ‘proof-shell-restart-cmd
’.
All locked regions are cleared and the active scripting buffer
deactivated.
If the proof shell is busy, an interrupt is sent with
‘proof-interrupt-process
’ and we wait until the process is ready.
The restart command should re-synchronize Proof General with the proof assistant, without actually exiting and restarting the proof assistant process.
It is up to the proof assistant how much context is cleared: for example, theories already loaded may be "cached" in some way, so that loading them the next time round only performs a re-linking operation, not full re-processing. (One way of caching is via object files, used by Coq).
Input to the proof shell via the queue region is managed by the
functions proof-extend-queue
and proof-shell-exec-loop
.
Extend the current queue with queueitems, queue end end.
To make sense, the commands should correspond to processing actions
for processing a region from (buffer-queue-or-locked-end) to end.
The queue mode is set to 'advancing
Extend the current queue with queueitems, queue end end.
To make sense, the commands should correspond to processing actions
for processing a region from (buffer-queue-or-locked-end) to end.
The queue mode is set to 'advancing
Main loop processing the ‘proof-action-list
’, called from shell filter.
‘proof-action-list
’ contains a list of (span command action [FLAGS]) lists.
If this function is called with a non-empty ‘proof-action-list
’, the
head of the list is the previously executed command which succeeded.
We execute the callback (action span) on the first item,
then (action span) on any following items which have null as
their cmd components.
If a there is a next command after that, send it to the process.
If the action list becomes empty, unlock the process and remove the queue region.
The return value is non-nil if the action list is now empty or contains only invisible elements for Prooftree synchronization.
Input is actually inserted into the shell buffer and sent to the process
by the low-level function proof-shell-insert
.
Insert strings at the end of the proof shell, call ‘scomint-send-input
’.
strings is a list of strings (which will be concatenated), or a single string.
The action argument is a symbol which is typically the name of a callback for when each string has been processed.
This calls ‘proof-shell-insert-hook
’. The arguments action and
scriptspan may be examined by the hook to determine how to modify
the string variable (exploiting dynamic scoping) which will be
the command actually sent to the shell.
Note that the hook is not called for the empty (null) string or a carriage return.
We strip the string of carriage returns before inserting it
and updating ‘proof-marker
’ to point to the end of the newly
inserted text.
Do not use this function directly, or output will be lost. It is only
used in ‘proof-add-to-queue
’ when we start processing a queue, and in
‘proof-shell-exec-loop
’, to process the next item.
When Proof General is processing a queue of commands, the lock is managed using a couple of utility functions. You should not need to use these directly.
Grab the proof shell lock, starting the proof assistant if need be.
Runs ‘proof-state-change-hook
’ to notify state change.
If queuemode is supplied, set the lock to that value.
Release the proof shell lock. Clear ‘proof-shell-busy
’.
Two main functions deal with output, proof-shell-classify-output
and proof-shell-process-urgent-message
. In effect we consider
the output to be two streams intermingled: the "urgent" messages which
have "eager" annotations, as well as the ordinary ruminations from the
prover.
The idea is to conceal as much irrelevant information from the user as
possible; only the remaining output between prompts and after the last
urgent message will be a candidate for the goal or response buffer. The
internal variable proof-shell-urgent-message-marker
tracks the
last urgent message seen.
When output is grabbed from the prover process, the first action
is to strip spurious carriage return characters from the end of
lines, if proof-shell-strip-crs-from-output
requires it.
Then the output is stored into
proof-shell-last-output
, and its type is stored in
proof-shell-last-output-kind
. Output which is deferred or
possibly discarded until the queue is empty is copied into
proof-shell-delayed-output
, with type
proof-shell-delayed-output-kind
. A record of the last prompt
seen from the prover process is also kept, in
proof-shell-last-prompt
.
If non-nil, remove carriage returns (^M) at the end of lines from output.
This is enabled for cygwin32 systems by default. You should turn it off
if you don’t need it (slight speed penalty).
A raw record of the last prompt seen from the proof system.
This is the string matched by ‘proof-shell-annotated-prompt-regexp
’.
A record of the last string seen from the proof system.
This is raw string, for internal use only.
A symbol denoting the type of the last output string from the proof system.
Specifically:
|
The output corresponding to this will be in ‘proof-shell-last-output
’.
See also ‘proof-shell-proof-completed
’ for further information about
the proof process output, when ends of proofs are spotted.
This variable can be used for instance specific functions which want
to examine ‘proof-shell-last-output
’.
A symbol denoting the type of the last output string from the proof system.
Specifically:
|
The output corresponding to this will be in ‘proof-shell-last-output
’.
See also ‘proof-shell-proof-completed
’ for further information about
the proof process output, when ends of proofs are spotted.
This variable can be used for instance specific functions which want
to examine ‘proof-shell-last-output
’.
A record of the start of the previous output in the shell buffer.
The previous output is held back for processing at end of queue.
A record of the start of the previous output in the shell buffer.
The previous output is held back for processing at end of queue.
A copy of the ‘proof-action-list
’ flags for ‘proof-shell-delayed-output’.
See if the output between start and end must be dealt with immediately.
To speed up processing, PG tries to avoid displaying output that
the user will not have a chance to see. Some output must be
handled immediately, however: these are errors, interrupts,
goals and loopbacks (proof step hints/proof by pointing results).
In this function we check, in turn:
‘ |
Other kinds of output are essentially display only, so only dealt with if necessary.
To extend this, set ‘proof-shell-handle-output-system-specific
’,
which is a hook to take particular additional actions.
This function sets variables: ‘proof-shell-last-output-kind
’,
and the counter ‘proof-shell-proof-completed
’ which counts commands
after a completed proof.
Display delayed goals/responses, when queue is stopped or completed.
This function handles the cases of ‘proof-shell-output-kind’ which
are not dealt with eagerly during script processing, namely
'response
and 'goals
types.
This is useful even with empty delayed output as it will empty the buffers.
The delayed output is in the region
[proof-shell-delayed-output-start
,proof-shell-delayed-output-end
].
If no goals classified output is found, the whole output is displayed in the response buffer.
If goals output is found, the last matching instance, possibly
bounded by ‘proof-shell-end-goals-regexp
’, will be displayed
in the goals buffer (and may be further analysed by Proof General).
Any output that appears before the last goals output (but
after messages classified as urgent, see ‘proof-shell-filter
’)
will also be displayed in the response buffer.
For example, if output has this form:
messsage-1 goals-1 message-2 goals-2 junk |
then goals-2 will be displayed in the goals buffer, and message-2 in the response buffer. junk will be ignored.
Notice that the above alternation (and separation of junk) can
only be distinguished if both ‘proof-shell-start-goals-regexp
’
and ‘proof-shell-end-goals-regexp
’ are set. With just the start
goals regexp set, goals-2 junk will appear in the goals buffer
and no response output would occur.
The goals and response outputs are copied into
‘proof-shell-last-goals-output
’ and
‘proof-shell-last-response-output
’ respectively.
The value returned is the value for ‘proof-shell-last-output-kind
’,
i.e., 'goals
or 'response
.
Marker in proof shell buffer pointing to end of last urgent message.
Analyse urgent message between start and end for various cases.
Cases are: trace output, included/retracted files, cleared goals/response buffer, variable setting, xml-encoded pgip response, theorem dependency message or interactive output indicator.
If none of these apply, display the text between start and end.
The text between start and end should be a string that starts with
text matching ‘proof-shell-eager-annotation-start
’ and
ends with text matching ‘proof-shell-eager-annotation-end
’.
The main processing point which triggers other actions is
proof-shell-filter
. It is called from
proof-shell-filter-wrapper
, which itself is called from an
ordinary Emacs process filter inside the simplified comint
library that is distributed with Proof General (in
lib/scomint.el
).
Master filter for the proof assistant shell-process.
A function for ‘scomint-output-filter-functions
’.
Deal with output and issue new input from the queue. This is an
important internal function. The output must be collected from
‘proof-shell-buffer
’ for the following reason. This function
might block inside ‘process-send-string
’ when sending input to
the proof assistant or to prooftree. In this case Emacs might
call the process filter again while the previous instance is
still running. ‘proof-shell-filter-wrapper
’ detects and delays
such calls but does not buffer the output.
Handle urgent messages first. As many as possible are processed,
using the function ‘proof-shell-process-urgent-messages
’.
If a prompt is seen, run ‘proof-shell-filter-manage-output
’ on the
output between the new prompt and the last input (position of
‘proof-marker
’) or the last urgent message (position of
‘proof-shell-urgent-message-marker
’), whichever is later. For
example, in this case:
PROMPT> input output-1 urgent-message-1 output-2 urgent-message-2 output-3 PROMPT> |
‘proof-marker
’ points after input.
‘proof-shell-urgent-message-marker
’ points after urgent-message-2,
after both urgent messages have been processed by
‘proof-shell-process-urgent-messages
’. Urgent messages always
processed; they are intended to correspond to informational
notes that the prover makes to inform the user or interface on
progress.
In this case, the ordinary outputs output-1 and output-2 are
ignored; only output-3 will be processed by
‘proof-shell-filter-manage-output
’.
Error or interrupt messages are expected to terminate an interactive output and appear last before a prompt and will always be processed. Error messages and interrupt messages are therefore not considered as urgent messages.
The first time that a prompt is seen, ‘proof-marker
’ is
initialised to the end of the prompt. This should correspond
with initializing the process. After that, ‘proof-marker
’
is only changed when input is sent in ‘proof-shell-insert
’.
Subroutine of ‘proof-shell-filter
’ for output between start and end.
First, we invoke ‘proof-shell-handle-immediate-output
’ which classifies
and handles output that must be dealt with immediately.
Other output (user display) is only displayed when the proof action list becomes empty, to avoid a confusing rapidly changing output that slows down processing.
After processing the current output, the last step undertaken by the filter is to send the next command from the queue.
Wrapper for ‘proof-shell-filter
’, protecting against parallel calls.
In Emacs a process filter function can be called while the same
filter is currently running for the same process, for instance,
when the filter blocks on I/O. This wrapper protects the main
entry point, ‘proof-shell-filter
’ against such parallel,
overlapping calls.
The argument str-do-not-use contains the most recent output, but
is discarded. ‘proof-shell-filter
’ collects the output from
‘proof-shell-buffer
’ (where it is inserted by
‘scomint-output-filter
’), relieving this function from the task
to buffer the output that arrives during parallel, overlapping
calls.
To debug Proof General, it may be helpful to set the
configuration variable proof-general-debug
.
Non-nil to run Proof General in debug mode.
This changes some behaviour (e.g. markup stripping) and displays
debugging messages in the response buffer. To avoid erasing
messages shortly after they’re printed, set ‘proof-tidy-response
’ to nil.
This is only useful for PG developers.
The default value is nil
.
For more information about debugging Emacs lisp, consult the Emacs Lisp
Reference Manual. I recommend using the source-level debugger
edebug
.
This document was generated on April 14, 2023 using texi2html 1.82.


{% extends "base.html" %} {% block title %}Sample Home{% endblock title %} {% block content %}
This is the index.html page of the sample app.


--- # Feel free to add content and custom Front Matter to this file. # To modify the layout, see https://jekyllrb.com/docs/themes/#overriding-theme-defaults layout: home products: - title: On-Call Schedule url: /products/on-call-schedule image: /images/on-call-schedule.jpg desc: Lets you efficiently create on-call calendars based on your team --- {%- if page.products.size > 0 -%}
{{ product.desc }}